Metamath Proof Explorer

Theorem prwf

Description: An unordered pair is well-founded if its elements are. (Contributed by Mario Carneiro, 10-Jun-2013) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion prwf ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → A B ∈ ⋃ R1 On

Proof

Step Hyp Ref Expression
1 df-pr ⊢ A B = A ∪ B
2 snwf ⊢ A ∈ ⋃ R1 On → A ∈ ⋃ R1 On
3 snwf ⊢ B ∈ ⋃ R1 On → B ∈ ⋃ R1 On
4 unwf ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On ↔ A ∪ B ∈ ⋃ R1 On
5 4 biimpi ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → A ∪ B ∈ ⋃ R1 On
6 2 3 5 syl2an ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → A ∪ B ∈ ⋃ R1 On
7 1 6 eqeltrid ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → A B ∈ ⋃ R1 On