subfacp1lem4

Description: Lemma for subfacp1 . The function F , which swaps 1 with M and leaves all other elements alone, is a bijection of order 2 , i.e. it is its own inverse. (Contributed by Mario Carneiro, 19-Jan-2015)

	Ref	Expression
Hypotheses	derang.d	$⊢ D = (x \in Fin ⟼ \|\{f \| (f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y)\}\|)$
	subfac.n	$⊢ S = (n \in ℕ_{0} ⟼ D ((1 \dots n)))$
	subfacp1lem.a	$⊢ A = \{f \| (f : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) f (y) \neq y)\}$
	subfacp1lem1.n	$⊢ φ \to N \in ℕ$
	subfacp1lem1.m	$⊢ φ \to M \in (2 \dots N + 1)$
	subfacp1lem1.x	$⊢ M \in V$
	subfacp1lem1.k	$⊢ K = (2 \dots N + 1) ∖ \{M\}$
	subfacp1lem5.b	$⊢ B = \{g \in A \| (g (1) = M \land g (M) \neq 1)\}$
	subfacp1lem5.f	$⊢ F = ({I ↾}_{K}) \cup \{⟨1, M⟩, ⟨M, 1⟩\}$
Assertion	subfacp1lem4	$⊢ φ \to F^{-1} = F$

Proof

