f1oprswap

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

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

Proof

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

Metamath Proof Explorer

Theorem f1oprswap

Proof