Theorem cnvprop

Description: Converse of a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023)

	Ref	Expression
Assertion	cnvprop	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ) → ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { ⟨ 𝐵 , 𝐴 ⟩ , ⟨ 𝐷 , 𝐶 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		cnvsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ◡ { ⟨ 𝐴 , 𝐵 ⟩ } = { ⟨ 𝐵 , 𝐴 ⟩ } )
2	1	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ) → ◡ { ⟨ 𝐴 , 𝐵 ⟩ } = { ⟨ 𝐵 , 𝐴 ⟩ } )
3		cnvsng	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) → ◡ { ⟨ 𝐶 , 𝐷 ⟩ } = { ⟨ 𝐷 , 𝐶 ⟩ } )
4	3	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ) → ◡ { ⟨ 𝐶 , 𝐷 ⟩ } = { ⟨ 𝐷 , 𝐶 ⟩ } )
5	2 4	uneq12d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ) → ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ◡ { ⟨ 𝐶 , 𝐷 ⟩ } ) = ( { ⟨ 𝐵 , 𝐴 ⟩ } ∪ { ⟨ 𝐷 , 𝐶 ⟩ } ) )
6		df-pr	⊢ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } )
7	6	cnveqi	⊢ ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ◡ ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } )
8		cnvun	⊢ ◡ ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) = ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ◡ { ⟨ 𝐶 , 𝐷 ⟩ } )
9	7 8	eqtri	⊢ ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∪ ◡ { ⟨ 𝐶 , 𝐷 ⟩ } )
10		df-pr	⊢ { ⟨ 𝐵 , 𝐴 ⟩ , ⟨ 𝐷 , 𝐶 ⟩ } = ( { ⟨ 𝐵 , 𝐴 ⟩ } ∪ { ⟨ 𝐷 , 𝐶 ⟩ } )
11	5 9 10	3eqtr4g	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ) → ◡ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { ⟨ 𝐵 , 𝐴 ⟩ , ⟨ 𝐷 , 𝐶 ⟩ } )