subfacp1lem5

Description: Lemma for subfacp1 . In subfacp1lem6 we cut up the set of all derangements on 1 ... ( N + 1 ) first according to the value at 1 , and then by whether or not ( f( f1 ) ) = 1 . In this lemma, we show that the subset of all N + 1 derangements with ( f( f1 ) ) =/= 1 for fixed M = ( f1 ) is in bijection with derangements of 2 ... ( N + 1 ) , because pre-composing with the function F swaps 1 and M and turns the function into a bijection with ( f1 ) = 1 and ( fx ) =/= x for all other x , so dropping the point at 1 yields a derangement on the N remaining points. (Contributed by Mario Carneiro, 23-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⟩\}$
	subfacp1lem5.c	$⊢ C = \{f \| (f : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1) \land \forall y \in (2 \dots N + 1) f (y) \neq y)\}$
Assertion	subfacp1lem5	$⊢ φ \to \|B\| = S (N)$

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		subfacp1lem5.c	$⊢ C = \{f \| (f : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1) \land \forall y \in (2 \dots N + 1) f (y) \neq y)\}$
11		fzfi	$⊢ (1 \dots N + 1) \in Fin$
12		deranglem	$⊢ (1 \dots N + 1) \in Fin \to \{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)\} \in Fin$
13	11 12	ax-mp	$⊢ \{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)\} \in Fin$
14	3 13	eqeltri	$⊢ A \in Fin$
15	8	ssrab3	$⊢ B \subseteq A$
16		ssfi	$⊢ (A \in Fin \land B \subseteq A) \to B \in Fin$
17	14 15 16	mp2an	$⊢ B \in Fin$
18	17	elexi	$⊢ B \in V$
19	18	a1i	$⊢ φ \to B \in V$
20		eqid	$⊢ (b \in B ⟼ {(F \circ b) ↾}_{(2 \dots N + 1)}) = (b \in B ⟼ {(F \circ b) ↾}_{(2 \dots N + 1)})$
21		f1oi	$⊢ ({I ↾}_{K}) : K \underset{1-1 onto}{⟶} K$
22	21	a1i	$⊢ φ \to ({I ↾}_{K}) : K \underset{1-1 onto}{⟶} K$
23	1 2 3 4 5 6 7 9 22	subfacp1lem2a	$⊢ φ \to (F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land F (1) = M \land F (M) = 1)$
24	23	simp1d	$⊢ φ \to F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
25		simpr	$⊢ (φ \land b \in B) \to b \in B$
26		fveq1	$⊢ g = b \to g (1) = b (1)$
27	26	eqeq1d	$⊢ g = b \to (g (1) = M \leftrightarrow b (1) = M)$
28		fveq1	$⊢ g = b \to g (M) = b (M)$
29	28	neeq1d	$⊢ g = b \to (g (M) \neq 1 \leftrightarrow b (M) \neq 1)$
30	27 29	anbi12d	$⊢ g = b \to ((g (1) = M \land g (M) \neq 1) \leftrightarrow (b (1) = M \land b (M) \neq 1))$
31	30 8	elrab2	$⊢ b \in B \leftrightarrow (b \in A \land (b (1) = M \land b (M) \neq 1))$
32	25 31	sylib	$⊢ (φ \land b \in B) \to (b \in A \land (b (1) = M \land b (M) \neq 1))$
33	32	simpld	$⊢ (φ \land b \in B) \to b \in A$
34		vex	$⊢ b \in V$
35		f1oeq1	$⊢ f = b \to (f : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \leftrightarrow b : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1))$
36		fveq1	$⊢ f = b \to f (y) = b (y)$
37	36	neeq1d	$⊢ f = b \to (f (y) \neq y \leftrightarrow b (y) \neq y)$
38	37	ralbidv	$⊢ f = b \to (\forall y \in (1 \dots N + 1) f (y) \neq y \leftrightarrow \forall y \in (1 \dots N + 1) b (y) \neq y)$
39	35 38	anbi12d	$⊢ f = b \to ((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) \leftrightarrow (b : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) b (y) \neq y))$
40	34 39 3	elab2	$⊢ b \in A \leftrightarrow (b : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) b (y) \neq y)$
41	33 40	sylib	$⊢ (φ \land b \in B) \to (b : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) b (y) \neq y)$
42	41	simpld	$⊢ (φ \land b \in B) \to b : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
43		f1oco	$⊢ (F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land b : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)) \to (F \circ b) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
44	24 42 43	syl2an2r	$⊢ (φ \land b \in B) \to (F \circ b) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
45		f1of1	$⊢ (F \circ b) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to (F \circ b) : (1 \dots N + 1) \underset{1-1}{⟶} (1 \dots N + 1)$
46		df-f1	$⊢ (F \circ b) : (1 \dots N + 1) \underset{1-1}{⟶} (1 \dots N + 1) \leftrightarrow ((F \circ b) : (1 \dots N + 1) ⟶ (1 \dots N + 1) \land Fun {(F \circ b)}^{-1})$
47	46	simprbi	$⊢ (F \circ b) : (1 \dots N + 1) \underset{1-1}{⟶} (1 \dots N + 1) \to Fun {(F \circ b)}^{-1}$
48	44 45 47	3syl	$⊢ (φ \land b \in B) \to Fun {(F \circ b)}^{-1}$
49		f1ofn	$⊢ (F \circ b) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to (F \circ b) Fn (1 \dots N + 1)$
50		fnresdm	$⊢ (F \circ b) Fn (1 \dots N + 1) \to {(F \circ b) ↾}_{(1 \dots N + 1)} = F \circ b$
51		f1oeq1	$⊢ {(F \circ b) ↾}_{(1 \dots N + 1)} = F \circ b \to (({(F \circ b) ↾}_{(1 \dots N + 1)}) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \leftrightarrow (F \circ b) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1))$
52	44 49 50 51	4syl	$⊢ (φ \land b \in B) \to (({(F \circ b) ↾}_{(1 \dots N + 1)}) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \leftrightarrow (F \circ b) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1))$
53	44 52	mpbird	$⊢ (φ \land b \in B) \to ({(F \circ b) ↾}_{(1 \dots N + 1)}) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
54		f1ofo	$⊢ ({(F \circ b) ↾}_{(1 \dots N + 1)}) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to ({(F \circ b) ↾}_{(1 \dots N + 1)}) : (1 \dots N + 1) \underset{onto}{⟶} (1 \dots N + 1)$
55	53 54	syl	$⊢ (φ \land b \in B) \to ({(F \circ b) ↾}_{(1 \dots N + 1)}) : (1 \dots N + 1) \underset{onto}{⟶} (1 \dots N + 1)$
56		1ex	$⊢ 1 \in V$
57	56 56	f1osn	$⊢ \{⟨1, 1⟩\} : \{1\} \underset{1-1 onto}{⟶} \{1\}$
58	44 49	syl	$⊢ (φ \land b \in B) \to (F \circ b) Fn (1 \dots N + 1)$
59	4	peano2nnd	$⊢ φ \to N + 1 \in ℕ$
60		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
61	59 60	eleqtrdi	$⊢ φ \to N + 1 \in ℤ_{\geq 1}$
62		eluzfz1	$⊢ N + 1 \in ℤ_{\geq 1} \to 1 \in (1 \dots N + 1)$
63	61 62	syl	$⊢ φ \to 1 \in (1 \dots N + 1)$
64	63	adantr	$⊢ (φ \land b \in B) \to 1 \in (1 \dots N + 1)$
65		fnressn	$⊢ ((F \circ b) Fn (1 \dots N + 1) \land 1 \in (1 \dots N + 1)) \to {(F \circ b) ↾}_{\{1\}} = \{⟨1, (F \circ b) (1)⟩\}$
66	58 64 65	syl2anc	$⊢ (φ \land b \in B) \to {(F \circ b) ↾}_{\{1\}} = \{⟨1, (F \circ b) (1)⟩\}$
67		f1of	$⊢ b : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to b : (1 \dots N + 1) ⟶ (1 \dots N + 1)$
68	42 67	syl	$⊢ (φ \land b \in B) \to b : (1 \dots N + 1) ⟶ (1 \dots N + 1)$
69	68 64	fvco3d	$⊢ (φ \land b \in B) \to (F \circ b) (1) = F (b (1))$
70	32	simprd	$⊢ (φ \land b \in B) \to (b (1) = M \land b (M) \neq 1)$
71	70	simpld	$⊢ (φ \land b \in B) \to b (1) = M$
72	71	fveq2d	$⊢ (φ \land b \in B) \to F (b (1)) = F (M)$
73	23	simp3d	$⊢ φ \to F (M) = 1$
74	73	adantr	$⊢ (φ \land b \in B) \to F (M) = 1$
75	69 72 74	3eqtrd	$⊢ (φ \land b \in B) \to (F \circ b) (1) = 1$
76	75	opeq2d	$⊢ (φ \land b \in B) \to ⟨1, (F \circ b) (1)⟩ = ⟨1, 1⟩$
77	76	sneqd	$⊢ (φ \land b \in B) \to \{⟨1, (F \circ b) (1)⟩\} = \{⟨1, 1⟩\}$
78	66 77	eqtrd	$⊢ (φ \land b \in B) \to {(F \circ b) ↾}_{\{1\}} = \{⟨1, 1⟩\}$
79		f1oeq1	$⊢ {(F \circ b) ↾}_{\{1\}} = \{⟨1, 1⟩\} \to (({(F \circ b) ↾}_{\{1\}}) : \{1\} \underset{1-1 onto}{⟶} \{1\} \leftrightarrow \{⟨1, 1⟩\} : \{1\} \underset{1-1 onto}{⟶} \{1\})$
80	78 79	syl	$⊢ (φ \land b \in B) \to (({(F \circ b) ↾}_{\{1\}}) : \{1\} \underset{1-1 onto}{⟶} \{1\} \leftrightarrow \{⟨1, 1⟩\} : \{1\} \underset{1-1 onto}{⟶} \{1\})$
81	57 80	mpbiri	$⊢ (φ \land b \in B) \to ({(F \circ b) ↾}_{\{1\}}) : \{1\} \underset{1-1 onto}{⟶} \{1\}$
82		f1ofo	$⊢ ({(F \circ b) ↾}_{\{1\}}) : \{1\} \underset{1-1 onto}{⟶} \{1\} \to ({(F \circ b) ↾}_{\{1\}}) : \{1\} \underset{onto}{⟶} \{1\}$
83	81 82	syl	$⊢ (φ \land b \in B) \to ({(F \circ b) ↾}_{\{1\}}) : \{1\} \underset{onto}{⟶} \{1\}$
84		resdif	$⊢ (Fun {(F \circ b)}^{-1} \land ({(F \circ b) ↾}_{(1 \dots N + 1)}) : (1 \dots N + 1) \underset{onto}{⟶} (1 \dots N + 1) \land ({(F \circ b) ↾}_{\{1\}}) : \{1\} \underset{onto}{⟶} \{1\}) \to ({(F \circ b) ↾}_{((1 \dots N + 1) ∖ \{1\})}) : (1 \dots N + 1) ∖ \{1\} \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1\}$
85	48 55 83 84	syl3anc	$⊢ (φ \land b \in B) \to ({(F \circ b) ↾}_{((1 \dots N + 1) ∖ \{1\})}) : (1 \dots N + 1) ∖ \{1\} \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1\}$
86		fzsplit	$⊢ 1 \in (1 \dots N + 1) \to (1 \dots N + 1) = (1 \dots 1) \cup (1 + 1 \dots N + 1)$
87	63 86	syl	$⊢ φ \to (1 \dots N + 1) = (1 \dots 1) \cup (1 + 1 \dots N + 1)$
88		1z	$⊢ 1 \in ℤ$
89		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
90	88 89	ax-mp	$⊢ (1 \dots 1) = \{1\}$
91		1p1e2	$⊢ 1 + 1 = 2$
92	91	oveq1i	$⊢ (1 + 1 \dots N + 1) = (2 \dots N + 1)$
93	90 92	uneq12i	$⊢ (1 \dots 1) \cup (1 + 1 \dots N + 1) = \{1\} \cup (2 \dots N + 1)$
94	87 93	eqtr2di	$⊢ φ \to \{1\} \cup (2 \dots N + 1) = (1 \dots N + 1)$
95	63	snssd	$⊢ φ \to \{1\} \subseteq (1 \dots N + 1)$
96		incom	$⊢ \{1\} \cap (2 \dots N + 1) = (2 \dots N + 1) \cap \{1\}$
97		1lt2	$⊢ 1 < 2$
98		1re	$⊢ 1 \in ℝ$
99		2re	$⊢ 2 \in ℝ$
100	98 99	ltnlei	$⊢ 1 < 2 \leftrightarrow \neg 2 \leq 1$
101	97 100	mpbi	$⊢ \neg 2 \leq 1$
102		elfzle1	$⊢ 1 \in (2 \dots N + 1) \to 2 \leq 1$
103	101 102	mto	$⊢ \neg 1 \in (2 \dots N + 1)$
104		disjsn	$⊢ (2 \dots N + 1) \cap \{1\} = \emptyset \leftrightarrow \neg 1 \in (2 \dots N + 1)$
105	103 104	mpbir	$⊢ (2 \dots N + 1) \cap \{1\} = \emptyset$
106	96 105	eqtri	$⊢ \{1\} \cap (2 \dots N + 1) = \emptyset$
107		uneqdifeq	$⊢ (\{1\} \subseteq (1 \dots N + 1) \land \{1\} \cap (2 \dots N + 1) = \emptyset) \to (\{1\} \cup (2 \dots N + 1) = (1 \dots N + 1) \leftrightarrow (1 \dots N + 1) ∖ \{1\} = (2 \dots N + 1))$
108	95 106 107	sylancl	$⊢ φ \to (\{1\} \cup (2 \dots N + 1) = (1 \dots N + 1) \leftrightarrow (1 \dots N + 1) ∖ \{1\} = (2 \dots N + 1))$
109	94 108	mpbid	$⊢ φ \to (1 \dots N + 1) ∖ \{1\} = (2 \dots N + 1)$
110	109	adantr	$⊢ (φ \land b \in B) \to (1 \dots N + 1) ∖ \{1\} = (2 \dots N + 1)$
111		reseq2	$⊢ (1 \dots N + 1) ∖ \{1\} = (2 \dots N + 1) \to {(F \circ b) ↾}_{((1 \dots N + 1) ∖ \{1\})} = {(F \circ b) ↾}_{(2 \dots N + 1)}$
112		f1oeq1	$⊢ {(F \circ b) ↾}_{((1 \dots N + 1) ∖ \{1\})} = {(F \circ b) ↾}_{(2 \dots N + 1)} \to (({(F \circ b) ↾}_{((1 \dots N + 1) ∖ \{1\})}) : (1 \dots N + 1) ∖ \{1\} \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1\} \leftrightarrow ({(F \circ b) ↾}_{(2 \dots N + 1)}) : (1 \dots N + 1) ∖ \{1\} \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1\})$
113	111 112	syl	$⊢ (1 \dots N + 1) ∖ \{1\} = (2 \dots N + 1) \to (({(F \circ b) ↾}_{((1 \dots N + 1) ∖ \{1\})}) : (1 \dots N + 1) ∖ \{1\} \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1\} \leftrightarrow ({(F \circ b) ↾}_{(2 \dots N + 1)}) : (1 \dots N + 1) ∖ \{1\} \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1\})$
114		f1oeq2	$⊢ (1 \dots N + 1) ∖ \{1\} = (2 \dots N + 1) \to (({(F \circ b) ↾}_{(2 \dots N + 1)}) : (1 \dots N + 1) ∖ \{1\} \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1\} \leftrightarrow ({(F \circ b) ↾}_{(2 \dots N + 1)}) : (2 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1\})$
115		f1oeq3	$⊢ (1 \dots N + 1) ∖ \{1\} = (2 \dots N + 1) \to (({(F \circ b) ↾}_{(2 \dots N + 1)}) : (2 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1\} \leftrightarrow ({(F \circ b) ↾}_{(2 \dots N + 1)}) : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1))$
116	113 114 115	3bitrd	$⊢ (1 \dots N + 1) ∖ \{1\} = (2 \dots N + 1) \to (({(F \circ b) ↾}_{((1 \dots N + 1) ∖ \{1\})}) : (1 \dots N + 1) ∖ \{1\} \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1\} \leftrightarrow ({(F \circ b) ↾}_{(2 \dots N + 1)}) : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1))$
117	110 116	syl	$⊢ (φ \land b \in B) \to (({(F \circ b) ↾}_{((1 \dots N + 1) ∖ \{1\})}) : (1 \dots N + 1) ∖ \{1\} \underset{1-1 onto}{⟶} (1 \dots N + 1) ∖ \{1\} \leftrightarrow ({(F \circ b) ↾}_{(2 \dots N + 1)}) : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1))$
118	85 117	mpbid	$⊢ (φ \land b \in B) \to ({(F \circ b) ↾}_{(2 \dots N + 1)}) : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1)$
119	68	adantr	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to b : (1 \dots N + 1) ⟶ (1 \dots N + 1)$
120		fzp1ss	$⊢ 1 \in ℤ \to (1 + 1 \dots N + 1) \subseteq (1 \dots N + 1)$
121	88 120	ax-mp	$⊢ (1 + 1 \dots N + 1) \subseteq (1 \dots N + 1)$
122	92 121	eqsstrri	$⊢ (2 \dots N + 1) \subseteq (1 \dots N + 1)$
123		simpr	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to y \in (2 \dots N + 1)$
124	122 123	sseldi	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to y \in (1 \dots N + 1)$
125	119 124	fvco3d	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to (F \circ b) (y) = F (b (y))$
126	1 2 3 4 5 6 7 8 9	subfacp1lem4	$⊢ φ \to F^{-1} = F$
127	126	fveq1d	$⊢ φ \to F^{-1} (y) = F (y)$
128	127	ad2antrr	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to F^{-1} (y) = F (y)$
129	70	simprd	$⊢ (φ \land b \in B) \to b (M) \neq 1$
130	129 74	neeqtrrd	$⊢ (φ \land b \in B) \to b (M) \neq F (M)$
131	130	adantr	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to b (M) \neq F (M)$
132		fveq2	$⊢ y = M \to b (y) = b (M)$
133		fveq2	$⊢ y = M \to F (y) = F (M)$
134	132 133	neeq12d	$⊢ y = M \to (b (y) \neq F (y) \leftrightarrow b (M) \neq F (M))$
135	131 134	syl5ibrcom	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to (y = M \to b (y) \neq F (y))$
136	122	sseli	$⊢ y \in (2 \dots N + 1) \to y \in (1 \dots N + 1)$
137	41	simprd	$⊢ (φ \land b \in B) \to \forall y \in (1 \dots N + 1) b (y) \neq y$
138	137	r19.21bi	$⊢ ((φ \land b \in B) \land y \in (1 \dots N + 1)) \to b (y) \neq y$
139	136 138	sylan2	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to b (y) \neq y$
140	139	adantrr	$⊢ ((φ \land b \in B) \land (y \in (2 \dots N + 1) \land y \neq M)) \to b (y) \neq y$
141	7	eleq2i	$⊢ y \in K \leftrightarrow y \in ((2 \dots N + 1) ∖ \{M\})$
142		eldifsn	$⊢ y \in ((2 \dots N + 1) ∖ \{M\}) \leftrightarrow (y \in (2 \dots N + 1) \land y \neq M)$
143	141 142	bitri	$⊢ y \in K \leftrightarrow (y \in (2 \dots N + 1) \land y \neq M)$
144	1 2 3 4 5 6 7 9 22	subfacp1lem2b	$⊢ (φ \land y \in K) \to F (y) = ({I ↾}_{K}) (y)$
145		fvresi	$⊢ y \in K \to ({I ↾}_{K}) (y) = y$
146	145	adantl	$⊢ (φ \land y \in K) \to ({I ↾}_{K}) (y) = y$
147	144 146	eqtrd	$⊢ (φ \land y \in K) \to F (y) = y$
148	143 147	sylan2br	$⊢ (φ \land (y \in (2 \dots N + 1) \land y \neq M)) \to F (y) = y$
149	148	adantlr	$⊢ ((φ \land b \in B) \land (y \in (2 \dots N + 1) \land y \neq M)) \to F (y) = y$
150	140 149	neeqtrrd	$⊢ ((φ \land b \in B) \land (y \in (2 \dots N + 1) \land y \neq M)) \to b (y) \neq F (y)$
151	150	expr	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to (y \neq M \to b (y) \neq F (y))$
152	135 151	pm2.61dne	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to b (y) \neq F (y)$
153	152	necomd	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to F (y) \neq b (y)$
154	128 153	eqnetrd	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to F^{-1} (y) \neq b (y)$
155	24	adantr	$⊢ (φ \land b \in B) \to F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
156		ffvelrn	$⊢ (b : (1 \dots N + 1) ⟶ (1 \dots N + 1) \land y \in (1 \dots N + 1)) \to b (y) \in (1 \dots N + 1)$
157	68 136 156	syl2an	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to b (y) \in (1 \dots N + 1)$
158		f1ocnvfv	$⊢ (F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land b (y) \in (1 \dots N + 1)) \to (F (b (y)) = y \to F^{-1} (y) = b (y))$
159	155 157 158	syl2an2r	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to (F (b (y)) = y \to F^{-1} (y) = b (y))$
160	159	necon3d	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to (F^{-1} (y) \neq b (y) \to F (b (y)) \neq y)$
161	154 160	mpd	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to F (b (y)) \neq y$
162	125 161	eqnetrd	$⊢ ((φ \land b \in B) \land y \in (2 \dots N + 1)) \to (F \circ b) (y) \neq y$
163	162	ralrimiva	$⊢ (φ \land b \in B) \to \forall y \in (2 \dots N + 1) (F \circ b) (y) \neq y$
164		f1of	$⊢ ({I ↾}_{K}) : K \underset{1-1 onto}{⟶} K \to ({I ↾}_{K}) : K ⟶ K$
165	21 164	ax-mp	$⊢ ({I ↾}_{K}) : K ⟶ K$
166		fzfi	$⊢ (2 \dots N + 1) \in Fin$
167		difexg	$⊢ (2 \dots N + 1) \in Fin \to (2 \dots N + 1) ∖ \{M\} \in V$
168	166 167	ax-mp	$⊢ (2 \dots N + 1) ∖ \{M\} \in V$
169	7 168	eqeltri	$⊢ K \in V$
170		fex	$⊢ (({I ↾}_{K}) : K ⟶ K \land K \in V) \to {I ↾}_{K} \in V$
171	165 169 170	mp2an	$⊢ {I ↾}_{K} \in V$
172		prex	$⊢ \{⟨1, M⟩, ⟨M, 1⟩\} \in V$
173	171 172	unex	$⊢ ({I ↾}_{K}) \cup \{⟨1, M⟩, ⟨M, 1⟩\} \in V$
174	9 173	eqeltri	$⊢ F \in V$
175	174 34	coex	$⊢ F \circ b \in V$
176	175	resex	$⊢ {(F \circ b) ↾}_{(2 \dots N + 1)} \in V$
177		f1oeq1	$⊢ f = {(F \circ b) ↾}_{(2 \dots N + 1)} \to (f : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1) \leftrightarrow ({(F \circ b) ↾}_{(2 \dots N + 1)}) : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1))$
178		fveq1	$⊢ f = {(F \circ b) ↾}_{(2 \dots N + 1)} \to f (y) = ({(F \circ b) ↾}_{(2 \dots N + 1)}) (y)$
179		fvres	$⊢ y \in (2 \dots N + 1) \to ({(F \circ b) ↾}_{(2 \dots N + 1)}) (y) = (F \circ b) (y)$
180	178 179	sylan9eq	$⊢ (f = {(F \circ b) ↾}_{(2 \dots N + 1)} \land y \in (2 \dots N + 1)) \to f (y) = (F \circ b) (y)$
181	180	neeq1d	$⊢ (f = {(F \circ b) ↾}_{(2 \dots N + 1)} \land y \in (2 \dots N + 1)) \to (f (y) \neq y \leftrightarrow (F \circ b) (y) \neq y)$
182	181	ralbidva	$⊢ f = {(F \circ b) ↾}_{(2 \dots N + 1)} \to (\forall y \in (2 \dots N + 1) f (y) \neq y \leftrightarrow \forall y \in (2 \dots N + 1) (F \circ b) (y) \neq y)$
183	177 182	anbi12d	$⊢ f = {(F \circ b) ↾}_{(2 \dots N + 1)} \to ((f : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1) \land \forall y \in (2 \dots N + 1) f (y) \neq y) \leftrightarrow (({(F \circ b) ↾}_{(2 \dots N + 1)}) : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1) \land \forall y \in (2 \dots N + 1) (F \circ b) (y) \neq y))$
184	176 183 10	elab2	$⊢ {(F \circ b) ↾}_{(2 \dots N + 1)} \in C \leftrightarrow (({(F \circ b) ↾}_{(2 \dots N + 1)}) : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1) \land \forall y \in (2 \dots N + 1) (F \circ b) (y) \neq y)$
185	118 163 184	sylanbrc	$⊢ (φ \land b \in B) \to {(F \circ b) ↾}_{(2 \dots N + 1)} \in C$
186		simpr	$⊢ (φ \land c \in C) \to c \in C$
187		vex	$⊢ c \in V$
188		f1oeq1	$⊢ f = c \to (f : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1) \leftrightarrow c : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1))$
189		fveq1	$⊢ f = c \to f (y) = c (y)$
190	189	neeq1d	$⊢ f = c \to (f (y) \neq y \leftrightarrow c (y) \neq y)$
191	190	ralbidv	$⊢ f = c \to (\forall y \in (2 \dots N + 1) f (y) \neq y \leftrightarrow \forall y \in (2 \dots N + 1) c (y) \neq y)$
192	188 191	anbi12d	$⊢ f = c \to ((f : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1) \land \forall y \in (2 \dots N + 1) f (y) \neq y) \leftrightarrow (c : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1) \land \forall y \in (2 \dots N + 1) c (y) \neq y))$
193	187 192 10	elab2	$⊢ c \in C \leftrightarrow (c : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1) \land \forall y \in (2 \dots N + 1) c (y) \neq y)$
194	186 193	sylib	$⊢ (φ \land c \in C) \to (c : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1) \land \forall y \in (2 \dots N + 1) c (y) \neq y)$
195	194	simpld	$⊢ (φ \land c \in C) \to c : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1)$
196		f1oun	$⊢ ((\{⟨1, 1⟩\} : \{1\} \underset{1-1 onto}{⟶} \{1\} \land c : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1)) \land (\{1\} \cap (2 \dots N + 1) = \emptyset \land \{1\} \cap (2 \dots N + 1) = \emptyset)) \to (\{⟨1, 1⟩\} \cup c) : \{1\} \cup (2 \dots N + 1) \underset{1-1 onto}{⟶} \{1\} \cup (2 \dots N + 1)$
197	106 106 196	mpanr12	$⊢ (\{⟨1, 1⟩\} : \{1\} \underset{1-1 onto}{⟶} \{1\} \land c : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1)) \to (\{⟨1, 1⟩\} \cup c) : \{1\} \cup (2 \dots N + 1) \underset{1-1 onto}{⟶} \{1\} \cup (2 \dots N + 1)$
198	57 195 197	sylancr	$⊢ (φ \land c \in C) \to (\{⟨1, 1⟩\} \cup c) : \{1\} \cup (2 \dots N + 1) \underset{1-1 onto}{⟶} \{1\} \cup (2 \dots N + 1)$
199		f1oeq2	$⊢ \{1\} \cup (2 \dots N + 1) = (1 \dots N + 1) \to ((\{⟨1, 1⟩\} \cup c) : \{1\} \cup (2 \dots N + 1) \underset{1-1 onto}{⟶} \{1\} \cup (2 \dots N + 1) \leftrightarrow (\{⟨1, 1⟩\} \cup c) : (1 \dots N + 1) \underset{1-1 onto}{⟶} \{1\} \cup (2 \dots N + 1))$
200		f1oeq3	$⊢ \{1\} \cup (2 \dots N + 1) = (1 \dots N + 1) \to ((\{⟨1, 1⟩\} \cup c) : (1 \dots N + 1) \underset{1-1 onto}{⟶} \{1\} \cup (2 \dots N + 1) \leftrightarrow (\{⟨1, 1⟩\} \cup c) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1))$
201	199 200	bitrd	$⊢ \{1\} \cup (2 \dots N + 1) = (1 \dots N + 1) \to ((\{⟨1, 1⟩\} \cup c) : \{1\} \cup (2 \dots N + 1) \underset{1-1 onto}{⟶} \{1\} \cup (2 \dots N + 1) \leftrightarrow (\{⟨1, 1⟩\} \cup c) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1))$
202	94 201	syl	$⊢ φ \to ((\{⟨1, 1⟩\} \cup c) : \{1\} \cup (2 \dots N + 1) \underset{1-1 onto}{⟶} \{1\} \cup (2 \dots N + 1) \leftrightarrow (\{⟨1, 1⟩\} \cup c) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1))$
203	202	biimpa	$⊢ (φ \land (\{⟨1, 1⟩\} \cup c) : \{1\} \cup (2 \dots N + 1) \underset{1-1 onto}{⟶} \{1\} \cup (2 \dots N + 1)) \to (\{⟨1, 1⟩\} \cup c) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
204	198 203	syldan	$⊢ (φ \land c \in C) \to (\{⟨1, 1⟩\} \cup c) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
205		f1oco	$⊢ (F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land (\{⟨1, 1⟩\} \cup c) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)) \to (F \circ (\{⟨1, 1⟩\} \cup c)) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
206	24 204 205	syl2an2r	$⊢ (φ \land c \in C) \to (F \circ (\{⟨1, 1⟩\} \cup c)) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
207		f1of	$⊢ (\{⟨1, 1⟩\} \cup c) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to (\{⟨1, 1⟩\} \cup c) : (1 \dots N + 1) ⟶ (1 \dots N + 1)$
208	204 207	syl	$⊢ (φ \land c \in C) \to (\{⟨1, 1⟩\} \cup c) : (1 \dots N + 1) ⟶ (1 \dots N + 1)$
209		fvco3	$⊢ ((\{⟨1, 1⟩\} \cup c) : (1 \dots N + 1) ⟶ (1 \dots N + 1) \land y \in (1 \dots N + 1)) \to (F \circ (\{⟨1, 1⟩\} \cup c)) (y) = F ((\{⟨1, 1⟩\} \cup c) (y))$
210	208 209	sylan	$⊢ ((φ \land c \in C) \land y \in (1 \dots N + 1)) \to (F \circ (\{⟨1, 1⟩\} \cup c)) (y) = F ((\{⟨1, 1⟩\} \cup c) (y))$
211	127	ad2antrr	$⊢ ((φ \land c \in C) \land y \in (1 \dots N + 1)) \to F^{-1} (y) = F (y)$
212		simpr	$⊢ ((φ \land c \in C) \land y \in (1 \dots N + 1)) \to y \in (1 \dots N + 1)$
213	94	ad2antrr	$⊢ ((φ \land c \in C) \land y \in (1 \dots N + 1)) \to \{1\} \cup (2 \dots N + 1) = (1 \dots N + 1)$
214	212 213	eleqtrrd	$⊢ ((φ \land c \in C) \land y \in (1 \dots N + 1)) \to y \in (\{1\} \cup (2 \dots N + 1))$
215		elun	$⊢ y \in (\{1\} \cup (2 \dots N + 1)) \leftrightarrow (y \in \{1\} \lor y \in (2 \dots N + 1))$
216	214 215	sylib	$⊢ ((φ \land c \in C) \land y \in (1 \dots N + 1)) \to (y \in \{1\} \lor y \in (2 \dots N + 1))$
217		nelne2	$⊢ (M \in (2 \dots N + 1) \land \neg 1 \in (2 \dots N + 1)) \to M \neq 1$
218	5 103 217	sylancl	$⊢ φ \to M \neq 1$
219	218	adantr	$⊢ (φ \land c \in C) \to M \neq 1$
220	23	simp2d	$⊢ φ \to F (1) = M$
221	220	adantr	$⊢ (φ \land c \in C) \to F (1) = M$
222		f1ofun	$⊢ (\{⟨1, 1⟩\} \cup c) : \{1\} \cup (2 \dots N + 1) \underset{1-1 onto}{⟶} \{1\} \cup (2 \dots N + 1) \to Fun (\{⟨1, 1⟩\} \cup c)$
223	198 222	syl	$⊢ (φ \land c \in C) \to Fun (\{⟨1, 1⟩\} \cup c)$
224		ssun1	$⊢ \{⟨1, 1⟩\} \subseteq \{⟨1, 1⟩\} \cup c$
225	56	snid	$⊢ 1 \in \{1\}$
226	56	dmsnop	$⊢ dom \{⟨1, 1⟩\} = \{1\}$
227	225 226	eleqtrri	$⊢ 1 \in dom \{⟨1, 1⟩\}$
228		funssfv	$⊢ (Fun (\{⟨1, 1⟩\} \cup c) \land \{⟨1, 1⟩\} \subseteq \{⟨1, 1⟩\} \cup c \land 1 \in dom \{⟨1, 1⟩\}) \to (\{⟨1, 1⟩\} \cup c) (1) = \{⟨1, 1⟩\} (1)$
229	224 227 228	mp3an23	$⊢ Fun (\{⟨1, 1⟩\} \cup c) \to (\{⟨1, 1⟩\} \cup c) (1) = \{⟨1, 1⟩\} (1)$
230	223 229	syl	$⊢ (φ \land c \in C) \to (\{⟨1, 1⟩\} \cup c) (1) = \{⟨1, 1⟩\} (1)$
231	56 56	fvsn	$⊢ \{⟨1, 1⟩\} (1) = 1$
232	230 231	eqtrdi	$⊢ (φ \land c \in C) \to (\{⟨1, 1⟩\} \cup c) (1) = 1$
233	219 221 232	3netr4d	$⊢ (φ \land c \in C) \to F (1) \neq (\{⟨1, 1⟩\} \cup c) (1)$
234		elsni	$⊢ y \in \{1\} \to y = 1$
235	234	fveq2d	$⊢ y \in \{1\} \to F (y) = F (1)$
236	234	fveq2d	$⊢ y \in \{1\} \to (\{⟨1, 1⟩\} \cup c) (y) = (\{⟨1, 1⟩\} \cup c) (1)$
237	235 236	neeq12d	$⊢ y \in \{1\} \to (F (y) \neq (\{⟨1, 1⟩\} \cup c) (y) \leftrightarrow F (1) \neq (\{⟨1, 1⟩\} \cup c) (1))$
238	233 237	syl5ibrcom	$⊢ (φ \land c \in C) \to (y \in \{1\} \to F (y) \neq (\{⟨1, 1⟩\} \cup c) (y))$
239	238	imp	$⊢ ((φ \land c \in C) \land y \in \{1\}) \to F (y) \neq (\{⟨1, 1⟩\} \cup c) (y)$
240	223	adantr	$⊢ ((φ \land c \in C) \land y \in (2 \dots N + 1)) \to Fun (\{⟨1, 1⟩\} \cup c)$
241		ssun2	$⊢ c \subseteq \{⟨1, 1⟩\} \cup c$
242	241	a1i	$⊢ ((φ \land c \in C) \land y \in (2 \dots N + 1)) \to c \subseteq \{⟨1, 1⟩\} \cup c$
243		f1odm	$⊢ c : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1) \to dom c = (2 \dots N + 1)$
244	195 243	syl	$⊢ (φ \land c \in C) \to dom c = (2 \dots N + 1)$
245	244	eleq2d	$⊢ (φ \land c \in C) \to (y \in dom c \leftrightarrow y \in (2 \dots N + 1))$
246	245	biimpar	$⊢ ((φ \land c \in C) \land y \in (2 \dots N + 1)) \to y \in dom c$
247		funssfv	$⊢ (Fun (\{⟨1, 1⟩\} \cup c) \land c \subseteq \{⟨1, 1⟩\} \cup c \land y \in dom c) \to (\{⟨1, 1⟩\} \cup c) (y) = c (y)$
248	240 242 246 247	syl3anc	$⊢ ((φ \land c \in C) \land y \in (2 \dots N + 1)) \to (\{⟨1, 1⟩\} \cup c) (y) = c (y)$
249		f1of	$⊢ c : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1) \to c : (2 \dots N + 1) ⟶ (2 \dots N + 1)$
250	195 249	syl	$⊢ (φ \land c \in C) \to c : (2 \dots N + 1) ⟶ (2 \dots N + 1)$
251	5	adantr	$⊢ (φ \land c \in C) \to M \in (2 \dots N + 1)$
252	250 251	ffvelrnd	$⊢ (φ \land c \in C) \to c (M) \in (2 \dots N + 1)$
253		nelne2	$⊢ (c (M) \in (2 \dots N + 1) \land \neg 1 \in (2 \dots N + 1)) \to c (M) \neq 1$
254	252 103 253	sylancl	$⊢ (φ \land c \in C) \to c (M) \neq 1$
255	254	adantr	$⊢ ((φ \land c \in C) \land y \in (2 \dots N + 1)) \to c (M) \neq 1$
256	73	ad2antrr	$⊢ ((φ \land c \in C) \land y \in (2 \dots N + 1)) \to F (M) = 1$
257	255 256	neeqtrrd	$⊢ ((φ \land c \in C) \land y \in (2 \dots N + 1)) \to c (M) \neq F (M)$
258		fveq2	$⊢ y = M \to c (y) = c (M)$
259	258 133	neeq12d	$⊢ y = M \to (c (y) \neq F (y) \leftrightarrow c (M) \neq F (M))$
260	257 259	syl5ibrcom	$⊢ ((φ \land c \in C) \land y \in (2 \dots N + 1)) \to (y = M \to c (y) \neq F (y))$
261	194	simprd	$⊢ (φ \land c \in C) \to \forall y \in (2 \dots N + 1) c (y) \neq y$
262	261	r19.21bi	$⊢ ((φ \land c \in C) \land y \in (2 \dots N + 1)) \to c (y) \neq y$
263	262	adantrr	$⊢ ((φ \land c \in C) \land (y \in (2 \dots N + 1) \land y \neq M)) \to c (y) \neq y$
264	148	adantlr	$⊢ ((φ \land c \in C) \land (y \in (2 \dots N + 1) \land y \neq M)) \to F (y) = y$
265	263 264	neeqtrrd	$⊢ ((φ \land c \in C) \land (y \in (2 \dots N + 1) \land y \neq M)) \to c (y) \neq F (y)$
266	265	expr	$⊢ ((φ \land c \in C) \land y \in (2 \dots N + 1)) \to (y \neq M \to c (y) \neq F (y))$
267	260 266	pm2.61dne	$⊢ ((φ \land c \in C) \land y \in (2 \dots N + 1)) \to c (y) \neq F (y)$
268	248 267	eqnetrd	$⊢ ((φ \land c \in C) \land y \in (2 \dots N + 1)) \to (\{⟨1, 1⟩\} \cup c) (y) \neq F (y)$
269	268	necomd	$⊢ ((φ \land c \in C) \land y \in (2 \dots N + 1)) \to F (y) \neq (\{⟨1, 1⟩\} \cup c) (y)$
270	239 269	jaodan	$⊢ ((φ \land c \in C) \land (y \in \{1\} \lor y \in (2 \dots N + 1))) \to F (y) \neq (\{⟨1, 1⟩\} \cup c) (y)$
271	216 270	syldan	$⊢ ((φ \land c \in C) \land y \in (1 \dots N + 1)) \to F (y) \neq (\{⟨1, 1⟩\} \cup c) (y)$
272	211 271	eqnetrd	$⊢ ((φ \land c \in C) \land y \in (1 \dots N + 1)) \to F^{-1} (y) \neq (\{⟨1, 1⟩\} \cup c) (y)$
273	24	adantr	$⊢ (φ \land c \in C) \to F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
274	208	ffvelrnda	$⊢ ((φ \land c \in C) \land y \in (1 \dots N + 1)) \to (\{⟨1, 1⟩\} \cup c) (y) \in (1 \dots N + 1)$
275		f1ocnvfv	$⊢ (F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land (\{⟨1, 1⟩\} \cup c) (y) \in (1 \dots N + 1)) \to (F ((\{⟨1, 1⟩\} \cup c) (y)) = y \to F^{-1} (y) = (\{⟨1, 1⟩\} \cup c) (y))$
276	273 274 275	syl2an2r	$⊢ ((φ \land c \in C) \land y \in (1 \dots N + 1)) \to (F ((\{⟨1, 1⟩\} \cup c) (y)) = y \to F^{-1} (y) = (\{⟨1, 1⟩\} \cup c) (y))$
277	276	necon3d	$⊢ ((φ \land c \in C) \land y \in (1 \dots N + 1)) \to (F^{-1} (y) \neq (\{⟨1, 1⟩\} \cup c) (y) \to F ((\{⟨1, 1⟩\} \cup c) (y)) \neq y)$
278	272 277	mpd	$⊢ ((φ \land c \in C) \land y \in (1 \dots N + 1)) \to F ((\{⟨1, 1⟩\} \cup c) (y)) \neq y$
279	210 278	eqnetrd	$⊢ ((φ \land c \in C) \land y \in (1 \dots N + 1)) \to (F \circ (\{⟨1, 1⟩\} \cup c)) (y) \neq y$
280	279	ralrimiva	$⊢ (φ \land c \in C) \to \forall y \in (1 \dots N + 1) (F \circ (\{⟨1, 1⟩\} \cup c)) (y) \neq y$
281		snex	$⊢ \{⟨1, 1⟩\} \in V$
282	281 187	unex	$⊢ \{⟨1, 1⟩\} \cup c \in V$
283	174 282	coex	$⊢ F \circ (\{⟨1, 1⟩\} \cup c) \in V$
284		f1oeq1	$⊢ f = F \circ (\{⟨1, 1⟩\} \cup c) \to (f : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \leftrightarrow (F \circ (\{⟨1, 1⟩\} \cup c)) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1))$
285		fveq1	$⊢ f = F \circ (\{⟨1, 1⟩\} \cup c) \to f (y) = (F \circ (\{⟨1, 1⟩\} \cup c)) (y)$
286	285	neeq1d	$⊢ f = F \circ (\{⟨1, 1⟩\} \cup c) \to (f (y) \neq y \leftrightarrow (F \circ (\{⟨1, 1⟩\} \cup c)) (y) \neq y)$
287	286	ralbidv	$⊢ f = F \circ (\{⟨1, 1⟩\} \cup c) \to (\forall y \in (1 \dots N + 1) f (y) \neq y \leftrightarrow \forall y \in (1 \dots N + 1) (F \circ (\{⟨1, 1⟩\} \cup c)) (y) \neq y)$
288	284 287	anbi12d	$⊢ f = F \circ (\{⟨1, 1⟩\} \cup c) \to ((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) \leftrightarrow ((F \circ (\{⟨1, 1⟩\} \cup c)) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) (F \circ (\{⟨1, 1⟩\} \cup c)) (y) \neq y))$
289	283 288 3	elab2	$⊢ F \circ (\{⟨1, 1⟩\} \cup c) \in A \leftrightarrow ((F \circ (\{⟨1, 1⟩\} \cup c)) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) (F \circ (\{⟨1, 1⟩\} \cup c)) (y) \neq y)$
290	206 280 289	sylanbrc	$⊢ (φ \land c \in C) \to F \circ (\{⟨1, 1⟩\} \cup c) \in A$
291	63	adantr	$⊢ (φ \land c \in C) \to 1 \in (1 \dots N + 1)$
292	208 291	fvco3d	$⊢ (φ \land c \in C) \to (F \circ (\{⟨1, 1⟩\} \cup c)) (1) = F ((\{⟨1, 1⟩\} \cup c) (1))$
293	232	fveq2d	$⊢ (φ \land c \in C) \to F ((\{⟨1, 1⟩\} \cup c) (1)) = F (1)$
294	292 293 221	3eqtrd	$⊢ (φ \land c \in C) \to (F \circ (\{⟨1, 1⟩\} \cup c)) (1) = M$
295	122 5	sseldi	$⊢ φ \to M \in (1 \dots N + 1)$
296	295	adantr	$⊢ (φ \land c \in C) \to M \in (1 \dots N + 1)$
297	208 296	fvco3d	$⊢ (φ \land c \in C) \to (F \circ (\{⟨1, 1⟩\} \cup c)) (M) = F ((\{⟨1, 1⟩\} \cup c) (M))$
298	241	a1i	$⊢ (φ \land c \in C) \to c \subseteq \{⟨1, 1⟩\} \cup c$
299	251 244	eleqtrrd	$⊢ (φ \land c \in C) \to M \in dom c$
300		funssfv	$⊢ (Fun (\{⟨1, 1⟩\} \cup c) \land c \subseteq \{⟨1, 1⟩\} \cup c \land M \in dom c) \to (\{⟨1, 1⟩\} \cup c) (M) = c (M)$
301	223 298 299 300	syl3anc	$⊢ (φ \land c \in C) \to (\{⟨1, 1⟩\} \cup c) (M) = c (M)$
302	301	fveq2d	$⊢ (φ \land c \in C) \to F ((\{⟨1, 1⟩\} \cup c) (M)) = F (c (M))$
303	297 302	eqtrd	$⊢ (φ \land c \in C) \to (F \circ (\{⟨1, 1⟩\} \cup c)) (M) = F (c (M))$
304	126	fveq1d	$⊢ φ \to F^{-1} (1) = F (1)$
305	304 220	eqtrd	$⊢ φ \to F^{-1} (1) = M$
306	305	adantr	$⊢ (φ \land c \in C) \to F^{-1} (1) = M$
307		id	$⊢ y = M \to y = M$
308	258 307	neeq12d	$⊢ y = M \to (c (y) \neq y \leftrightarrow c (M) \neq M)$
309	308 261 251	rspcdva	$⊢ (φ \land c \in C) \to c (M) \neq M$
310	309	necomd	$⊢ (φ \land c \in C) \to M \neq c (M)$
311	306 310	eqnetrd	$⊢ (φ \land c \in C) \to F^{-1} (1) \neq c (M)$
312	122 252	sseldi	$⊢ (φ \land c \in C) \to c (M) \in (1 \dots N + 1)$
313		f1ocnvfv	$⊢ (F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land c (M) \in (1 \dots N + 1)) \to (F (c (M)) = 1 \to F^{-1} (1) = c (M))$
314	24 312 313	syl2an2r	$⊢ (φ \land c \in C) \to (F (c (M)) = 1 \to F^{-1} (1) = c (M))$
315	314	necon3d	$⊢ (φ \land c \in C) \to (F^{-1} (1) \neq c (M) \to F (c (M)) \neq 1)$
316	311 315	mpd	$⊢ (φ \land c \in C) \to F (c (M)) \neq 1$
317	303 316	eqnetrd	$⊢ (φ \land c \in C) \to (F \circ (\{⟨1, 1⟩\} \cup c)) (M) \neq 1$
318	294 317	jca	$⊢ (φ \land c \in C) \to ((F \circ (\{⟨1, 1⟩\} \cup c)) (1) = M \land (F \circ (\{⟨1, 1⟩\} \cup c)) (M) \neq 1)$
319		fveq1	$⊢ g = F \circ (\{⟨1, 1⟩\} \cup c) \to g (1) = (F \circ (\{⟨1, 1⟩\} \cup c)) (1)$
320	319	eqeq1d	$⊢ g = F \circ (\{⟨1, 1⟩\} \cup c) \to (g (1) = M \leftrightarrow (F \circ (\{⟨1, 1⟩\} \cup c)) (1) = M)$
321		fveq1	$⊢ g = F \circ (\{⟨1, 1⟩\} \cup c) \to g (M) = (F \circ (\{⟨1, 1⟩\} \cup c)) (M)$
322	321	neeq1d	$⊢ g = F \circ (\{⟨1, 1⟩\} \cup c) \to (g (M) \neq 1 \leftrightarrow (F \circ (\{⟨1, 1⟩\} \cup c)) (M) \neq 1)$
323	320 322	anbi12d	$⊢ g = F \circ (\{⟨1, 1⟩\} \cup c) \to ((g (1) = M \land g (M) \neq 1) \leftrightarrow ((F \circ (\{⟨1, 1⟩\} \cup c)) (1) = M \land (F \circ (\{⟨1, 1⟩\} \cup c)) (M) \neq 1))$
324	323 8	elrab2	$⊢ F \circ (\{⟨1, 1⟩\} \cup c) \in B \leftrightarrow (F \circ (\{⟨1, 1⟩\} \cup c) \in A \land ((F \circ (\{⟨1, 1⟩\} \cup c)) (1) = M \land (F \circ (\{⟨1, 1⟩\} \cup c)) (M) \neq 1))$
325	290 318 324	sylanbrc	$⊢ (φ \land c \in C) \to F \circ (\{⟨1, 1⟩\} \cup c) \in B$
326	24	adantr	$⊢ (φ \land (b \in B \land c \in C)) \to F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
327		f1of1	$⊢ F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to F : (1 \dots N + 1) \underset{1-1}{⟶} (1 \dots N + 1)$
328	326 327	syl	$⊢ (φ \land (b \in B \land c \in C)) \to F : (1 \dots N + 1) \underset{1-1}{⟶} (1 \dots N + 1)$
329		f1of	$⊢ F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to F : (1 \dots N + 1) ⟶ (1 \dots N + 1)$
330	326 329	syl	$⊢ (φ \land (b \in B \land c \in C)) \to F : (1 \dots N + 1) ⟶ (1 \dots N + 1)$
331	68	adantrr	$⊢ (φ \land (b \in B \land c \in C)) \to b : (1 \dots N + 1) ⟶ (1 \dots N + 1)$
332	330 331	fcod	$⊢ (φ \land (b \in B \land c \in C)) \to (F \circ b) : (1 \dots N + 1) ⟶ (1 \dots N + 1)$
333	208	adantrl	$⊢ (φ \land (b \in B \land c \in C)) \to (\{⟨1, 1⟩\} \cup c) : (1 \dots N + 1) ⟶ (1 \dots N + 1)$
334		cocan1	$⊢ (F : (1 \dots N + 1) \underset{1-1}{⟶} (1 \dots N + 1) \land (F \circ b) : (1 \dots N + 1) ⟶ (1 \dots N + 1) \land (\{⟨1, 1⟩\} \cup c) : (1 \dots N + 1) ⟶ (1 \dots N + 1)) \to (F \circ (F \circ b) = F \circ (\{⟨1, 1⟩\} \cup c) \leftrightarrow F \circ b = \{⟨1, 1⟩\} \cup c)$
335	328 332 333 334	syl3anc	$⊢ (φ \land (b \in B \land c \in C)) \to (F \circ (F \circ b) = F \circ (\{⟨1, 1⟩\} \cup c) \leftrightarrow F \circ b = \{⟨1, 1⟩\} \cup c)$
336		coass	$⊢ (F \circ F) \circ b = F \circ (F \circ b)$
337	126	coeq1d	$⊢ φ \to F^{-1} \circ F = F \circ F$
338		f1ococnv1	$⊢ F : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to F^{-1} \circ F = {I ↾}_{(1 \dots N + 1)}$
339	24 338	syl	$⊢ φ \to F^{-1} \circ F = {I ↾}_{(1 \dots N + 1)}$
340	337 339	eqtr3d	$⊢ φ \to F \circ F = {I ↾}_{(1 \dots N + 1)}$
341	340	adantr	$⊢ (φ \land (b \in B \land c \in C)) \to F \circ F = {I ↾}_{(1 \dots N + 1)}$
342	341	coeq1d	$⊢ (φ \land (b \in B \land c \in C)) \to (F \circ F) \circ b = ({I ↾}_{(1 \dots N + 1)}) \circ b$
343		fcoi2	$⊢ b : (1 \dots N + 1) ⟶ (1 \dots N + 1) \to ({I ↾}_{(1 \dots N + 1)}) \circ b = b$
344	331 343	syl	$⊢ (φ \land (b \in B \land c \in C)) \to ({I ↾}_{(1 \dots N + 1)}) \circ b = b$
345	342 344	eqtrd	$⊢ (φ \land (b \in B \land c \in C)) \to (F \circ F) \circ b = b$
346	336 345	syl5eqr	$⊢ (φ \land (b \in B \land c \in C)) \to F \circ (F \circ b) = b$
347	346	eqeq1d	$⊢ (φ \land (b \in B \land c \in C)) \to (F \circ (F \circ b) = F \circ (\{⟨1, 1⟩\} \cup c) \leftrightarrow b = F \circ (\{⟨1, 1⟩\} \cup c))$
348	75	adantrr	$⊢ (φ \land (b \in B \land c \in C)) \to (F \circ b) (1) = 1$
349	232	adantrl	$⊢ (φ \land (b \in B \land c \in C)) \to (\{⟨1, 1⟩\} \cup c) (1) = 1$
350	348 349	eqtr4d	$⊢ (φ \land (b \in B \land c \in C)) \to (F \circ b) (1) = (\{⟨1, 1⟩\} \cup c) (1)$
351		fveq2	$⊢ y = 1 \to (F \circ b) (y) = (F \circ b) (1)$
352		fveq2	$⊢ y = 1 \to (\{⟨1, 1⟩\} \cup c) (y) = (\{⟨1, 1⟩\} \cup c) (1)$
353	351 352	eqeq12d	$⊢ y = 1 \to ((F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y) \leftrightarrow (F \circ b) (1) = (\{⟨1, 1⟩\} \cup c) (1))$
354	56 353	ralsn	$⊢ \forall y \in \{1\} (F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y) \leftrightarrow (F \circ b) (1) = (\{⟨1, 1⟩\} \cup c) (1)$
355	350 354	sylibr	$⊢ (φ \land (b \in B \land c \in C)) \to \forall y \in \{1\} (F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y)$
356	355	biantrurd	$⊢ (φ \land (b \in B \land c \in C)) \to (\forall y \in (2 \dots N + 1) (F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y) \leftrightarrow (\forall y \in \{1\} (F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y) \land \forall y \in (2 \dots N + 1) (F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y)))$
357		ralunb	$⊢ \forall y \in (\{1\} \cup (2 \dots N + 1)) (F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y) \leftrightarrow (\forall y \in \{1\} (F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y) \land \forall y \in (2 \dots N + 1) (F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y))$
358	356 357	bitr4di	$⊢ (φ \land (b \in B \land c \in C)) \to (\forall y \in (2 \dots N + 1) (F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y) \leftrightarrow \forall y \in (\{1\} \cup (2 \dots N + 1)) (F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y))$
359	179	adantl	$⊢ ((φ \land (b \in B \land c \in C)) \land y \in (2 \dots N + 1)) \to ({(F \circ b) ↾}_{(2 \dots N + 1)}) (y) = (F \circ b) (y)$
360	359	eqcomd	$⊢ ((φ \land (b \in B \land c \in C)) \land y \in (2 \dots N + 1)) \to (F \circ b) (y) = ({(F \circ b) ↾}_{(2 \dots N + 1)}) (y)$
361	248	adantlrl	$⊢ ((φ \land (b \in B \land c \in C)) \land y \in (2 \dots N + 1)) \to (\{⟨1, 1⟩\} \cup c) (y) = c (y)$
362	360 361	eqeq12d	$⊢ ((φ \land (b \in B \land c \in C)) \land y \in (2 \dots N + 1)) \to ((F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y) \leftrightarrow ({(F \circ b) ↾}_{(2 \dots N + 1)}) (y) = c (y))$
363	362	ralbidva	$⊢ (φ \land (b \in B \land c \in C)) \to (\forall y \in (2 \dots N + 1) (F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y) \leftrightarrow \forall y \in (2 \dots N + 1) ({(F \circ b) ↾}_{(2 \dots N + 1)}) (y) = c (y))$
364	94	adantr	$⊢ (φ \land (b \in B \land c \in C)) \to \{1\} \cup (2 \dots N + 1) = (1 \dots N + 1)$
365	364	raleqdv	$⊢ (φ \land (b \in B \land c \in C)) \to (\forall y \in (\{1\} \cup (2 \dots N + 1)) (F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y) \leftrightarrow \forall y \in (1 \dots N + 1) (F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y))$
366	358 363 365	3bitr3rd	$⊢ (φ \land (b \in B \land c \in C)) \to (\forall y \in (1 \dots N + 1) (F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y) \leftrightarrow \forall y \in (2 \dots N + 1) ({(F \circ b) ↾}_{(2 \dots N + 1)}) (y) = c (y))$
367	58	adantrr	$⊢ (φ \land (b \in B \land c \in C)) \to (F \circ b) Fn (1 \dots N + 1)$
368	204	adantrl	$⊢ (φ \land (b \in B \land c \in C)) \to (\{⟨1, 1⟩\} \cup c) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1)$
369		f1ofn	$⊢ (\{⟨1, 1⟩\} \cup c) : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \to (\{⟨1, 1⟩\} \cup c) Fn (1 \dots N + 1)$
370	368 369	syl	$⊢ (φ \land (b \in B \land c \in C)) \to (\{⟨1, 1⟩\} \cup c) Fn (1 \dots N + 1)$
371		eqfnfv	$⊢ ((F \circ b) Fn (1 \dots N + 1) \land (\{⟨1, 1⟩\} \cup c) Fn (1 \dots N + 1)) \to (F \circ b = \{⟨1, 1⟩\} \cup c \leftrightarrow \forall y \in (1 \dots N + 1) (F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y))$
372	367 370 371	syl2anc	$⊢ (φ \land (b \in B \land c \in C)) \to (F \circ b = \{⟨1, 1⟩\} \cup c \leftrightarrow \forall y \in (1 \dots N + 1) (F \circ b) (y) = (\{⟨1, 1⟩\} \cup c) (y))$
373		fnssres	$⊢ ((F \circ b) Fn (1 \dots N + 1) \land (2 \dots N + 1) \subseteq (1 \dots N + 1)) \to ({(F \circ b) ↾}_{(2 \dots N + 1)}) Fn (2 \dots N + 1)$
374	367 122 373	sylancl	$⊢ (φ \land (b \in B \land c \in C)) \to ({(F \circ b) ↾}_{(2 \dots N + 1)}) Fn (2 \dots N + 1)$
375	195	adantrl	$⊢ (φ \land (b \in B \land c \in C)) \to c : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1)$
376		f1ofn	$⊢ c : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1) \to c Fn (2 \dots N + 1)$
377	375 376	syl	$⊢ (φ \land (b \in B \land c \in C)) \to c Fn (2 \dots N + 1)$
378		eqfnfv	$⊢ (({(F \circ b) ↾}_{(2 \dots N + 1)}) Fn (2 \dots N + 1) \land c Fn (2 \dots N + 1)) \to ({(F \circ b) ↾}_{(2 \dots N + 1)} = c \leftrightarrow \forall y \in (2 \dots N + 1) ({(F \circ b) ↾}_{(2 \dots N + 1)}) (y) = c (y))$
379	374 377 378	syl2anc	$⊢ (φ \land (b \in B \land c \in C)) \to ({(F \circ b) ↾}_{(2 \dots N + 1)} = c \leftrightarrow \forall y \in (2 \dots N + 1) ({(F \circ b) ↾}_{(2 \dots N + 1)}) (y) = c (y))$
380	366 372 379	3bitr4d	$⊢ (φ \land (b \in B \land c \in C)) \to (F \circ b = \{⟨1, 1⟩\} \cup c \leftrightarrow {(F \circ b) ↾}_{(2 \dots N + 1)} = c)$
381		eqcom	$⊢ {(F \circ b) ↾}_{(2 \dots N + 1)} = c \leftrightarrow c = {(F \circ b) ↾}_{(2 \dots N + 1)}$
382	380 381	bitrdi	$⊢ (φ \land (b \in B \land c \in C)) \to (F \circ b = \{⟨1, 1⟩\} \cup c \leftrightarrow c = {(F \circ b) ↾}_{(2 \dots N + 1)})$
383	335 347 382	3bitr3d	$⊢ (φ \land (b \in B \land c \in C)) \to (b = F \circ (\{⟨1, 1⟩\} \cup c) \leftrightarrow c = {(F \circ b) ↾}_{(2 \dots N + 1)})$
384	20 185 325 383	f1o2d	$⊢ φ \to (b \in B ⟼ {(F \circ b) ↾}_{(2 \dots N + 1)}) : B \underset{1-1 onto}{⟶} C$
385	19 384	hasheqf1od	$⊢ φ \to \|B\| = \|C\|$
386	1 2	derangen2	$⊢ (2 \dots N + 1) \in Fin \to D ((2 \dots N + 1)) = S (\|(2 \dots N + 1)\|)$
387	1	derangval	$⊢ (2 \dots N + 1) \in Fin \to D ((2 \dots N + 1)) = \|\{f \| (f : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1) \land \forall y \in (2 \dots N + 1) f (y) \neq y)\}\|$
388	10	fveq2i	$⊢ \|C\| = \|\{f \| (f : (2 \dots N + 1) \underset{1-1 onto}{⟶} (2 \dots N + 1) \land \forall y \in (2 \dots N + 1) f (y) \neq y)\}\|$
389	387 388	eqtr4di	$⊢ (2 \dots N + 1) \in Fin \to D ((2 \dots N + 1)) = \|C\|$
390	386 389	eqtr3d	$⊢ (2 \dots N + 1) \in Fin \to S (\|(2 \dots N + 1)\|) = \|C\|$
391	166 390	ax-mp	$⊢ S (\|(2 \dots N + 1)\|) = \|C\|$
392	4 60	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
393		eluzp1p1	$⊢ N \in ℤ_{\geq 1} \to N + 1 \in ℤ_{\geq (1 + 1)}$
394	392 393	syl	$⊢ φ \to N + 1 \in ℤ_{\geq (1 + 1)}$
395		df-2	$⊢ 2 = 1 + 1$
396	395	fveq2i	$⊢ ℤ_{\geq 2} = ℤ_{\geq (1 + 1)}$
397	394 396	eleqtrrdi	$⊢ φ \to N + 1 \in ℤ_{\geq 2}$
398		hashfz	$⊢ N + 1 \in ℤ_{\geq 2} \to \|(2 \dots N + 1)\| = (N + 1) - 2 + 1$
399	397 398	syl	$⊢ φ \to \|(2 \dots N + 1)\| = (N + 1) - 2 + 1$
400	59	nncnd	$⊢ φ \to N + 1 \in ℂ$
401		2cnd	$⊢ φ \to 2 \in ℂ$
402		1cnd	$⊢ φ \to 1 \in ℂ$
403	400 401 402	subsubd	$⊢ φ \to N + 1 - (2 - 1) = (N + 1) - 2 + 1$
404		2m1e1	$⊢ 2 - 1 = 1$
405	404	oveq2i	$⊢ N + 1 - (2 - 1) = N + 1 - 1$
406	4	nncnd	$⊢ φ \to N \in ℂ$
407		ax-1cn	$⊢ 1 \in ℂ$
408		pncan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - 1 = N$
409	406 407 408	sylancl	$⊢ φ \to N + 1 - 1 = N$
410	405 409	syl5eq	$⊢ φ \to N + 1 - (2 - 1) = N$
411	399 403 410	3eqtr2d	$⊢ φ \to \|(2 \dots N + 1)\| = N$
412	411	fveq2d	$⊢ φ \to S (\|(2 \dots N + 1)\|) = S (N)$
413	391 412	syl5eqr	$⊢ φ \to \|C\| = S (N)$
414	385 413	eqtrd	$⊢ φ \to \|B\| = S (N)$

Metamath Proof Explorer

Theorem subfacp1lem5

Proof