f1ofvswap

Description: Swapping two values in a bijection between two classes yields another bijection between those classes. (Contributed by BTernaryTau, 31-Aug-2024)

		Ref	Expression
	Assertion	f1ofvswap	$⊢ (F : A \underset{1-1 onto}{⟶} B \land X \in A \land Y \in A) \to (({F ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, F (Y)⟩, ⟨Y, F (X)⟩\}) : A \underset{1-1 onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		f1oi	$⊢ ({I ↾}_{(A ∖ \{X, Y\})}) : A ∖ \{X, Y\} \underset{1-1 onto}{⟶} A ∖ \{X, Y\}$
2		f1oprswap	$⊢ (X \in A \land Y \in A) \to \{⟨X, Y⟩, ⟨Y, X⟩\} : \{X, Y\} \underset{1-1 onto}{⟶} \{X, Y\}$
3		disjdifr	$⊢ (A ∖ \{X, Y\}) \cap \{X, Y\} = \emptyset$
4		f1oun	$⊢ ((({I ↾}_{(A ∖ \{X, Y\})}) : A ∖ \{X, Y\} \underset{1-1 onto}{⟶} A ∖ \{X, Y\} \land \{⟨X, Y⟩, ⟨Y, X⟩\} : \{X, Y\} \underset{1-1 onto}{⟶} \{X, Y\}) \land ((A ∖ \{X, Y\}) \cap \{X, Y\} = \emptyset \land (A ∖ \{X, Y\}) \cap \{X, Y\} = \emptyset)) \to (({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\}) : (A ∖ \{X, Y\}) \cup \{X, Y\} \underset{1-1 onto}{⟶} (A ∖ \{X, Y\}) \cup \{X, Y\}$
5	3 3 4	mpanr12	$⊢ (({I ↾}_{(A ∖ \{X, Y\})}) : A ∖ \{X, Y\} \underset{1-1 onto}{⟶} A ∖ \{X, Y\} \land \{⟨X, Y⟩, ⟨Y, X⟩\} : \{X, Y\} \underset{1-1 onto}{⟶} \{X, Y\}) \to (({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\}) : (A ∖ \{X, Y\}) \cup \{X, Y\} \underset{1-1 onto}{⟶} (A ∖ \{X, Y\}) \cup \{X, Y\}$
6	1 2 5	sylancr	$⊢ (X \in A \land Y \in A) \to (({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\}) : (A ∖ \{X, Y\}) \cup \{X, Y\} \underset{1-1 onto}{⟶} (A ∖ \{X, Y\}) \cup \{X, Y\}$
7		prssi	$⊢ (X \in A \land Y \in A) \to \{X, Y\} \subseteq A$
8		undifr	$⊢ \{X, Y\} \subseteq A \leftrightarrow (A ∖ \{X, Y\}) \cup \{X, Y\} = A$
9	7 8	sylib	$⊢ (X \in A \land Y \in A) \to (A ∖ \{X, Y\}) \cup \{X, Y\} = A$
10		f1oeq23	$⊢ ((A ∖ \{X, Y\}) \cup \{X, Y\} = A \land (A ∖ \{X, Y\}) \cup \{X, Y\} = A) \to ((({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\}) : (A ∖ \{X, Y\}) \cup \{X, Y\} \underset{1-1 onto}{⟶} (A ∖ \{X, Y\}) \cup \{X, Y\} \leftrightarrow (({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\}) : A \underset{1-1 onto}{⟶} A)$
11	9 9 10	syl2anc	$⊢ (X \in A \land Y \in A) \to ((({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\}) : (A ∖ \{X, Y\}) \cup \{X, Y\} \underset{1-1 onto}{⟶} (A ∖ \{X, Y\}) \cup \{X, Y\} \leftrightarrow (({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\}) : A \underset{1-1 onto}{⟶} A)$
12	6 11	mpbid	$⊢ (X \in A \land Y \in A) \to (({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\}) : A \underset{1-1 onto}{⟶} A$
13		f1oco	$⊢ (F : A \underset{1-1 onto}{⟶} B \land (({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\}) : A \underset{1-1 onto}{⟶} A) \to (F \circ (({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\})) : A \underset{1-1 onto}{⟶} B$
14	12 13	sylan2	$⊢ (F : A \underset{1-1 onto}{⟶} B \land (X \in A \land Y \in A)) \to (F \circ (({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\})) : A \underset{1-1 onto}{⟶} B$
15	14	3impb	$⊢ (F : A \underset{1-1 onto}{⟶} B \land X \in A \land Y \in A) \to (F \circ (({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\})) : A \underset{1-1 onto}{⟶} B$
16		f1ofn	$⊢ F : A \underset{1-1 onto}{⟶} B \to F Fn A$
17		coundi	$⊢ F \circ (({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\}) = (F \circ ({I ↾}_{(A ∖ \{X, Y\})})) \cup (F \circ \{⟨X, Y⟩, ⟨Y, X⟩\})$
18		fcoconst	$⊢ (F Fn A \land Y \in A) \to F \circ (\{X\} \times \{Y\}) = \{X\} \times \{F (Y)\}$
19	18	3adant2	$⊢ (F Fn A \land X \in A \land Y \in A) \to F \circ (\{X\} \times \{Y\}) = \{X\} \times \{F (Y)\}$
20		xpsng	$⊢ (X \in A \land Y \in A) \to \{X\} \times \{Y\} = \{⟨X, Y⟩\}$
21	20	coeq2d	$⊢ (X \in A \land Y \in A) \to F \circ (\{X\} \times \{Y\}) = F \circ \{⟨X, Y⟩\}$
22	21	3adant1	$⊢ (F Fn A \land X \in A \land Y \in A) \to F \circ (\{X\} \times \{Y\}) = F \circ \{⟨X, Y⟩\}$
23		fvex	$⊢ F (Y) \in V$
24		xpsng	$⊢ (X \in A \land F (Y) \in V) \to \{X\} \times \{F (Y)\} = \{⟨X, F (Y)⟩\}$
25	23 24	mpan2	$⊢ X \in A \to \{X\} \times \{F (Y)\} = \{⟨X, F (Y)⟩\}$
26	25	3ad2ant2	$⊢ (F Fn A \land X \in A \land Y \in A) \to \{X\} \times \{F (Y)\} = \{⟨X, F (Y)⟩\}$
27	19 22 26	3eqtr3d	$⊢ (F Fn A \land X \in A \land Y \in A) \to F \circ \{⟨X, Y⟩\} = \{⟨X, F (Y)⟩\}$
28		fcoconst	$⊢ (F Fn A \land X \in A) \to F \circ (\{Y\} \times \{X\}) = \{Y\} \times \{F (X)\}$
29	28	3adant3	$⊢ (F Fn A \land X \in A \land Y \in A) \to F \circ (\{Y\} \times \{X\}) = \{Y\} \times \{F (X)\}$
30		xpsng	$⊢ (Y \in A \land X \in A) \to \{Y\} \times \{X\} = \{⟨Y, X⟩\}$
31	30	coeq2d	$⊢ (Y \in A \land X \in A) \to F \circ (\{Y\} \times \{X\}) = F \circ \{⟨Y, X⟩\}$
32	31	ancoms	$⊢ (X \in A \land Y \in A) \to F \circ (\{Y\} \times \{X\}) = F \circ \{⟨Y, X⟩\}$
33	32	3adant1	$⊢ (F Fn A \land X \in A \land Y \in A) \to F \circ (\{Y\} \times \{X\}) = F \circ \{⟨Y, X⟩\}$
34		fvex	$⊢ F (X) \in V$
35		xpsng	$⊢ (Y \in A \land F (X) \in V) \to \{Y\} \times \{F (X)\} = \{⟨Y, F (X)⟩\}$
36	34 35	mpan2	$⊢ Y \in A \to \{Y\} \times \{F (X)\} = \{⟨Y, F (X)⟩\}$
37	36	3ad2ant3	$⊢ (F Fn A \land X \in A \land Y \in A) \to \{Y\} \times \{F (X)\} = \{⟨Y, F (X)⟩\}$
38	29 33 37	3eqtr3d	$⊢ (F Fn A \land X \in A \land Y \in A) \to F \circ \{⟨Y, X⟩\} = \{⟨Y, F (X)⟩\}$
39	27 38	uneq12d	$⊢ (F Fn A \land X \in A \land Y \in A) \to (F \circ \{⟨X, Y⟩\}) \cup (F \circ \{⟨Y, X⟩\}) = \{⟨X, F (Y)⟩\} \cup \{⟨Y, F (X)⟩\}$
40		df-pr	$⊢ \{⟨X, Y⟩, ⟨Y, X⟩\} = \{⟨X, Y⟩\} \cup \{⟨Y, X⟩\}$
41	40	coeq2i	$⊢ F \circ \{⟨X, Y⟩, ⟨Y, X⟩\} = F \circ (\{⟨X, Y⟩\} \cup \{⟨Y, X⟩\})$
42		coundi	$⊢ F \circ (\{⟨X, Y⟩\} \cup \{⟨Y, X⟩\}) = (F \circ \{⟨X, Y⟩\}) \cup (F \circ \{⟨Y, X⟩\})$
43	41 42	eqtri	$⊢ F \circ \{⟨X, Y⟩, ⟨Y, X⟩\} = (F \circ \{⟨X, Y⟩\}) \cup (F \circ \{⟨Y, X⟩\})$
44		df-pr	$⊢ \{⟨X, F (Y)⟩, ⟨Y, F (X)⟩\} = \{⟨X, F (Y)⟩\} \cup \{⟨Y, F (X)⟩\}$
45	39 43 44	3eqtr4g	$⊢ (F Fn A \land X \in A \land Y \in A) \to F \circ \{⟨X, Y⟩, ⟨Y, X⟩\} = \{⟨X, F (Y)⟩, ⟨Y, F (X)⟩\}$
46	45	uneq2d	$⊢ (F Fn A \land X \in A \land Y \in A) \to (F \circ ({I ↾}_{(A ∖ \{X, Y\})})) \cup (F \circ \{⟨X, Y⟩, ⟨Y, X⟩\}) = (F \circ ({I ↾}_{(A ∖ \{X, Y\})})) \cup \{⟨X, F (Y)⟩, ⟨Y, F (X)⟩\}$
47	17 46	eqtrid	$⊢ (F Fn A \land X \in A \land Y \in A) \to F \circ (({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\}) = (F \circ ({I ↾}_{(A ∖ \{X, Y\})})) \cup \{⟨X, F (Y)⟩, ⟨Y, F (X)⟩\}$
48		coires1	$⊢ F \circ ({I ↾}_{(A ∖ \{X, Y\})}) = {F ↾}_{(A ∖ \{X, Y\})}$
49	48	uneq1i	$⊢ (F \circ ({I ↾}_{(A ∖ \{X, Y\})})) \cup \{⟨X, F (Y)⟩, ⟨Y, F (X)⟩\} = ({F ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, F (Y)⟩, ⟨Y, F (X)⟩\}$
50	47 49	eqtrdi	$⊢ (F Fn A \land X \in A \land Y \in A) \to F \circ (({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\}) = ({F ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, F (Y)⟩, ⟨Y, F (X)⟩\}$
51	16 50	syl3an1	$⊢ (F : A \underset{1-1 onto}{⟶} B \land X \in A \land Y \in A) \to F \circ (({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\}) = ({F ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, F (Y)⟩, ⟨Y, F (X)⟩\}$
52	51	f1oeq1d	$⊢ (F : A \underset{1-1 onto}{⟶} B \land X \in A \land Y \in A) \to ((F \circ (({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\})) : A \underset{1-1 onto}{⟶} B \leftrightarrow (({F ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, F (Y)⟩, ⟨Y, F (X)⟩\}) : A \underset{1-1 onto}{⟶} B)$
53	15 52	mpbid	$⊢ (F : A \underset{1-1 onto}{⟶} B \land X \in A \land Y \in A) \to (({F ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, F (Y)⟩, ⟨Y, F (X)⟩\}) : A \underset{1-1 onto}{⟶} B$

Metamath Proof Explorer

Theorem f1ofvswap

Proof