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

Metamath Proof Explorer

Theorem subfacp1lem5

Proof