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

Metamath Proof Explorer

Theorem opwf

Description: An ordered pair is well-founded if its elements are. (Contributed by Mario Carneiro, 10-Jun-2013)

Ref Expression
Assertion opwf ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ∪ ( 𝑅1 “ On ) )

Proof

Step Hyp Ref Expression
1 dfopg ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } )
2 snwf ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) )
3 prwf ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → { 𝐴 , 𝐵 } ∈ ∪ ( 𝑅1 “ On ) )
4 prwf ⊢ ( ( { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐴 , 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) → { { 𝐴 } , { 𝐴 , 𝐵 } } ∈ ∪ ( 𝑅1 “ On ) )
5 2 3 4 syl2an2r ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → { { 𝐴 } , { 𝐴 , 𝐵 } } ∈ ∪ ( 𝑅1 “ On ) )
6 1 5 eqeltrd ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ∪ ( 𝑅1 “ On ) )