Step	Hyp	Ref	Expression
1		derang.d	$⊢ D = (x \in Fin ⟼ \|\{f \| (f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y)\}\|)$
2		subfac.n	$⊢ S = (n \in ℕ_{0} ⟼ D ((1 \dots n)))$
3		subfacp1lem.a	$⊢ A = \{f \| (f : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) f (y) \neq y)\}$
4		subfacp1lem1.n	$⊢ φ \to N \in ℕ$
5		subfacp1lem1.m	$⊢ φ \to M \in (2 \dots N + 1)$
6		subfacp1lem1.x	$⊢ M \in V$
7		subfacp1lem1.k	$⊢ K = (2 \dots N + 1) ∖ \{M\}$
8		subfacp1lem5.b	$⊢ B = \{g \in A \| (g (1) = M \land g (M) \neq 1)\}$
9		subfacp1lem5.f	$⊢ F = ({I ↾}_{K}) \cup \{⟨1, M⟩, ⟨M, 1⟩\}$
10		f1oi	$⊢ ({I ↾}_{K}) : K \underset{1-1 onto}{⟶} K$
11	10	a1i	$⊢ φ \to ({I ↾}_{K}) : K \underset{1-1 onto}{⟶} K$
12	1 2 3 4 5 6 7 9 11	subfacp1lem2a	$⊢ φ \to (F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land F (1) = M \land F (M) = 1)$
13	12	simp1d	$⊢ φ \to F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
14		f1ocnv	$⊢ F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to F^{-1} : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
15		f1ofn	$⊢ F^{-1} : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to F^{-1} Fn (1 \dots N + 1)$
16	13 14 15	3syl	$⊢ φ \to F^{-1} Fn (1 \dots N + 1)$
17		f1ofn	$⊢ F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to F Fn (1 \dots N + 1)$
18	13 17	syl	$⊢ φ \to F Fn (1 \dots N + 1)$
19	1 2 3 4 5 6 7	subfacp1lem1	$⊢ φ \to (K \cap \{1, M\} = \emptyset \land K \cup \{1, M\} = (1 \dots N + 1) \land \|K\| = N - 1)$
20	19	simp2d	$⊢ φ \to K \cup \{1, M\} = (1 \dots N + 1)$
21	20	eleq2d	$⊢ φ \to (x \in (K \cup \{1, M\}) \leftrightarrow x \in (1 \dots N + 1))$
22	21	biimpar	$⊢ (φ \land x \in (1 \dots N + 1)) \to x \in (K \cup \{1, M\})$
23		elun	$⊢ x \in (K \cup \{1, M\}) \leftrightarrow (x \in K \lor x \in \{1, M\})$
24	22 23	sylib	$⊢ (φ \land x \in (1 \dots N + 1)) \to (x \in K \lor x \in \{1, M\})$
25	1 2 3 4 5 6 7 9 11	subfacp1lem2b	$⊢ (φ \land x \in K) \to F (x) = ({I ↾}_{K}) (x)$
26		fvresi	$⊢ x \in K \to ({I ↾}_{K}) (x) = x$
27	26	adantl	$⊢ (φ \land x \in K) \to ({I ↾}_{K}) (x) = x$
28	25 27	eqtrd	$⊢ (φ \land x \in K) \to F (x) = x$
29	28	fveq2d	$⊢ (φ \land x \in K) \to F (F (x)) = F (x)$
30	29 28	eqtrd	$⊢ (φ \land x \in K) \to F (F (x)) = x$
31		vex	$⊢ x \in V$
32	31	elpr	$⊢ x \in \{1, M\} \leftrightarrow (x = 1 \lor x = M)$
33	12	simp2d	$⊢ φ \to F (1) = M$
34	33	fveq2d	$⊢ φ \to F (F (1)) = F (M)$
35	12	simp3d	$⊢ φ \to F (M) = 1$
36	34 35	eqtrd	$⊢ φ \to F (F (1)) = 1$
37		2fveq3	$⊢ x = 1 \to F (F (x)) = F (F (1))$
38		id	$⊢ x = 1 \to x = 1$
39	37 38	eqeq12d	$⊢ x = 1 \to (F (F (x)) = x \leftrightarrow F (F (1)) = 1)$
40	36 39	syl5ibrcom	$⊢ φ \to (x = 1 \to F (F (x)) = x)$
41	35	fveq2d	$⊢ φ \to F (F (M)) = F (1)$
42	41 33	eqtrd	$⊢ φ \to F (F (M)) = M$
43		2fveq3	$⊢ x = M \to F (F (x)) = F (F (M))$
44		id	$⊢ x = M \to x = M$
45	43 44	eqeq12d	$⊢ x = M \to (F (F (x)) = x \leftrightarrow F (F (M)) = M)$
46	42 45	syl5ibrcom	$⊢ φ \to (x = M \to F (F (x)) = x)$
47	40 46	jaod	$⊢ φ \to ((x = 1 \lor x = M) \to F (F (x)) = x)$
48	47	imp	$⊢ (φ \land (x = 1 \lor x = M)) \to F (F (x)) = x$
49	32 48	sylan2b	$⊢ (φ \land x \in \{1, M\}) \to F (F (x)) = x$
50	30 49	jaodan	$⊢ (φ \land (x \in K \lor x \in \{1, M\})) \to F (F (x)) = x$
51	24 50	syldan	$⊢ (φ \land x \in (1 \dots N + 1)) \to F (F (x)) = x$
52	13	adantr	$⊢ (φ \land x \in (1 \dots N + 1)) \to F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
53		f1of	$⊢ F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to F : (1 \dots N + 1) ⟶ (1 \dots N + 1)$
54	13 53	syl	$⊢ φ \to F : (1 \dots N + 1) ⟶ (1 \dots N + 1)$
55	54	ffvelrnda	$⊢ (φ \land x \in (1 \dots N + 1)) \to F (x) \in (1 \dots N + 1)$
56		f1ocnvfv	$⊢ (F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land F (x) \in (1 \dots N + 1)) \to (F (F (x)) = x \to F^{-1} (x) = F (x))$
57	52 55 56	syl2anc	$⊢ (φ \land x \in (1 \dots N + 1)) \to (F (F (x)) = x \to F^{-1} (x) = F (x))$
58	51 57	mpd	$⊢ (φ \land x \in (1 \dots N + 1)) \to F^{-1} (x) = F (x)$
59	16 18 58	eqfnfvd	$⊢ φ \to F^{-1} = F$

Metamath Proof Explorer

Theorem subfacp1lem4

Proof