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

Metamath Proof Explorer

Theorem subfacp1lem5

Proof