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		undif	$⊢ \{X, Y\} \subseteq A \leftrightarrow \{X, Y\} \cup (A ∖ \{X, Y\}) = A$
9		uncom	$⊢ \{X, Y\} \cup (A ∖ \{X, Y\}) = (A ∖ \{X, Y\}) \cup \{X, Y\}$
10	9	eqeq1i	$⊢ \{X, Y\} \cup (A ∖ \{X, Y\}) = A \leftrightarrow (A ∖ \{X, Y\}) \cup \{X, Y\} = A$
11	8 10	bitri	$⊢ \{X, Y\} \subseteq A \leftrightarrow (A ∖ \{X, Y\}) \cup \{X, Y\} = A$
12	7 11	sylib	$⊢ (X \in A \land Y \in A) \to (A ∖ \{X, Y\}) \cup \{X, Y\} = A$
13		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)$
14	12 12 13	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)$
15	6 14	mpbid	$⊢ (X \in A \land Y \in A) \to (({I ↾}_{(A ∖ \{X, Y\})}) \cup \{⟨X, Y⟩, ⟨Y, X⟩\}) : A \underset{1-1 onto}{⟶} A$
16		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$
17	15 16	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$
18	17	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$
19		f1ofn	$⊢ F : A \underset{1-1 onto}{⟶} B \to F Fn A$
20		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⟩\})$
21		fcoconst	$⊢ (F Fn A \land Y \in A) \to F \circ (\{X\} \times \{Y\}) = \{X\} \times \{F (Y)\}$
22	21	3adant2	$⊢ (F Fn A \land X \in A \land Y \in A) \to F \circ (\{X\} \times \{Y\}) = \{X\} \times \{F (Y)\}$
23		xpsng	$⊢ (X \in A \land Y \in A) \to \{X\} \times \{Y\} = \{⟨X, Y⟩\}$
24	23	coeq2d	$⊢ (X \in A \land Y \in A) \to F \circ (\{X\} \times \{Y\}) = F \circ \{⟨X, Y⟩\}$
25	24	3adant1	$⊢ (F Fn A \land X \in A \land Y \in A) \to F \circ (\{X\} \times \{Y\}) = F \circ \{⟨X, Y⟩\}$
26		fvex	$⊢ F (Y) \in V$
27		xpsng	$⊢ (X \in A \land F (Y) \in V) \to \{X\} \times \{F (Y)\} = \{⟨X, F (Y)⟩\}$
28	26 27	mpan2	$⊢ X \in A \to \{X\} \times \{F (Y)\} = \{⟨X, F (Y)⟩\}$
29	28	3ad2ant2	$⊢ (F Fn A \land X \in A \land Y \in A) \to \{X\} \times \{F (Y)\} = \{⟨X, F (Y)⟩\}$
30	22 25 29	3eqtr3d	$⊢ (F Fn A \land X \in A \land Y \in A) \to F \circ \{⟨X, Y⟩\} = \{⟨X, F (Y)⟩\}$
31		fcoconst	$⊢ (F Fn A \land X \in A) \to F \circ (\{Y\} \times \{X\}) = \{Y\} \times \{F (X)\}$
32	31	3adant3	$⊢ (F Fn A \land X \in A \land Y \in A) \to F \circ (\{Y\} \times \{X\}) = \{Y\} \times \{F (X)\}$
33		xpsng	$⊢ (Y \in A \land X \in A) \to \{Y\} \times \{X\} = \{⟨Y, X⟩\}$
34	33	coeq2d	$⊢ (Y \in A \land X \in A) \to F \circ (\{Y\} \times \{X\}) = F \circ \{⟨Y, X⟩\}$
35	34	ancoms	$⊢ (X \in A \land Y \in A) \to F \circ (\{Y\} \times \{X\}) = F \circ \{⟨Y, X⟩\}$
36	35	3adant1	$⊢ (F Fn A \land X \in A \land Y \in A) \to F \circ (\{Y\} \times \{X\}) = F \circ \{⟨Y, X⟩\}$
37		fvex	$⊢ F (X) \in V$
38		xpsng	$⊢ (Y \in A \land F (X) \in V) \to \{Y\} \times \{F (X)\} = \{⟨Y, F (X)⟩\}$
39	37 38	mpan2	$⊢ Y \in A \to \{Y\} \times \{F (X)\} = \{⟨Y, F (X)⟩\}$
40	39	3ad2ant3	$⊢ (F Fn A \land X \in A \land Y \in A) \to \{Y\} \times \{F (X)\} = \{⟨Y, F (X)⟩\}$
41	32 36 40	3eqtr3d	$⊢ (F Fn A \land X \in A \land Y \in A) \to F \circ \{⟨Y, X⟩\} = \{⟨Y, F (X)⟩\}$
42	30 41	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)⟩\}$
43		df-pr	$⊢ \{⟨X, Y⟩, ⟨Y, X⟩\} = \{⟨X, Y⟩\} \cup \{⟨Y, X⟩\}$
44	43	coeq2i	$⊢ F \circ \{⟨X, Y⟩, ⟨Y, X⟩\} = F \circ (\{⟨X, Y⟩\} \cup \{⟨Y, X⟩\})$
45		coundi	$⊢ F \circ (\{⟨X, Y⟩\} \cup \{⟨Y, X⟩\}) = (F \circ \{⟨X, Y⟩\}) \cup (F \circ \{⟨Y, X⟩\})$
46	44 45	eqtri	$⊢ F \circ \{⟨X, Y⟩, ⟨Y, X⟩\} = (F \circ \{⟨X, Y⟩\}) \cup (F \circ \{⟨Y, X⟩\})$
47		df-pr	$⊢ \{⟨X, F (Y)⟩, ⟨Y, F (X)⟩\} = \{⟨X, F (Y)⟩\} \cup \{⟨Y, F (X)⟩\}$
48	42 46 47	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)⟩\}$
49	48	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)⟩\}$
50	20 49	syl5eq	$⊢ (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)⟩\}$
51		coires1	$⊢ F \circ ({I ↾}_{(A ∖ \{X, Y\})}) = {F ↾}_{(A ∖ \{X, Y\})}$
52	51	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)⟩\}$
53	50 52	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)⟩\}$
54	19 53	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)⟩\}$
55	54	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)$
56	18 55	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