This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → { 𝐴 , 𝐵 } ∈ ∪ ( 𝑅1 “ On ) )

Proof

Step Hyp Ref Expression
1 df-pr ⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
2 snwf ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) )
3 snwf ⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) )
4 unwf ⊢ ( ( { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) ↔ ( { 𝐴 } ∪ { 𝐵 } ) ∈ ∪ ( 𝑅1 “ On ) )
5 4 biimpi ⊢ ( ( { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) → ( { 𝐴 } ∪ { 𝐵 } ) ∈ ∪ ( 𝑅1 “ On ) )
6 2 3 5 syl2an ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( { 𝐴 } ∪ { 𝐵 } ) ∈ ∪ ( 𝑅1 “ On ) )
7 1 6 eqeltrid ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → { 𝐴 , 𝐵 } ∈ ∪ ( 𝑅1 “ On ) )