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 ) )