Theorem cnvprop

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

	Ref	Expression
Assertion	cnvprop	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(C\in V\wedge D\in W\right)\right)\to {\left\{⟨A,B⟩,⟨C,D⟩\right\}}^{-1}=\left\{⟨B,A⟩,⟨D,C⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cnvsng	$$⊢\left(A\in V\wedge B\in W\right)\to {\left\{⟨A,B⟩\right\}}^{-1}=\left\{⟨B,A⟩\right\}$$
2	1	adantr	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(C\in V\wedge D\in W\right)\right)\to {\left\{⟨A,B⟩\right\}}^{-1}=\left\{⟨B,A⟩\right\}$$
3		cnvsng	$$⊢\left(C\in V\wedge D\in W\right)\to {\left\{⟨C,D⟩\right\}}^{-1}=\left\{⟨D,C⟩\right\}$$
4	3	adantl	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(C\in V\wedge D\in W\right)\right)\to {\left\{⟨C,D⟩\right\}}^{-1}=\left\{⟨D,C⟩\right\}$$
5	2 4	uneq12d	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(C\in V\wedge D\in W\right)\right)\to {\left\{⟨A,B⟩\right\}}^{-1}\cup {\left\{⟨C,D⟩\right\}}^{-1}=\left\{⟨B,A⟩\right\}\cup \left\{⟨D,C⟩\right\}$$
6		df-pr	$$⊢\left\{⟨A,B⟩,⟨C,D⟩\right\}=\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}$$
7	6	cnveqi	$$⊢{\left\{⟨A,B⟩,⟨C,D⟩\right\}}^{-1}={\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)}^{-1}$$
8		cnvun	$$⊢{\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)}^{-1}={\left\{⟨A,B⟩\right\}}^{-1}\cup {\left\{⟨C,D⟩\right\}}^{-1}$$
9	7 8	eqtri	$$⊢{\left\{⟨A,B⟩,⟨C,D⟩\right\}}^{-1}={\left\{⟨A,B⟩\right\}}^{-1}\cup {\left\{⟨C,D⟩\right\}}^{-1}$$
10		df-pr	$$⊢\left\{⟨B,A⟩,⟨D,C⟩\right\}=\left\{⟨B,A⟩\right\}\cup \left\{⟨D,C⟩\right\}$$
11	5 9 10	3eqtr4g	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(C\in V\wedge D\in W\right)\right)\to {\left\{⟨A,B⟩,⟨C,D⟩\right\}}^{-1}=\left\{⟨B,A⟩,⟨D,C⟩\right\}$$