Theorem f1oprswap

Description: A two-element swap is a bijection on a pair. (Contributed by Mario Carneiro, 23-Jan-2015)

	Ref	Expression
Assertion	f1oprswap	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{⟨A,B⟩,⟨B,A⟩\right\}:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{A,B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		f1osng	$$⊢\left(A\in V\wedge A\in V\right)\to \left\{⟨A,A⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}$$
2	1	anidms	$$⊢A\in V\to \left\{⟨A,A⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}$$
3	2	ad2antrr	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge A=B\right)\to \left\{⟨A,A⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}$$
4		dfsn2	$$⊢\left\{⟨A,A⟩\right\}=\left\{⟨A,A⟩,⟨A,A⟩\right\}$$
5		opeq2	$$⊢A=B\to ⟨A,A⟩=⟨A,B⟩$$
6		opeq1	$$⊢A=B\to ⟨A,A⟩=⟨B,A⟩$$
7	5 6	preq12d	$$⊢A=B\to \left\{⟨A,A⟩,⟨A,A⟩\right\}=\left\{⟨A,B⟩,⟨B,A⟩\right\}$$
8	4 7	eqtrid	$$⊢A=B\to \left\{⟨A,A⟩\right\}=\left\{⟨A,B⟩,⟨B,A⟩\right\}$$
9		dfsn2	$$⊢\left\{A\right\}=\left\{A,A\right\}$$
10		preq2	$$⊢A=B\to \left\{A,A\right\}=\left\{A,B\right\}$$
11	9 10	eqtrid	$$⊢A=B\to \left\{A\right\}=\left\{A,B\right\}$$
12	8 11 11	f1oeq123d	$$⊢A=B\to \left(\left\{⟨A,A⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\leftrightarrow \left\{⟨A,B⟩,⟨B,A⟩\right\}:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{A,B\right\}\right)$$
13	12	adantl	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge A=B\right)\to \left(\left\{⟨A,A⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{A\right\}\leftrightarrow \left\{⟨A,B⟩,⟨B,A⟩\right\}:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{A,B\right\}\right)$$
14	3 13	mpbid	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge A=B\right)\to \left\{⟨A,B⟩,⟨B,A⟩\right\}:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{A,B\right\}$$
15		simpll	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge A\ne B\right)\to A\in V$$
16		simplr	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge A\ne B\right)\to B\in W$$
17		simpr	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge A\ne B\right)\to A\ne B$$
18		fnprg	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(B\in W\wedge A\in V\right)\wedge A\ne B\right)\to \left\{⟨A,B⟩,⟨B,A⟩\right\}Fn\left\{A,B\right\}$$
19	15 16 16 15 17 18	syl221anc	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge A\ne B\right)\to \left\{⟨A,B⟩,⟨B,A⟩\right\}Fn\left\{A,B\right\}$$
20		cnvsng	$$⊢\left(A\in V\wedge B\in W\right)\to {\left\{⟨A,B⟩\right\}}^{-1}=\left\{⟨B,A⟩\right\}$$
21		cnvsng	$$⊢\left(B\in W\wedge A\in V\right)\to {\left\{⟨B,A⟩\right\}}^{-1}=\left\{⟨A,B⟩\right\}$$
22	21	ancoms	$$⊢\left(A\in V\wedge B\in W\right)\to {\left\{⟨B,A⟩\right\}}^{-1}=\left\{⟨A,B⟩\right\}$$
23	20 22	uneq12d	$$⊢\left(A\in V\wedge B\in W\right)\to {\left\{⟨A,B⟩\right\}}^{-1}\cup {\left\{⟨B,A⟩\right\}}^{-1}=\left\{⟨B,A⟩\right\}\cup \left\{⟨A,B⟩\right\}$$
24		uncom	$$⊢\left\{⟨B,A⟩\right\}\cup \left\{⟨A,B⟩\right\}=\left\{⟨A,B⟩\right\}\cup \left\{⟨B,A⟩\right\}$$
25	23 24	eqtrdi	$$⊢\left(A\in V\wedge B\in W\right)\to {\left\{⟨A,B⟩\right\}}^{-1}\cup {\left\{⟨B,A⟩\right\}}^{-1}=\left\{⟨A,B⟩\right\}\cup \left\{⟨B,A⟩\right\}$$
26	25	adantr	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge A\ne B\right)\to {\left\{⟨A,B⟩\right\}}^{-1}\cup {\left\{⟨B,A⟩\right\}}^{-1}=\left\{⟨A,B⟩\right\}\cup \left\{⟨B,A⟩\right\}$$
27		df-pr	$$⊢\left\{⟨A,B⟩,⟨B,A⟩\right\}=\left\{⟨A,B⟩\right\}\cup \left\{⟨B,A⟩\right\}$$
28	27	cnveqi	$$⊢{\left\{⟨A,B⟩,⟨B,A⟩\right\}}^{-1}={\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨B,A⟩\right\}\right)}^{-1}$$
29		cnvun	$$⊢{\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨B,A⟩\right\}\right)}^{-1}={\left\{⟨A,B⟩\right\}}^{-1}\cup {\left\{⟨B,A⟩\right\}}^{-1}$$
30	28 29	eqtri	$$⊢{\left\{⟨A,B⟩,⟨B,A⟩\right\}}^{-1}={\left\{⟨A,B⟩\right\}}^{-1}\cup {\left\{⟨B,A⟩\right\}}^{-1}$$
31	26 30 27	3eqtr4g	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge A\ne B\right)\to {\left\{⟨A,B⟩,⟨B,A⟩\right\}}^{-1}=\left\{⟨A,B⟩,⟨B,A⟩\right\}$$
32	31	fneq1d	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge A\ne B\right)\to \left({\left\{⟨A,B⟩,⟨B,A⟩\right\}}^{-1}Fn\left\{A,B\right\}\leftrightarrow \left\{⟨A,B⟩,⟨B,A⟩\right\}Fn\left\{A,B\right\}\right)$$
33	19 32	mpbird	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge A\ne B\right)\to {\left\{⟨A,B⟩,⟨B,A⟩\right\}}^{-1}Fn\left\{A,B\right\}$$
34		dff1o4	$$⊢\left\{⟨A,B⟩,⟨B,A⟩\right\}:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{A,B\right\}\leftrightarrow \left(\left\{⟨A,B⟩,⟨B,A⟩\right\}Fn\left\{A,B\right\}\wedge {\left\{⟨A,B⟩,⟨B,A⟩\right\}}^{-1}Fn\left\{A,B\right\}\right)$$
35	19 33 34	sylanbrc	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge A\ne B\right)\to \left\{⟨A,B⟩,⟨B,A⟩\right\}:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{A,B\right\}$$
36	14 35	pm2.61dane	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{⟨A,B⟩,⟨B,A⟩\right\}:\left\{A,B\right\}\underset{1-1\; onto}{⟶}\left\{A,B\right\}$$