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