poimirlem16

Description: Lemma for poimir establishing the vertices of the simplex of poimirlem17 . (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	poimir.0	$⊢ φ \to N \in ℕ$
	poimirlem22.s	$⊢ S = \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\}$
	poimirlem22.1	$⊢ φ \to F : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
	poimirlem22.2	$⊢ φ \to T \in S$
	poimirlem18.3	$⊢ (φ \land n \in (1 \dots N)) \to \exists p \in ran F p (n) \neq K$
	poimirlem18.4	$⊢ φ \to 2^{nd} (T) = 0$
Assertion	poimirlem16	$⊢ φ \to F = (y \in (0 \dots N - 1) ⟼ (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) + if (n = 2^{nd} (1^{st} (T)) (1), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})))$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$⊢ φ \to N \in ℕ$
2		poimirlem22.s	$⊢ S = \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\}$
3		poimirlem22.1	$⊢ φ \to F : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
4		poimirlem22.2	$⊢ φ \to T \in S$
5		poimirlem18.3	$⊢ (φ \land n \in (1 \dots N)) \to \exists p \in ran F p (n) \neq K$
6		poimirlem18.4	$⊢ φ \to 2^{nd} (T) = 0$
7		fveq2	$⊢ t = T \to 2^{nd} (t) = 2^{nd} (T)$
8	7	breq2d	$⊢ t = T \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (T))$
9	8	ifbid	$⊢ t = T \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (T), y, y + 1)$
10		2fveq3	$⊢ t = T \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T))$
11		2fveq3	$⊢ t = T \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T))$
12	11	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots j)]$
13	12	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}$
14	11	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)]$
15	14	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}$
16	13 15	uneq12d	$⊢ t = T \to (2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})$
17	10 16	oveq12d	$⊢ t = T \to 1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))$
18	9 17	csbeq12dv	$⊢ t = T \to ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
19	18	mpteq2dv	$⊢ t = T \to (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))) = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
20	19	eqeq2d	$⊢ t = T \to (F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))) \leftrightarrow F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))))$
21	20 2	elrab2	$⊢ T \in S \leftrightarrow (T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \land F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))))$
22	21	simprbi	$⊢ T \in S \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
23	4 22	syl	$⊢ φ \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
24		elrabi	$⊢ T \in \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\} \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
25	24 2	eleq2s	$⊢ T \in S \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
26	4 25	syl	$⊢ φ \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
27		xp1st	$⊢ T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
28	26 27	syl	$⊢ φ \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
29		xp1st	$⊢ 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
30	28 29	syl	$⊢ φ \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
31		elmapfn	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
32	30 31	syl	$⊢ φ \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
33	32	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
34		1ex	$⊢ 1 \in V$
35		fnconstg	$⊢ 1 \in V \to (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots y + 1)]$
36	34 35	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots y + 1)]$
37		c0ex	$⊢ 0 \in V$
38		fnconstg	$⊢ 0 \in V \to (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]$
39	37 38	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]$
40	36 39	pm3.2i	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \land (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)])$
41		xp2nd	$⊢ 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
42	28 41	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
43		fvex	$⊢ 2^{nd} (1^{st} (T)) \in V$
44		f1oeq1	$⊢ f = 2^{nd} (1^{st} (T)) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
45	43 44	elab	$⊢ 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
46	42 45	sylib	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
47		dff1o3	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow (2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \land Fun {2^{nd} (1^{st} (T))}^{-1})$
48	47	simprbi	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun {2^{nd} (1^{st} (T))}^{-1}$
49	46 48	syl	$⊢ φ \to Fun {2^{nd} (1^{st} (T))}^{-1}$
50		imain	$⊢ Fun {2^{nd} (1^{st} (T))}^{-1} \to 2^{nd} (1^{st} (T)) [(1 \dots y + 1) \cap (y + 1 + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \cap 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]$
51	49 50	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots y + 1) \cap (y + 1 + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \cap 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]$
52		elfznn0	$⊢ y \in (0 \dots N - 1) \to y \in ℕ_{0}$
53		nn0p1nn	$⊢ y \in ℕ_{0} \to y + 1 \in ℕ$
54	52 53	syl	$⊢ y \in (0 \dots N - 1) \to y + 1 \in ℕ$
55	54	nnred	$⊢ y \in (0 \dots N - 1) \to y + 1 \in ℝ$
56	55	ltp1d	$⊢ y \in (0 \dots N - 1) \to y + 1 < y + 1 + 1$
57		fzdisj	$⊢ y + 1 < y + 1 + 1 \to (1 \dots y + 1) \cap (y + 1 + 1 \dots N) = \emptyset$
58	56 57	syl	$⊢ y \in (0 \dots N - 1) \to (1 \dots y + 1) \cap (y + 1 + 1 \dots N) = \emptyset$
59	58	imaeq2d	$⊢ y \in (0 \dots N - 1) \to 2^{nd} (1^{st} (T)) [(1 \dots y + 1) \cap (y + 1 + 1 \dots N)] = 2^{nd} (1^{st} (T)) [\emptyset]$
60		ima0	$⊢ 2^{nd} (1^{st} (T)) [\emptyset] = \emptyset$
61	59 60	eqtrdi	$⊢ y \in (0 \dots N - 1) \to 2^{nd} (1^{st} (T)) [(1 \dots y + 1) \cap (y + 1 + 1 \dots N)] = \emptyset$
62	51 61	sylan9req	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \cap 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] = \emptyset$
63		fnun	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \land (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]) \land 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \cap 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] = \emptyset) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \cup 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)])$
64	40 62 63	sylancr	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \cup 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)])$
65		imaundi	$⊢ 2^{nd} (1^{st} (T)) [(1 \dots y + 1) \cup (y + 1 + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \cup 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]$
66		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
67	54 66	eleqtrdi	$⊢ y \in (0 \dots N - 1) \to y + 1 \in ℤ_{\geq 1}$
68		peano2uz	$⊢ y + 1 \in ℤ_{\geq 1} \to y + 1 + 1 \in ℤ_{\geq 1}$
69	67 68	syl	$⊢ y \in (0 \dots N - 1) \to y + 1 + 1 \in ℤ_{\geq 1}$
70	1	nncnd	$⊢ φ \to N \in ℂ$
71		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
72	70 71	syl	$⊢ φ \to N - 1 + 1 = N$
73	72	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to N - 1 + 1 = N$
74		elfzuz3	$⊢ y \in (0 \dots N - 1) \to N - 1 \in ℤ_{\geq y}$
75		eluzp1p1	$⊢ N - 1 \in ℤ_{\geq y} \to N - 1 + 1 \in ℤ_{\geq (y + 1)}$
76	74 75	syl	$⊢ y \in (0 \dots N - 1) \to N - 1 + 1 \in ℤ_{\geq (y + 1)}$
77	76	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to N - 1 + 1 \in ℤ_{\geq (y + 1)}$
78	73 77	eqeltrrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to N \in ℤ_{\geq (y + 1)}$
79		fzsplit2	$⊢ (y + 1 + 1 \in ℤ_{\geq 1} \land N \in ℤ_{\geq (y + 1)}) \to (1 \dots N) = (1 \dots y + 1) \cup (y + 1 + 1 \dots N)$
80	69 78 79	syl2an2	$⊢ (φ \land y \in (0 \dots N - 1)) \to (1 \dots N) = (1 \dots y + 1) \cup (y + 1 + 1 \dots N)$
81	80	imaeq2d	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots y + 1) \cup (y + 1 + 1 \dots N)]$
82		f1ofo	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
83		foima	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = (1 \dots N)$
84	46 82 83	3syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = (1 \dots N)$
85	84	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = (1 \dots N)$
86	81 85	eqtr3d	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 \dots y + 1) \cup (y + 1 + 1 \dots N)] = (1 \dots N)$
87	65 86	eqtr3id	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \cup 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] = (1 \dots N)$
88	87	fneq2d	$⊢ (φ \land y \in (0 \dots N - 1)) \to (((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \cup 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]) \leftrightarrow ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) Fn (1 \dots N))$
89	64 88	mpbid	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
90		ovexd	$⊢ (φ \land y \in (0 \dots N - 1)) \to (1 \dots N) \in V$
91		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
92		eqidd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) = 1^{st} (1^{st} (T)) (n)$
93		eqidd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n)$
94	33 89 90 90 91 92 93	offval	$⊢ (φ \land y \in (0 \dots N - 1)) \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) = (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) + ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n))$
95		oveq1	$⊢ 1 = if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) \to 1 + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n) = if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n)$
96	95	eqeq2d	$⊢ 1 = if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) \to (((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = 1 + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n) \leftrightarrow ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n))$
97		oveq1	$⊢ 0 = if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) \to 0 + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n) = if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n)$
98	97	eqeq2d	$⊢ 0 = if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) \to (((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = 0 + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n) \leftrightarrow ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n))$
99		1p0e1	$⊢ 1 + 0 = 1$
100	99	eqcomi	$⊢ 1 = 1 + 0$
101		f1ofn	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) Fn (1 \dots N)$
102	46 101	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) Fn (1 \dots N)$
103	102	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) Fn (1 \dots N)$
104		fzss2	$⊢ N \in ℤ_{\geq (y + 1)} \to (1 \dots y + 1) \subseteq (1 \dots N)$
105	78 104	syl	$⊢ (φ \land y \in (0 \dots N - 1)) \to (1 \dots y + 1) \subseteq (1 \dots N)$
106		eluzfz1	$⊢ y + 1 \in ℤ_{\geq 1} \to 1 \in (1 \dots y + 1)$
107	67 106	syl	$⊢ y \in (0 \dots N - 1) \to 1 \in (1 \dots y + 1)$
108	107	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to 1 \in (1 \dots y + 1)$
109		fnfvima	$⊢ (2^{nd} (1^{st} (T)) Fn (1 \dots N) \land (1 \dots y + 1) \subseteq (1 \dots N) \land 1 \in (1 \dots y + 1)) \to 2^{nd} (1^{st} (T)) (1) \in 2^{nd} (1^{st} (T)) [(1 \dots y + 1)]$
110	103 105 108 109	syl3anc	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) (1) \in 2^{nd} (1^{st} (T)) [(1 \dots y + 1)]$
111		fvun1	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \land (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \land (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \cap 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] = \emptyset \land 2^{nd} (1^{st} (T)) (1) \in 2^{nd} (1^{st} (T)) [(1 \dots y + 1)])) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (1)) = (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) (2^{nd} (1^{st} (T)) (1))$
112	36 39 111	mp3an12	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \cap 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] = \emptyset \land 2^{nd} (1^{st} (T)) (1) \in 2^{nd} (1^{st} (T)) [(1 \dots y + 1)]) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (1)) = (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) (2^{nd} (1^{st} (T)) (1))$
113	62 110 112	syl2anc	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (1)) = (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) (2^{nd} (1^{st} (T)) (1))$
114	34	fvconst2	$⊢ 2^{nd} (1^{st} (T)) (1) \in 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \to (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) (2^{nd} (1^{st} (T)) (1)) = 1$
115	110 114	syl	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) (2^{nd} (1^{st} (T)) (1)) = 1$
116	113 115	eqtrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (1)) = 1$
117		simpr	$⊢ (φ \land n \in (1 \dots N - 1)) \to n \in (1 \dots N - 1)$
118	1	nnzd	$⊢ φ \to N \in ℤ$
119		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
120	118 119	syl	$⊢ φ \to N - 1 \in ℤ$
121		1z	$⊢ 1 \in ℤ$
122	120 121	jctil	$⊢ φ \to (1 \in ℤ \land N - 1 \in ℤ)$
123		elfzelz	$⊢ n \in (1 \dots N - 1) \to n \in ℤ$
124	123 121	jctir	$⊢ n \in (1 \dots N - 1) \to (n \in ℤ \land 1 \in ℤ)$
125		fzaddel	$⊢ ((1 \in ℤ \land N - 1 \in ℤ) \land (n \in ℤ \land 1 \in ℤ)) \to (n \in (1 \dots N - 1) \leftrightarrow n + 1 \in (1 + 1 \dots N - 1 + 1))$
126	122 124 125	syl2an	$⊢ (φ \land n \in (1 \dots N - 1)) \to (n \in (1 \dots N - 1) \leftrightarrow n + 1 \in (1 + 1 \dots N - 1 + 1))$
127	117 126	mpbid	$⊢ (φ \land n \in (1 \dots N - 1)) \to n + 1 \in (1 + 1 \dots N - 1 + 1)$
128	72	oveq2d	$⊢ φ \to (1 + 1 \dots N - 1 + 1) = (1 + 1 \dots N)$
129	128	adantr	$⊢ (φ \land n \in (1 \dots N - 1)) \to (1 + 1 \dots N - 1 + 1) = (1 + 1 \dots N)$
130	127 129	eleqtrd	$⊢ (φ \land n \in (1 \dots N - 1)) \to n + 1 \in (1 + 1 \dots N)$
131	130	ralrimiva	$⊢ φ \to \forall n \in (1 \dots N - 1) n + 1 \in (1 + 1 \dots N)$
132		simpr	$⊢ (φ \land y \in (1 + 1 \dots N)) \to y \in (1 + 1 \dots N)$
133		peano2z	$⊢ 1 \in ℤ \to 1 + 1 \in ℤ$
134	121 133	ax-mp	$⊢ 1 + 1 \in ℤ$
135	118 134	jctil	$⊢ φ \to (1 + 1 \in ℤ \land N \in ℤ)$
136		elfzelz	$⊢ y \in (1 + 1 \dots N) \to y \in ℤ$
137	136 121	jctir	$⊢ y \in (1 + 1 \dots N) \to (y \in ℤ \land 1 \in ℤ)$
138		fzsubel	$⊢ ((1 + 1 \in ℤ \land N \in ℤ) \land (y \in ℤ \land 1 \in ℤ)) \to (y \in (1 + 1 \dots N) \leftrightarrow y - 1 \in (1 + 1 - 1 \dots N - 1))$
139	135 137 138	syl2an	$⊢ (φ \land y \in (1 + 1 \dots N)) \to (y \in (1 + 1 \dots N) \leftrightarrow y - 1 \in (1 + 1 - 1 \dots N - 1))$
140	132 139	mpbid	$⊢ (φ \land y \in (1 + 1 \dots N)) \to y - 1 \in (1 + 1 - 1 \dots N - 1)$
141		ax-1cn	$⊢ 1 \in ℂ$
142	141 141	pncan3oi	$⊢ 1 + 1 - 1 = 1$
143	142	oveq1i	$⊢ (1 + 1 - 1 \dots N - 1) = (1 \dots N - 1)$
144	140 143	eleqtrdi	$⊢ (φ \land y \in (1 + 1 \dots N)) \to y - 1 \in (1 \dots N - 1)$
145	136	zcnd	$⊢ y \in (1 + 1 \dots N) \to y \in ℂ$
146		elfznn	$⊢ n \in (1 \dots N - 1) \to n \in ℕ$
147	146	nncnd	$⊢ n \in (1 \dots N - 1) \to n \in ℂ$
148		subadd2	$⊢ (y \in ℂ \land 1 \in ℂ \land n \in ℂ) \to (y - 1 = n \leftrightarrow n + 1 = y)$
149	141 148	mp3an2	$⊢ (y \in ℂ \land n \in ℂ) \to (y - 1 = n \leftrightarrow n + 1 = y)$
150	149	bicomd	$⊢ (y \in ℂ \land n \in ℂ) \to (n + 1 = y \leftrightarrow y - 1 = n)$
151		eqcom	$⊢ n + 1 = y \leftrightarrow y = n + 1$
152		eqcom	$⊢ y - 1 = n \leftrightarrow n = y - 1$
153	150 151 152	3bitr3g	$⊢ (y \in ℂ \land n \in ℂ) \to (y = n + 1 \leftrightarrow n = y - 1)$
154	145 147 153	syl2an	$⊢ (y \in (1 + 1 \dots N) \land n \in (1 \dots N - 1)) \to (y = n + 1 \leftrightarrow n = y - 1)$
155	154	ralrimiva	$⊢ y \in (1 + 1 \dots N) \to \forall n \in (1 \dots N - 1) (y = n + 1 \leftrightarrow n = y - 1)$
156	155	adantl	$⊢ (φ \land y \in (1 + 1 \dots N)) \to \forall n \in (1 \dots N - 1) (y = n + 1 \leftrightarrow n = y - 1)$
157		reu6i	$⊢ (y - 1 \in (1 \dots N - 1) \land \forall n \in (1 \dots N - 1) (y = n + 1 \leftrightarrow n = y - 1)) \to \exists! n \in (1 \dots N - 1) y = n + 1$
158	144 156 157	syl2anc	$⊢ (φ \land y \in (1 + 1 \dots N)) \to \exists! n \in (1 \dots N - 1) y = n + 1$
159	158	ralrimiva	$⊢ φ \to \forall y \in (1 + 1 \dots N) \exists! n \in (1 \dots N - 1) y = n + 1$
160		eqid	$⊢ (n \in (1 \dots N - 1) ⟼ n + 1) = (n \in (1 \dots N - 1) ⟼ n + 1)$
161	160	f1ompt	$⊢ (n \in (1 \dots N - 1) ⟼ n + 1) : (1 \dots N - 1) \underset{1-1 onto}{⟶} (1 + 1 \dots N) \leftrightarrow (\forall n \in (1 \dots N - 1) n + 1 \in (1 + 1 \dots N) \land \forall y \in (1 + 1 \dots N) \exists! n \in (1 \dots N - 1) y = n + 1)$
162	131 159 161	sylanbrc	$⊢ φ \to (n \in (1 \dots N - 1) ⟼ n + 1) : (1 \dots N - 1) \underset{1-1 onto}{⟶} (1 + 1 \dots N)$
163		f1osng	$⊢ (N \in ℕ \land 1 \in V) \to \{⟨N, 1⟩\} : \{N\} \underset{1-1 onto}{⟶} \{1\}$
164	1 34 163	sylancl	$⊢ φ \to \{⟨N, 1⟩\} : \{N\} \underset{1-1 onto}{⟶} \{1\}$
165	1	nnred	$⊢ φ \to N \in ℝ$
166	165	ltm1d	$⊢ φ \to N - 1 < N$
167	120	zred	$⊢ φ \to N - 1 \in ℝ$
168	167 165	ltnled	$⊢ φ \to (N - 1 < N \leftrightarrow \neg N \leq N - 1)$
169	166 168	mpbid	$⊢ φ \to \neg N \leq N - 1$
170		elfzle2	$⊢ N \in (1 \dots N - 1) \to N \leq N - 1$
171	169 170	nsyl	$⊢ φ \to \neg N \in (1 \dots N - 1)$
172		disjsn	$⊢ (1 \dots N - 1) \cap \{N\} = \emptyset \leftrightarrow \neg N \in (1 \dots N - 1)$
173	171 172	sylibr	$⊢ φ \to (1 \dots N - 1) \cap \{N\} = \emptyset$
174		1re	$⊢ 1 \in ℝ$
175	174	ltp1i	$⊢ 1 < 1 + 1$
176	174 174	readdcli	$⊢ 1 + 1 \in ℝ$
177	174 176	ltnlei	$⊢ 1 < 1 + 1 \leftrightarrow \neg 1 + 1 \leq 1$
178	175 177	mpbi	$⊢ \neg 1 + 1 \leq 1$
179		elfzle1	$⊢ 1 \in (1 + 1 \dots N) \to 1 + 1 \leq 1$
180	178 179	mto	$⊢ \neg 1 \in (1 + 1 \dots N)$
181		disjsn	$⊢ (1 + 1 \dots N) \cap \{1\} = \emptyset \leftrightarrow \neg 1 \in (1 + 1 \dots N)$
182	180 181	mpbir	$⊢ (1 + 1 \dots N) \cap \{1\} = \emptyset$
183		f1oun	$⊢ (((n \in (1 \dots N - 1) ⟼ n + 1) : (1 \dots N - 1) \underset{1-1 onto}{⟶} (1 + 1 \dots N) \land \{⟨N, 1⟩\} : \{N\} \underset{1-1 onto}{⟶} \{1\}) \land ((1 \dots N - 1) \cap \{N\} = \emptyset \land (1 + 1 \dots N) \cap \{1\} = \emptyset)) \to ((n \in (1 \dots N - 1) ⟼ n + 1) \cup \{⟨N, 1⟩\}) : (1 \dots N - 1) \cup \{N\} \underset{1-1 onto}{⟶} (1 + 1 \dots N) \cup \{1\}$
184	182 183	mpanr2	$⊢ (((n \in (1 \dots N - 1) ⟼ n + 1) : (1 \dots N - 1) \underset{1-1 onto}{⟶} (1 + 1 \dots N) \land \{⟨N, 1⟩\} : \{N\} \underset{1-1 onto}{⟶} \{1\}) \land (1 \dots N - 1) \cap \{N\} = \emptyset) \to ((n \in (1 \dots N - 1) ⟼ n + 1) \cup \{⟨N, 1⟩\}) : (1 \dots N - 1) \cup \{N\} \underset{1-1 onto}{⟶} (1 + 1 \dots N) \cup \{1\}$
185	162 164 173 184	syl21anc	$⊢ φ \to ((n \in (1 \dots N - 1) ⟼ n + 1) \cup \{⟨N, 1⟩\}) : (1 \dots N - 1) \cup \{N\} \underset{1-1 onto}{⟶} (1 + 1 \dots N) \cup \{1\}$
186	34	a1i	$⊢ φ \to 1 \in V$
187	1 66	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
188	72 187	eqeltrd	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq 1}$
189		uzid	$⊢ N - 1 \in ℤ \to N - 1 \in ℤ_{\geq (N - 1)}$
190		peano2uz	$⊢ N - 1 \in ℤ_{\geq (N - 1)} \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
191	120 189 190	3syl	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
192	72 191	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq (N - 1)}$
193		fzsplit2	$⊢ (N - 1 + 1 \in ℤ_{\geq 1} \land N \in ℤ_{\geq (N - 1)}) \to (1 \dots N) = (1 \dots N - 1) \cup (N - 1 + 1 \dots N)$
194	188 192 193	syl2anc	$⊢ φ \to (1 \dots N) = (1 \dots N - 1) \cup (N - 1 + 1 \dots N)$
195	72	oveq1d	$⊢ φ \to (N - 1 + 1 \dots N) = (N \dots N)$
196		fzsn	$⊢ N \in ℤ \to (N \dots N) = \{N\}$
197	118 196	syl	$⊢ φ \to (N \dots N) = \{N\}$
198	195 197	eqtrd	$⊢ φ \to (N - 1 + 1 \dots N) = \{N\}$
199	198	uneq2d	$⊢ φ \to (1 \dots N - 1) \cup (N - 1 + 1 \dots N) = (1 \dots N - 1) \cup \{N\}$
200	194 199	eqtr2d	$⊢ φ \to (1 \dots N - 1) \cup \{N\} = (1 \dots N)$
201		iftrue	$⊢ n = N \to if (n = N, 1, n + 1) = 1$
202	201	adantl	$⊢ (φ \land n = N) \to if (n = N, 1, n + 1) = 1$
203	1 186 200 202	fmptapd	$⊢ φ \to (n \in (1 \dots N - 1) ⟼ if (n = N, 1, n + 1)) \cup \{⟨N, 1⟩\} = (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))$
204		eleq1	$⊢ n = N \to (n \in (1 \dots N - 1) \leftrightarrow N \in (1 \dots N - 1))$
205	204	notbid	$⊢ n = N \to (\neg n \in (1 \dots N - 1) \leftrightarrow \neg N \in (1 \dots N - 1))$
206	171 205	syl5ibrcom	$⊢ φ \to (n = N \to \neg n \in (1 \dots N - 1))$
207	206	necon2ad	$⊢ φ \to (n \in (1 \dots N - 1) \to n \neq N)$
208	207	imp	$⊢ (φ \land n \in (1 \dots N - 1)) \to n \neq N$
209		ifnefalse	$⊢ n \neq N \to if (n = N, 1, n + 1) = n + 1$
210	208 209	syl	$⊢ (φ \land n \in (1 \dots N - 1)) \to if (n = N, 1, n + 1) = n + 1$
211	210	mpteq2dva	$⊢ φ \to (n \in (1 \dots N - 1) ⟼ if (n = N, 1, n + 1)) = (n \in (1 \dots N - 1) ⟼ n + 1)$
212	211	uneq1d	$⊢ φ \to (n \in (1 \dots N - 1) ⟼ if (n = N, 1, n + 1)) \cup \{⟨N, 1⟩\} = (n \in (1 \dots N - 1) ⟼ n + 1) \cup \{⟨N, 1⟩\}$
213	203 212	eqtr3d	$⊢ φ \to (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) = (n \in (1 \dots N - 1) ⟼ n + 1) \cup \{⟨N, 1⟩\}$
214	194 199	eqtrd	$⊢ φ \to (1 \dots N) = (1 \dots N - 1) \cup \{N\}$
215		uzid	$⊢ 1 \in ℤ \to 1 \in ℤ_{\geq 1}$
216		peano2uz	$⊢ 1 \in ℤ_{\geq 1} \to 1 + 1 \in ℤ_{\geq 1}$
217	121 215 216	mp2b	$⊢ 1 + 1 \in ℤ_{\geq 1}$
218		fzsplit2	$⊢ (1 + 1 \in ℤ_{\geq 1} \land N \in ℤ_{\geq 1}) \to (1 \dots N) = (1 \dots 1) \cup (1 + 1 \dots N)$
219	217 187 218	sylancr	$⊢ φ \to (1 \dots N) = (1 \dots 1) \cup (1 + 1 \dots N)$
220		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
221	121 220	ax-mp	$⊢ (1 \dots 1) = \{1\}$
222	221	uneq1i	$⊢ (1 \dots 1) \cup (1 + 1 \dots N) = \{1\} \cup (1 + 1 \dots N)$
223	222	equncomi	$⊢ (1 \dots 1) \cup (1 + 1 \dots N) = (1 + 1 \dots N) \cup \{1\}$
224	219 223	eqtrdi	$⊢ φ \to (1 \dots N) = (1 + 1 \dots N) \cup \{1\}$
225	213 214 224	f1oeq123d	$⊢ φ \to ((n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow ((n \in (1 \dots N - 1) ⟼ n + 1) \cup \{⟨N, 1⟩\}) : (1 \dots N - 1) \cup \{N\} \underset{1-1 onto}{⟶} (1 + 1 \dots N) \cup \{1\})$
226	185 225	mpbird	$⊢ φ \to (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
227		f1oco	$⊢ (2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)) \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
228	46 226 227	syl2anc	$⊢ φ \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
229		dff1o3	$⊢ (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \land Fun {(2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)))}^{-1})$
230	229	simprbi	$⊢ (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun {(2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)))}^{-1}$
231	228 230	syl	$⊢ φ \to Fun {(2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)))}^{-1}$
232		imain	$⊢ Fun {(2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)))}^{-1} \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y) \cap (y + 1 \dots N)] = (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \cap (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)]$
233	231 232	syl	$⊢ φ \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y) \cap (y + 1 \dots N)] = (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \cap (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)]$
234	52	nn0red	$⊢ y \in (0 \dots N - 1) \to y \in ℝ$
235	234	ltp1d	$⊢ y \in (0 \dots N - 1) \to y < y + 1$
236		fzdisj	$⊢ y < y + 1 \to (1 \dots y) \cap (y + 1 \dots N) = \emptyset$
237	235 236	syl	$⊢ y \in (0 \dots N - 1) \to (1 \dots y) \cap (y + 1 \dots N) = \emptyset$
238	237	imaeq2d	$⊢ y \in (0 \dots N - 1) \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y) \cap (y + 1 \dots N)] = (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [\emptyset]$
239		ima0	$⊢ (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [\emptyset] = \emptyset$
240	238 239	eqtrdi	$⊢ y \in (0 \dots N - 1) \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y) \cap (y + 1 \dots N)] = \emptyset$
241	233 240	sylan9req	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \cap (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] = \emptyset$
242		imassrn	$⊢ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N)] \subseteq ran (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))$
243		f1of	$⊢ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) : (1 \dots N) ⟶ (1 \dots N)$
244		frn	$⊢ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) : (1 \dots N) ⟶ (1 \dots N) \to ran (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) \subseteq (1 \dots N)$
245	226 243 244	3syl	$⊢ φ \to ran (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) \subseteq (1 \dots N)$
246	242 245	sstrid	$⊢ φ \to (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N)] \subseteq (1 \dots N)$
247	246	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N)] \subseteq (1 \dots N)$
248		elfz1end	$⊢ N \in ℕ \leftrightarrow N \in (1 \dots N)$
249	1 248	sylib	$⊢ φ \to N \in (1 \dots N)$
250		eqid	$⊢ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) = (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))$
251	201 250 34	fvmpt	$⊢ N \in (1 \dots N) \to (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) (N) = 1$
252	249 251	syl	$⊢ φ \to (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) (N) = 1$
253	252	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) (N) = 1$
254		f1ofn	$⊢ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) Fn (1 \dots N)$
255	226 254	syl	$⊢ φ \to (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) Fn (1 \dots N)$
256	255	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) Fn (1 \dots N)$
257		fzss1	$⊢ y + 1 \in ℤ_{\geq 1} \to (y + 1 \dots N) \subseteq (1 \dots N)$
258	67 257	syl	$⊢ y \in (0 \dots N - 1) \to (y + 1 \dots N) \subseteq (1 \dots N)$
259	258	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to (y + 1 \dots N) \subseteq (1 \dots N)$
260		eluzfz2	$⊢ N \in ℤ_{\geq (y + 1)} \to N \in (y + 1 \dots N)$
261	78 260	syl	$⊢ (φ \land y \in (0 \dots N - 1)) \to N \in (y + 1 \dots N)$
262		fnfvima	$⊢ ((n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) Fn (1 \dots N) \land (y + 1 \dots N) \subseteq (1 \dots N) \land N \in (y + 1 \dots N)) \to (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) (N) \in (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N)]$
263	256 259 261 262	syl3anc	$⊢ (φ \land y \in (0 \dots N - 1)) \to (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) (N) \in (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N)]$
264	253 263	eqeltrrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to 1 \in (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N)]$
265		fnfvima	$⊢ (2^{nd} (1^{st} (T)) Fn (1 \dots N) \land (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N)] \subseteq (1 \dots N) \land 1 \in (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N)]) \to 2^{nd} (1^{st} (T)) (1) \in 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N)]]$
266	103 247 264 265	syl3anc	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) (1) \in 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N)]]$
267		imaco	$⊢ (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N)]]$
268	266 267	eleqtrrdi	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) (1) \in (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)]$
269		fnconstg	$⊢ 1 \in V \to ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) Fn (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)]$
270	34 269	ax-mp	$⊢ ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) Fn (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)]$
271		fnconstg	$⊢ 0 \in V \to ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}) Fn (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)]$
272	37 271	ax-mp	$⊢ ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}) Fn (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)]$
273		fvun2	$⊢ (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) Fn (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \land ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}) Fn (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \land ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \cap (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] = \emptyset \land 2^{nd} (1^{st} (T)) (1) \in (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)])) \to (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (1)) = ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (1))$
274	270 272 273	mp3an12	$⊢ ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \cap (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] = \emptyset \land 2^{nd} (1^{st} (T)) (1) \in (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)]) \to (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (1)) = ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (1))$
275	241 268 274	syl2anc	$⊢ (φ \land y \in (0 \dots N - 1)) \to (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (1)) = ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (1))$
276	37	fvconst2	$⊢ 2^{nd} (1^{st} (T)) (1) \in (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \to ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (1)) = 0$
277	268 276	syl	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (1)) = 0$
278	275 277	eqtrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (1)) = 0$
279	278	oveq2d	$⊢ (φ \land y \in (0 \dots N - 1)) \to 1 + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (1)) = 1 + 0$
280	100 116 279	3eqtr4a	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (1)) = 1 + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (1))$
281		fveq2	$⊢ n = 2^{nd} (1^{st} (T)) (1) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (1))$
282		fveq2	$⊢ n = 2^{nd} (1^{st} (T)) (1) \to (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n) = (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (1))$
283	282	oveq2d	$⊢ n = 2^{nd} (1^{st} (T)) (1) \to 1 + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n) = 1 + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (1))$
284	281 283	eqeq12d	$⊢ n = 2^{nd} (1^{st} (T)) (1) \to (((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = 1 + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n) \leftrightarrow ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (1)) = 1 + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (1)))$
285	280 284	syl5ibrcom	$⊢ (φ \land y \in (0 \dots N - 1)) \to (n = 2^{nd} (1^{st} (T)) (1) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = 1 + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n))$
286	285	imp	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n = 2^{nd} (1^{st} (T)) (1)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = 1 + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n)$
287	286	adantlr	$⊢ (((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \land n = 2^{nd} (1^{st} (T)) (1)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = 1 + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n)$
288		eldifsn	$⊢ n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}) \leftrightarrow (n \in (1 \dots N) \land n \neq 2^{nd} (1^{st} (T)) (1))$
289		df-ne	$⊢ n \neq 2^{nd} (1^{st} (T)) (1) \leftrightarrow \neg n = 2^{nd} (1^{st} (T)) (1)$
290	289	anbi2i	$⊢ (n \in (1 \dots N) \land n \neq 2^{nd} (1^{st} (T)) (1)) \leftrightarrow (n \in (1 \dots N) \land \neg n = 2^{nd} (1^{st} (T)) (1))$
291	288 290	bitri	$⊢ n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}) \leftrightarrow (n \in (1 \dots N) \land \neg n = 2^{nd} (1^{st} (T)) (1))$
292		fnconstg	$⊢ 1 \in V \to (2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)]$
293	34 292	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)]$
294	293 39	pm3.2i	$⊢ ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \land (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)])$
295		imain	$⊢ Fun {2^{nd} (1^{st} (T))}^{-1} \to 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1) \cap (y + 1 + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \cap 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]$
296	49 295	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1) \cap (y + 1 + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \cap 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]$
297		fzdisj	$⊢ y + 1 < y + 1 + 1 \to (1 + 1 \dots y + 1) \cap (y + 1 + 1 \dots N) = \emptyset$
298	56 297	syl	$⊢ y \in (0 \dots N - 1) \to (1 + 1 \dots y + 1) \cap (y + 1 + 1 \dots N) = \emptyset$
299	298	imaeq2d	$⊢ y \in (0 \dots N - 1) \to 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1) \cap (y + 1 + 1 \dots N)] = 2^{nd} (1^{st} (T)) [\emptyset]$
300	299 60	eqtrdi	$⊢ y \in (0 \dots N - 1) \to 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1) \cap (y + 1 + 1 \dots N)] = \emptyset$
301	296 300	sylan9req	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \cap 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] = \emptyset$
302		fnun	$⊢ (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \land (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]) \land 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \cap 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] = \emptyset) \to ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \cup 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)])$
303	294 301 302	sylancr	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \cup 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)])$
304		imaundi	$⊢ 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1) \cup (y + 1 + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \cup 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]$
305		fzpred	$⊢ N \in ℤ_{\geq 1} \to (1 \dots N) = \{1\} \cup (1 + 1 \dots N)$
306	187 305	syl	$⊢ φ \to (1 \dots N) = \{1\} \cup (1 + 1 \dots N)$
307		uncom	$⊢ \{1\} \cup (1 + 1 \dots N) = (1 + 1 \dots N) \cup \{1\}$
308	306 307	eqtrdi	$⊢ φ \to (1 \dots N) = (1 + 1 \dots N) \cup \{1\}$
309	308	difeq1d	$⊢ φ \to (1 \dots N) ∖ \{1\} = ((1 + 1 \dots N) \cup \{1\}) ∖ \{1\}$
310		difun2	$⊢ ((1 + 1 \dots N) \cup \{1\}) ∖ \{1\} = (1 + 1 \dots N) ∖ \{1\}$
311		disj3	$⊢ (1 + 1 \dots N) \cap \{1\} = \emptyset \leftrightarrow (1 + 1 \dots N) = (1 + 1 \dots N) ∖ \{1\}$
312	182 311	mpbi	$⊢ (1 + 1 \dots N) = (1 + 1 \dots N) ∖ \{1\}$
313	310 312	eqtr4i	$⊢ ((1 + 1 \dots N) \cup \{1\}) ∖ \{1\} = (1 + 1 \dots N)$
314	309 313	eqtrdi	$⊢ φ \to (1 \dots N) ∖ \{1\} = (1 + 1 \dots N)$
315	314	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to (1 \dots N) ∖ \{1\} = (1 + 1 \dots N)$
316		eluzp1p1	$⊢ y + 1 \in ℤ_{\geq 1} \to y + 1 + 1 \in ℤ_{\geq (1 + 1)}$
317	67 316	syl	$⊢ y \in (0 \dots N - 1) \to y + 1 + 1 \in ℤ_{\geq (1 + 1)}$
318		fzsplit2	$⊢ (y + 1 + 1 \in ℤ_{\geq (1 + 1)} \land N \in ℤ_{\geq (y + 1)}) \to (1 + 1 \dots N) = (1 + 1 \dots y + 1) \cup (y + 1 + 1 \dots N)$
319	317 78 318	syl2an2	$⊢ (φ \land y \in (0 \dots N - 1)) \to (1 + 1 \dots N) = (1 + 1 \dots y + 1) \cup (y + 1 + 1 \dots N)$
320	315 319	eqtrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to (1 \dots N) ∖ \{1\} = (1 + 1 \dots y + 1) \cup (y + 1 + 1 \dots N)$
321	320	imaeq2d	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{1\}] = 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1) \cup (y + 1 + 1 \dots N)]$
322		imadif	$⊢ Fun {2^{nd} (1^{st} (T))}^{-1} \to 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{1\}] = 2^{nd} (1^{st} (T)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (T)) [\{1\}]$
323	49 322	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{1\}] = 2^{nd} (1^{st} (T)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (T)) [\{1\}]$
324		eluzfz1	$⊢ N \in ℤ_{\geq 1} \to 1 \in (1 \dots N)$
325	187 324	syl	$⊢ φ \to 1 \in (1 \dots N)$
326		fnsnfv	$⊢ (2^{nd} (1^{st} (T)) Fn (1 \dots N) \land 1 \in (1 \dots N)) \to \{2^{nd} (1^{st} (T)) (1)\} = 2^{nd} (1^{st} (T)) [\{1\}]$
327	102 325 326	syl2anc	$⊢ φ \to \{2^{nd} (1^{st} (T)) (1)\} = 2^{nd} (1^{st} (T)) [\{1\}]$
328	327	eqcomd	$⊢ φ \to 2^{nd} (1^{st} (T)) [\{1\}] = \{2^{nd} (1^{st} (T)) (1)\}$
329	84 328	difeq12d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (T)) [\{1\}] = (1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}$
330	323 329	eqtrd	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{1\}] = (1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}$
331	330	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{1\}] = (1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}$
332	321 331	eqtr3d	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1) \cup (y + 1 + 1 \dots N)] = (1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}$
333	304 332	eqtr3id	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \cup 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] = (1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}$
334	333	fneq2d	$⊢ (φ \land y \in (0 \dots N - 1)) \to (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \cup 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]) \leftrightarrow ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}))$
335	303 334	mpbid	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\})$
336		disjdifr	$⊢ ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}) \cap \{2^{nd} (1^{st} (T)) (1)\} = \emptyset$
337		fnconstg	$⊢ 1 \in V \to (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\}) Fn \{2^{nd} (1^{st} (T)) (1)\}$
338	34 337	ax-mp	$⊢ (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\}) Fn \{2^{nd} (1^{st} (T)) (1)\}$
339		fvun1	$⊢ (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}) \land (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\}) Fn \{2^{nd} (1^{st} (T)) (1)\} \land (((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}) \cap \{2^{nd} (1^{st} (T)) (1)\} = \emptyset \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}))) \to (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\})) (n) = ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n)$
340	338 339	mp3an2	$⊢ (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}) \land (((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}) \cap \{2^{nd} (1^{st} (T)) (1)\} = \emptyset \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}))) \to (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\})) (n) = ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n)$
341		fnconstg	$⊢ 0 \in V \to (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\}) Fn \{2^{nd} (1^{st} (T)) (1)\}$
342	37 341	ax-mp	$⊢ (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\}) Fn \{2^{nd} (1^{st} (T)) (1)\}$
343		fvun1	$⊢ (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}) \land (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\}) Fn \{2^{nd} (1^{st} (T)) (1)\} \land (((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}) \cap \{2^{nd} (1^{st} (T)) (1)\} = \emptyset \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}))) \to (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\})) (n) = ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n)$
344	342 343	mp3an2	$⊢ (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}) \land (((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}) \cap \{2^{nd} (1^{st} (T)) (1)\} = \emptyset \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}))) \to (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\})) (n) = ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n)$
345	340 344	eqtr4d	$⊢ (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}) \land (((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}) \cap \{2^{nd} (1^{st} (T)) (1)\} = \emptyset \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}))) \to (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\})) (n) = (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\})) (n)$
346	336 345	mpanr1	$⊢ (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\}) \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\})) \to (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\})) (n) = (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\})) (n)$
347	335 346	sylan	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (1)\})) \to (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\})) (n) = (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\})) (n)$
348	291 347	sylan2br	$⊢ ((φ \land y \in (0 \dots N - 1)) \land (n \in (1 \dots N) \land \neg n = 2^{nd} (1^{st} (T)) (1))) \to (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\})) (n) = (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\})) (n)$
349	348	anassrs	$⊢ (((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \land \neg n = 2^{nd} (1^{st} (T)) (1)) \to (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\})) (n) = (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\})) (n)$
350		fzpred	$⊢ y + 1 \in ℤ_{\geq 1} \to (1 \dots y + 1) = \{1\} \cup (1 + 1 \dots y + 1)$
351	67 350	syl	$⊢ y \in (0 \dots N - 1) \to (1 \dots y + 1) = \{1\} \cup (1 + 1 \dots y + 1)$
352	351	imaeq2d	$⊢ y \in (0 \dots N - 1) \to 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] = 2^{nd} (1^{st} (T)) [\{1\} \cup (1 + 1 \dots y + 1)]$
353	352	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] = 2^{nd} (1^{st} (T)) [\{1\} \cup (1 + 1 \dots y + 1)]$
354	327	uneq1d	$⊢ φ \to \{2^{nd} (1^{st} (T)) (1)\} \cup 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] = 2^{nd} (1^{st} (T)) [\{1\}] \cup 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)]$
355		uncom	$⊢ 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \cup \{2^{nd} (1^{st} (T)) (1)\} = \{2^{nd} (1^{st} (T)) (1)\} \cup 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)]$
356		imaundi	$⊢ 2^{nd} (1^{st} (T)) [\{1\} \cup (1 + 1 \dots y + 1)] = 2^{nd} (1^{st} (T)) [\{1\}] \cup 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)]$
357	354 355 356	3eqtr4g	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \cup \{2^{nd} (1^{st} (T)) (1)\} = 2^{nd} (1^{st} (T)) [\{1\} \cup (1 + 1 \dots y + 1)]$
358	357	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \cup \{2^{nd} (1^{st} (T)) (1)\} = 2^{nd} (1^{st} (T)) [\{1\} \cup (1 + 1 \dots y + 1)]$
359	353 358	eqtr4d	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] = 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \cup \{2^{nd} (1^{st} (T)) (1)\}$
360	359	xpeq1d	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\} = (2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \cup \{2^{nd} (1^{st} (T)) (1)\}) \times \{1\}$
361		xpundir	$⊢ (2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \cup \{2^{nd} (1^{st} (T)) (1)\}) \times \{1\} = (2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\})$
362	360 361	eqtrdi	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\} = (2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\})$
363	362	uneq1d	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}) = ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\})) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})$
364		un23	$⊢ ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\})) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}) = ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\})$
365	363 364	eqtrdi	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}) = ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\})$
366	365	fveq1d	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\})) (n)$
367	366	ad2antrr	$⊢ (((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \land \neg n = 2^{nd} (1^{st} (T)) (1)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{1\})) (n)$
368		imaco	$⊢ (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] = 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(1 \dots y)]]$
369		df-ima	$⊢ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(1 \dots y)] = ran ({(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) ↾}_{(1 \dots y)})$
370		peano2uz	$⊢ N - 1 \in ℤ_{\geq y} \to N - 1 + 1 \in ℤ_{\geq y}$
371	74 370	syl	$⊢ y \in (0 \dots N - 1) \to N - 1 + 1 \in ℤ_{\geq y}$
372	371	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to N - 1 + 1 \in ℤ_{\geq y}$
373	73 372	eqeltrrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to N \in ℤ_{\geq y}$
374		fzss2	$⊢ N \in ℤ_{\geq y} \to (1 \dots y) \subseteq (1 \dots N)$
375	373 374	syl	$⊢ (φ \land y \in (0 \dots N - 1)) \to (1 \dots y) \subseteq (1 \dots N)$
376	375	resmptd	$⊢ (φ \land y \in (0 \dots N - 1)) \to {(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) ↾}_{(1 \dots y)} = (n \in (1 \dots y) ⟼ if (n = N, 1, n + 1))$
377		fzss2	$⊢ N - 1 \in ℤ_{\geq y} \to (1 \dots y) \subseteq (1 \dots N - 1)$
378	74 377	syl	$⊢ y \in (0 \dots N - 1) \to (1 \dots y) \subseteq (1 \dots N - 1)$
379	378	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to (1 \dots y) \subseteq (1 \dots N - 1)$
380	171	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to \neg N \in (1 \dots N - 1)$
381	379 380	ssneldd	$⊢ (φ \land y \in (0 \dots N - 1)) \to \neg N \in (1 \dots y)$
382		eleq1	$⊢ n = N \to (n \in (1 \dots y) \leftrightarrow N \in (1 \dots y))$
383	382	notbid	$⊢ n = N \to (\neg n \in (1 \dots y) \leftrightarrow \neg N \in (1 \dots y))$
384	381 383	syl5ibrcom	$⊢ (φ \land y \in (0 \dots N - 1)) \to (n = N \to \neg n \in (1 \dots y))$
385	384	necon2ad	$⊢ (φ \land y \in (0 \dots N - 1)) \to (n \in (1 \dots y) \to n \neq N)$
386	385	imp	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots y)) \to n \neq N$
387	386 209	syl	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots y)) \to if (n = N, 1, n + 1) = n + 1$
388	387	mpteq2dva	$⊢ (φ \land y \in (0 \dots N - 1)) \to (n \in (1 \dots y) ⟼ if (n = N, 1, n + 1)) = (n \in (1 \dots y) ⟼ n + 1)$
389	376 388	eqtrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to {(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) ↾}_{(1 \dots y)} = (n \in (1 \dots y) ⟼ n + 1)$
390	389	rneqd	$⊢ (φ \land y \in (0 \dots N - 1)) \to ran ({(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) ↾}_{(1 \dots y)}) = ran (n \in (1 \dots y) ⟼ n + 1)$
391	369 390	eqtrid	$⊢ (φ \land y \in (0 \dots N - 1)) \to (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(1 \dots y)] = ran (n \in (1 \dots y) ⟼ n + 1)$
392		eqid	$⊢ (n \in (1 \dots y) ⟼ n + 1) = (n \in (1 \dots y) ⟼ n + 1)$
393	392	elrnmpt	$⊢ j \in V \to (j \in ran (n \in (1 \dots y) ⟼ n + 1) \leftrightarrow \exists n \in (1 \dots y) j = n + 1)$
394	393	elv	$⊢ j \in ran (n \in (1 \dots y) ⟼ n + 1) \leftrightarrow \exists n \in (1 \dots y) j = n + 1$
395		elfzelz	$⊢ y \in (0 \dots N - 1) \to y \in ℤ$
396	395	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to y \in ℤ$
397		simpr	$⊢ (y \in ℤ \land n \in (1 \dots y)) \to n \in (1 \dots y)$
398	121	jctl	$⊢ y \in ℤ \to (1 \in ℤ \land y \in ℤ)$
399		elfzelz	$⊢ n \in (1 \dots y) \to n \in ℤ$
400	399 121	jctir	$⊢ n \in (1 \dots y) \to (n \in ℤ \land 1 \in ℤ)$
401		fzaddel	$⊢ ((1 \in ℤ \land y \in ℤ) \land (n \in ℤ \land 1 \in ℤ)) \to (n \in (1 \dots y) \leftrightarrow n + 1 \in (1 + 1 \dots y + 1))$
402	398 400 401	syl2an	$⊢ (y \in ℤ \land n \in (1 \dots y)) \to (n \in (1 \dots y) \leftrightarrow n + 1 \in (1 + 1 \dots y + 1))$
403	397 402	mpbid	$⊢ (y \in ℤ \land n \in (1 \dots y)) \to n + 1 \in (1 + 1 \dots y + 1)$
404		eleq1	$⊢ j = n + 1 \to (j \in (1 + 1 \dots y + 1) \leftrightarrow n + 1 \in (1 + 1 \dots y + 1))$
405	403 404	syl5ibrcom	$⊢ (y \in ℤ \land n \in (1 \dots y)) \to (j = n + 1 \to j \in (1 + 1 \dots y + 1))$
406	405	rexlimdva	$⊢ y \in ℤ \to (\exists n \in (1 \dots y) j = n + 1 \to j \in (1 + 1 \dots y + 1))$
407		elfzelz	$⊢ j \in (1 + 1 \dots y + 1) \to j \in ℤ$
408	407	zcnd	$⊢ j \in (1 + 1 \dots y + 1) \to j \in ℂ$
409		npcan1	$⊢ j \in ℂ \to j - 1 + 1 = j$
410	408 409	syl	$⊢ j \in (1 + 1 \dots y + 1) \to j - 1 + 1 = j$
411	410	eleq1d	$⊢ j \in (1 + 1 \dots y + 1) \to (j - 1 + 1 \in (1 + 1 \dots y + 1) \leftrightarrow j \in (1 + 1 \dots y + 1))$
412	411	ibir	$⊢ j \in (1 + 1 \dots y + 1) \to j - 1 + 1 \in (1 + 1 \dots y + 1)$
413	412	adantl	$⊢ (y \in ℤ \land j \in (1 + 1 \dots y + 1)) \to j - 1 + 1 \in (1 + 1 \dots y + 1)$
414		peano2zm	$⊢ j \in ℤ \to j - 1 \in ℤ$
415	407 414	syl	$⊢ j \in (1 + 1 \dots y + 1) \to j - 1 \in ℤ$
416	415 121	jctir	$⊢ j \in (1 + 1 \dots y + 1) \to (j - 1 \in ℤ \land 1 \in ℤ)$
417		fzaddel	$⊢ ((1 \in ℤ \land y \in ℤ) \land (j - 1 \in ℤ \land 1 \in ℤ)) \to (j - 1 \in (1 \dots y) \leftrightarrow j - 1 + 1 \in (1 + 1 \dots y + 1))$
418	398 416 417	syl2an	$⊢ (y \in ℤ \land j \in (1 + 1 \dots y + 1)) \to (j - 1 \in (1 \dots y) \leftrightarrow j - 1 + 1 \in (1 + 1 \dots y + 1))$
419	413 418	mpbird	$⊢ (y \in ℤ \land j \in (1 + 1 \dots y + 1)) \to j - 1 \in (1 \dots y)$
420	408	adantl	$⊢ (y \in ℤ \land j \in (1 + 1 \dots y + 1)) \to j \in ℂ$
421	409	eqcomd	$⊢ j \in ℂ \to j = j - 1 + 1$
422	420 421	syl	$⊢ (y \in ℤ \land j \in (1 + 1 \dots y + 1)) \to j = j - 1 + 1$
423		oveq1	$⊢ n = j - 1 \to n + 1 = j - 1 + 1$
424	423	rspceeqv	$⊢ (j - 1 \in (1 \dots y) \land j = j - 1 + 1) \to \exists n \in (1 \dots y) j = n + 1$
425	419 422 424	syl2anc	$⊢ (y \in ℤ \land j \in (1 + 1 \dots y + 1)) \to \exists n \in (1 \dots y) j = n + 1$
426	425	ex	$⊢ y \in ℤ \to (j \in (1 + 1 \dots y + 1) \to \exists n \in (1 \dots y) j = n + 1)$
427	406 426	impbid	$⊢ y \in ℤ \to (\exists n \in (1 \dots y) j = n + 1 \leftrightarrow j \in (1 + 1 \dots y + 1))$
428	396 427	syl	$⊢ (φ \land y \in (0 \dots N - 1)) \to (\exists n \in (1 \dots y) j = n + 1 \leftrightarrow j \in (1 + 1 \dots y + 1))$
429	394 428	bitrid	$⊢ (φ \land y \in (0 \dots N - 1)) \to (j \in ran (n \in (1 \dots y) ⟼ n + 1) \leftrightarrow j \in (1 + 1 \dots y + 1))$
430	429	eqrdv	$⊢ (φ \land y \in (0 \dots N - 1)) \to ran (n \in (1 \dots y) ⟼ n + 1) = (1 + 1 \dots y + 1)$
431	391 430	eqtrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(1 \dots y)] = (1 + 1 \dots y + 1)$
432	431	imaeq2d	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(1 \dots y)]] = 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)]$
433	368 432	eqtrid	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] = 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)]$
434	433	xpeq1d	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}$
435		imaundi	$⊢ (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [\{N\} \cup (y + 1 \dots N - 1)] = (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [\{N\}] \cup (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N - 1)]$
436		imaco	$⊢ (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [\{N\}] = 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [\{N\}]]$
437		imaco	$⊢ (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N - 1)] = 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N - 1)]]$
438	436 437	uneq12i	$⊢ (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [\{N\}] \cup (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N - 1)] = 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [\{N\}]] \cup 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N - 1)]]$
439	435 438	eqtri	$⊢ (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [\{N\} \cup (y + 1 \dots N - 1)] = 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [\{N\}]] \cup 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N - 1)]]$
440	192	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to N \in ℤ_{\geq (N - 1)}$
441		fzsplit2	$⊢ (N - 1 + 1 \in ℤ_{\geq (y + 1)} \land N \in ℤ_{\geq (N - 1)}) \to (y + 1 \dots N) = (y + 1 \dots N - 1) \cup (N - 1 + 1 \dots N)$
442	76 440 441	syl2an2	$⊢ (φ \land y \in (0 \dots N - 1)) \to (y + 1 \dots N) = (y + 1 \dots N - 1) \cup (N - 1 + 1 \dots N)$
443	198	uneq2d	$⊢ φ \to (y + 1 \dots N - 1) \cup (N - 1 + 1 \dots N) = (y + 1 \dots N - 1) \cup \{N\}$
444	443	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to (y + 1 \dots N - 1) \cup (N - 1 + 1 \dots N) = (y + 1 \dots N - 1) \cup \{N\}$
445	442 444	eqtrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to (y + 1 \dots N) = (y + 1 \dots N - 1) \cup \{N\}$
446		uncom	$⊢ (y + 1 \dots N - 1) \cup \{N\} = \{N\} \cup (y + 1 \dots N - 1)$
447	445 446	eqtrdi	$⊢ (φ \land y \in (0 \dots N - 1)) \to (y + 1 \dots N) = \{N\} \cup (y + 1 \dots N - 1)$
448	447	imaeq2d	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] = (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [\{N\} \cup (y + 1 \dots N - 1)]$
449	252	sneqd	$⊢ φ \to \{(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) (N)\} = \{1\}$
450		fnsnfv	$⊢ ((n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) Fn (1 \dots N) \land N \in (1 \dots N)) \to \{(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) (N)\} = (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [\{N\}]$
451	255 249 450	syl2anc	$⊢ φ \to \{(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) (N)\} = (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [\{N\}]$
452	449 451	eqtr3d	$⊢ φ \to \{1\} = (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [\{N\}]$
453	452	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [\{1\}] = 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [\{N\}]]$
454	327 453	eqtrd	$⊢ φ \to \{2^{nd} (1^{st} (T)) (1)\} = 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [\{N\}]]$
455	454	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to \{2^{nd} (1^{st} (T)) (1)\} = 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [\{N\}]]$
456		df-ima	$⊢ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N - 1)] = ran ({(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) ↾}_{(y + 1 \dots N - 1)})$
457		fzss1	$⊢ y + 1 \in ℤ_{\geq 1} \to (y + 1 \dots N - 1) \subseteq (1 \dots N - 1)$
458	67 457	syl	$⊢ y \in (0 \dots N - 1) \to (y + 1 \dots N - 1) \subseteq (1 \dots N - 1)$
459		fzss2	$⊢ N \in ℤ_{\geq (N - 1)} \to (1 \dots N - 1) \subseteq (1 \dots N)$
460	192 459	syl	$⊢ φ \to (1 \dots N - 1) \subseteq (1 \dots N)$
461	458 460	sylan9ssr	$⊢ (φ \land y \in (0 \dots N - 1)) \to (y + 1 \dots N - 1) \subseteq (1 \dots N)$
462	461	resmptd	$⊢ (φ \land y \in (0 \dots N - 1)) \to {(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) ↾}_{(y + 1 \dots N - 1)} = (n \in (y + 1 \dots N - 1) ⟼ if (n = N, 1, n + 1))$
463		elfzle2	$⊢ N \in (y + 1 \dots N - 1) \to N \leq N - 1$
464	169 463	nsyl	$⊢ φ \to \neg N \in (y + 1 \dots N - 1)$
465		eleq1	$⊢ n = N \to (n \in (y + 1 \dots N - 1) \leftrightarrow N \in (y + 1 \dots N - 1))$
466	465	notbid	$⊢ n = N \to (\neg n \in (y + 1 \dots N - 1) \leftrightarrow \neg N \in (y + 1 \dots N - 1))$
467	464 466	syl5ibrcom	$⊢ φ \to (n = N \to \neg n \in (y + 1 \dots N - 1))$
468	467	con2d	$⊢ φ \to (n \in (y + 1 \dots N - 1) \to \neg n = N)$
469	468	imp	$⊢ (φ \land n \in (y + 1 \dots N - 1)) \to \neg n = N$
470	469	iffalsed	$⊢ (φ \land n \in (y + 1 \dots N - 1)) \to if (n = N, 1, n + 1) = n + 1$
471	470	mpteq2dva	$⊢ φ \to (n \in (y + 1 \dots N - 1) ⟼ if (n = N, 1, n + 1)) = (n \in (y + 1 \dots N - 1) ⟼ n + 1)$
472	471	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to (n \in (y + 1 \dots N - 1) ⟼ if (n = N, 1, n + 1)) = (n \in (y + 1 \dots N - 1) ⟼ n + 1)$
473	462 472	eqtrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to {(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) ↾}_{(y + 1 \dots N - 1)} = (n \in (y + 1 \dots N - 1) ⟼ n + 1)$
474	473	rneqd	$⊢ (φ \land y \in (0 \dots N - 1)) \to ran ({(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) ↾}_{(y + 1 \dots N - 1)}) = ran (n \in (y + 1 \dots N - 1) ⟼ n + 1)$
475	456 474	eqtrid	$⊢ (φ \land y \in (0 \dots N - 1)) \to (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N - 1)] = ran (n \in (y + 1 \dots N - 1) ⟼ n + 1)$
476		elfzelz	$⊢ j \in (y + 1 + 1 \dots N - 1 + 1) \to j \in ℤ$
477	476	zcnd	$⊢ j \in (y + 1 + 1 \dots N - 1 + 1) \to j \in ℂ$
478	477 409	syl	$⊢ j \in (y + 1 + 1 \dots N - 1 + 1) \to j - 1 + 1 = j$
479	478	eleq1d	$⊢ j \in (y + 1 + 1 \dots N - 1 + 1) \to (j - 1 + 1 \in (y + 1 + 1 \dots N - 1 + 1) \leftrightarrow j \in (y + 1 + 1 \dots N - 1 + 1))$
480	479	ibir	$⊢ j \in (y + 1 + 1 \dots N - 1 + 1) \to j - 1 + 1 \in (y + 1 + 1 \dots N - 1 + 1)$
481	480	adantl	$⊢ ((φ \land y \in (0 \dots N - 1)) \land j \in (y + 1 + 1 \dots N - 1 + 1)) \to j - 1 + 1 \in (y + 1 + 1 \dots N - 1 + 1)$
482	54	nnzd	$⊢ y \in (0 \dots N - 1) \to y + 1 \in ℤ$
483	120 482	anim12ci	$⊢ (φ \land y \in (0 \dots N - 1)) \to (y + 1 \in ℤ \land N - 1 \in ℤ)$
484	476 414	syl	$⊢ j \in (y + 1 + 1 \dots N - 1 + 1) \to j - 1 \in ℤ$
485	484 121	jctir	$⊢ j \in (y + 1 + 1 \dots N - 1 + 1) \to (j - 1 \in ℤ \land 1 \in ℤ)$
486		fzaddel	$⊢ ((y + 1 \in ℤ \land N - 1 \in ℤ) \land (j - 1 \in ℤ \land 1 \in ℤ)) \to (j - 1 \in (y + 1 \dots N - 1) \leftrightarrow j - 1 + 1 \in (y + 1 + 1 \dots N - 1 + 1))$
487	483 485 486	syl2an	$⊢ ((φ \land y \in (0 \dots N - 1)) \land j \in (y + 1 + 1 \dots N - 1 + 1)) \to (j - 1 \in (y + 1 \dots N - 1) \leftrightarrow j - 1 + 1 \in (y + 1 + 1 \dots N - 1 + 1))$
488	481 487	mpbird	$⊢ ((φ \land y \in (0 \dots N - 1)) \land j \in (y + 1 + 1 \dots N - 1 + 1)) \to j - 1 \in (y + 1 \dots N - 1)$
489	477 421	syl	$⊢ j \in (y + 1 + 1 \dots N - 1 + 1) \to j = j - 1 + 1$
490	489	adantl	$⊢ ((φ \land y \in (0 \dots N - 1)) \land j \in (y + 1 + 1 \dots N - 1 + 1)) \to j = j - 1 + 1$
491	423	rspceeqv	$⊢ (j - 1 \in (y + 1 \dots N - 1) \land j = j - 1 + 1) \to \exists n \in (y + 1 \dots N - 1) j = n + 1$
492	488 490 491	syl2anc	$⊢ ((φ \land y \in (0 \dots N - 1)) \land j \in (y + 1 + 1 \dots N - 1 + 1)) \to \exists n \in (y + 1 \dots N - 1) j = n + 1$
493	492	ex	$⊢ (φ \land y \in (0 \dots N - 1)) \to (j \in (y + 1 + 1 \dots N - 1 + 1) \to \exists n \in (y + 1 \dots N - 1) j = n + 1)$
494		simpr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (y + 1 \dots N - 1)) \to n \in (y + 1 \dots N - 1)$
495		elfzelz	$⊢ n \in (y + 1 \dots N - 1) \to n \in ℤ$
496	495 121	jctir	$⊢ n \in (y + 1 \dots N - 1) \to (n \in ℤ \land 1 \in ℤ)$
497		fzaddel	$⊢ ((y + 1 \in ℤ \land N - 1 \in ℤ) \land (n \in ℤ \land 1 \in ℤ)) \to (n \in (y + 1 \dots N - 1) \leftrightarrow n + 1 \in (y + 1 + 1 \dots N - 1 + 1))$
498	483 496 497	syl2an	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (y + 1 \dots N - 1)) \to (n \in (y + 1 \dots N - 1) \leftrightarrow n + 1 \in (y + 1 + 1 \dots N - 1 + 1))$
499	494 498	mpbid	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (y + 1 \dots N - 1)) \to n + 1 \in (y + 1 + 1 \dots N - 1 + 1)$
500		eleq1	$⊢ j = n + 1 \to (j \in (y + 1 + 1 \dots N - 1 + 1) \leftrightarrow n + 1 \in (y + 1 + 1 \dots N - 1 + 1))$
501	499 500	syl5ibrcom	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (y + 1 \dots N - 1)) \to (j = n + 1 \to j \in (y + 1 + 1 \dots N - 1 + 1))$
502	501	rexlimdva	$⊢ (φ \land y \in (0 \dots N - 1)) \to (\exists n \in (y + 1 \dots N - 1) j = n + 1 \to j \in (y + 1 + 1 \dots N - 1 + 1))$
503	493 502	impbid	$⊢ (φ \land y \in (0 \dots N - 1)) \to (j \in (y + 1 + 1 \dots N - 1 + 1) \leftrightarrow \exists n \in (y + 1 \dots N - 1) j = n + 1)$
504		eqid	$⊢ (n \in (y + 1 \dots N - 1) ⟼ n + 1) = (n \in (y + 1 \dots N - 1) ⟼ n + 1)$
505	504	elrnmpt	$⊢ j \in V \to (j \in ran (n \in (y + 1 \dots N - 1) ⟼ n + 1) \leftrightarrow \exists n \in (y + 1 \dots N - 1) j = n + 1)$
506	505	elv	$⊢ j \in ran (n \in (y + 1 \dots N - 1) ⟼ n + 1) \leftrightarrow \exists n \in (y + 1 \dots N - 1) j = n + 1$
507	503 506	bitr4di	$⊢ (φ \land y \in (0 \dots N - 1)) \to (j \in (y + 1 + 1 \dots N - 1 + 1) \leftrightarrow j \in ran (n \in (y + 1 \dots N - 1) ⟼ n + 1))$
508	507	eqrdv	$⊢ (φ \land y \in (0 \dots N - 1)) \to (y + 1 + 1 \dots N - 1 + 1) = ran (n \in (y + 1 \dots N - 1) ⟼ n + 1)$
509	72	oveq2d	$⊢ φ \to (y + 1 + 1 \dots N - 1 + 1) = (y + 1 + 1 \dots N)$
510	509	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to (y + 1 + 1 \dots N - 1 + 1) = (y + 1 + 1 \dots N)$
511	475 508 510	3eqtr2rd	$⊢ (φ \land y \in (0 \dots N - 1)) \to (y + 1 + 1 \dots N) = (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N - 1)]$
512	511	imaeq2d	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N - 1)]]$
513	455 512	uneq12d	$⊢ (φ \land y \in (0 \dots N - 1)) \to \{2^{nd} (1^{st} (T)) (1)\} \cup 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [\{N\}]] \cup 2^{nd} (1^{st} (T)) [(n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)) [(y + 1 \dots N - 1)]]$
514	439 448 513	3eqtr4a	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] = \{2^{nd} (1^{st} (T)) (1)\} \cup 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]$
515	514	xpeq1d	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\} = (\{2^{nd} (1^{st} (T)) (1)\} \cup 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]) \times \{0\}$
516		xpundir	$⊢ (\{2^{nd} (1^{st} (T)) (1)\} \cup 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]) \times \{0\} = (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})$
517	515 516	eqtrdi	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\} = (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})$
518	434 517	uneq12d	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup ((\{2^{nd} (1^{st} (T)) (1)\} \times \{0\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}))$
519		unass	$⊢ ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\})) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup ((\{2^{nd} (1^{st} (T)) (1)\} \times \{0\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}))$
520		un23	$⊢ ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\})) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}) = ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\})$
521	519 520	eqtr3i	$⊢ (2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup ((\{2^{nd} (1^{st} (T)) (1)\} \times \{0\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) = ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\})$
522	518 521	eqtrdi	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}) = ((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\})$
523	522	fveq1d	$⊢ (φ \land y \in (0 \dots N - 1)) \to (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n) = (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\})) (n)$
524	523	ad2antrr	$⊢ (((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \land \neg n = 2^{nd} (1^{st} (T)) (1)) \to (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n) = (((2^{nd} (1^{st} (T)) [(1 + 1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (1)\} \times \{0\})) (n)$
525	349 367 524	3eqtr4d	$⊢ (((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \land \neg n = 2^{nd} (1^{st} (T)) (1)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n)$
526		snssi	$⊢ 1 \in ℂ \to \{1\} \subseteq ℂ$
527	141 526	ax-mp	$⊢ \{1\} \subseteq ℂ$
528		0cn	$⊢ 0 \in ℂ$
529		snssi	$⊢ 0 \in ℂ \to \{0\} \subseteq ℂ$
530	528 529	ax-mp	$⊢ \{0\} \subseteq ℂ$
531	527 530	unssi	$⊢ \{1\} \cup \{0\} \subseteq ℂ$
532	34	fconst	$⊢ ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) : (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] ⟶ \{1\}$
533	37	fconst	$⊢ ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}) : (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] ⟶ \{0\}$
534	532 533	pm3.2i	$⊢ (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) : (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] ⟶ \{1\} \land ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}) : (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] ⟶ \{0\})$
535		fun	$⊢ ((((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) : (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] ⟶ \{1\} \land ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}) : (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] ⟶ \{0\}) \land (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \cap (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] = \emptyset) \to (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) : (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \cup (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] ⟶ \{1\} \cup \{0\}$
536	534 241 535	sylancr	$⊢ (φ \land y \in (0 \dots N - 1)) \to (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) : (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \cup (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] ⟶ \{1\} \cup \{0\}$
537		imaundi	$⊢ (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y) \cup (y + 1 \dots N)] = (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \cup (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)]$
538		fzsplit2	$⊢ (y + 1 \in ℤ_{\geq 1} \land N \in ℤ_{\geq y}) \to (1 \dots N) = (1 \dots y) \cup (y + 1 \dots N)$
539	67 373 538	syl2an2	$⊢ (φ \land y \in (0 \dots N - 1)) \to (1 \dots N) = (1 \dots y) \cup (y + 1 \dots N)$
540	539	imaeq2d	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots N)] = (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y) \cup (y + 1 \dots N)]$
541		f1ofo	$⊢ (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
542		foima	$⊢ (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots N)] = (1 \dots N)$
543	228 541 542	3syl	$⊢ φ \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots N)] = (1 \dots N)$
544	543	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots N)] = (1 \dots N)$
545	540 544	eqtr3d	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y) \cup (y + 1 \dots N)] = (1 \dots N)$
546	537 545	eqtr3id	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \cup (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] = (1 \dots N)$
547	546	feq2d	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) : (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \cup (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] ⟶ \{1\} \cup \{0\} \leftrightarrow (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) : (1 \dots N) ⟶ \{1\} \cup \{0\})$
548	536 547	mpbid	$⊢ (φ \land y \in (0 \dots N - 1)) \to (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) : (1 \dots N) ⟶ \{1\} \cup \{0\}$
549	548	ffvelcdmda	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \to (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n) \in (\{1\} \cup \{0\})$
550	531 549	sselid	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \to (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n) \in ℂ$
551	550	addlidd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \to 0 + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n) = (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n)$
552	551	adantr	$⊢ (((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \land \neg n = 2^{nd} (1^{st} (T)) (1)) \to 0 + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n) = (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n)$
553	525 552	eqtr4d	$⊢ (((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \land \neg n = 2^{nd} (1^{st} (T)) (1)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = 0 + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n)$
554	96 98 287 553	ifbothda	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n)$
555	554	oveq2d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) + ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = 1^{st} (1^{st} (T)) (n) + if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n)$
556		elmapi	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
557	30 556	syl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
558	557	ffvelcdmda	$⊢ (φ \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) \in (0 ..^K)$
559		elfzonn0	$⊢ 1^{st} (1^{st} (T)) (n) \in (0 ..^K) \to 1^{st} (1^{st} (T)) (n) \in ℕ_{0}$
560	558 559	syl	$⊢ (φ \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) \in ℕ_{0}$
561	560	nn0cnd	$⊢ (φ \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) \in ℂ$
562	561	adantlr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) \in ℂ$
563	141 528	ifcli	$⊢ if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) \in ℂ$
564	563	a1i	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \to if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) \in ℂ$
565	562 564 550	addassd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) + if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n) = 1^{st} (1^{st} (T)) (n) + if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n)$
566	555 565	eqtr4d	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) + ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n) = 1^{st} (1^{st} (T)) (n) + if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n)$
567	566	mpteq2dva	$⊢ (φ \land y \in (0 \dots N - 1)) \to (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) + ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) (n)) = (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) + if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n))$
568	94 567	eqtrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})) = (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) + if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n))$
569	6	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (T) = 0$
570		elfzle1	$⊢ y \in (0 \dots N - 1) \to 0 \leq y$
571	570	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to 0 \leq y$
572	569 571	eqbrtrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (T) \leq y$
573		0re	$⊢ 0 \in ℝ$
574	6 573	eqeltrdi	$⊢ φ \to 2^{nd} (T) \in ℝ$
575		lenlt	$⊢ (2^{nd} (T) \in ℝ \land y \in ℝ) \to (2^{nd} (T) \leq y \leftrightarrow \neg y < 2^{nd} (T))$
576	574 234 575	syl2an	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (T) \leq y \leftrightarrow \neg y < 2^{nd} (T))$
577	572 576	mpbid	$⊢ (φ \land y \in (0 \dots N - 1)) \to \neg y < 2^{nd} (T)$
578	577	iffalsed	$⊢ (φ \land y \in (0 \dots N - 1)) \to if (y < 2^{nd} (T), y, y + 1) = y + 1$
579	578	csbeq1d	$⊢ (φ \land y \in (0 \dots N - 1)) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ (y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
580		ovex	$⊢ y + 1 \in V$
581		oveq2	$⊢ j = y + 1 \to (1 \dots j) = (1 \dots y + 1)$
582	581	imaeq2d	$⊢ j = y + 1 \to 2^{nd} (1^{st} (T)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots y + 1)]$
583	582	xpeq1d	$⊢ j = y + 1 \to 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}$
584		oveq1	$⊢ j = y + 1 \to j + 1 = y + 1 + 1$
585	584	oveq1d	$⊢ j = y + 1 \to (j + 1 \dots N) = (y + 1 + 1 \dots N)$
586	585	imaeq2d	$⊢ j = y + 1 \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)]$
587	586	xpeq1d	$⊢ j = y + 1 \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}$
588	583 587	uneq12d	$⊢ j = y + 1 \to (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\})$
589	588	oveq2d	$⊢ j = y + 1 \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}))$
590	580 589	csbie	$⊢ ⦋ (y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}))$
591	579 590	eqtrdi	$⊢ (φ \land y \in (0 \dots N - 1)) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y + 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 + 1 \dots N)] \times \{0\}))$
592		ovexd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) + if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) \in V$
593		fvexd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land n \in (1 \dots N)) \to (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n) \in V$
594		eqidd	$⊢ (φ \land y \in (0 \dots N - 1)) \to (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) + if (n = 2^{nd} (1^{st} (T)) (1), 1, 0)) = (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) + if (n = 2^{nd} (1^{st} (T)) (1), 1, 0))$
595	548	ffnd	$⊢ (φ \land y \in (0 \dots N - 1)) \to (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
596		nfcv	$⊢ \underline{Ⅎ} n 2^{nd} (1^{st} (T))$
597		nfmpt1	$⊢ \underline{Ⅎ} n (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))$
598	596 597	nfco	$⊢ \underline{Ⅎ} n (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1)))$
599		nfcv	$⊢ \underline{Ⅎ} n (1 \dots y)$
600	598 599	nfima	$⊢ \underline{Ⅎ} n (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)]$
601		nfcv	$⊢ \underline{Ⅎ} n \{1\}$
602	600 601	nfxp	$⊢ \underline{Ⅎ} n ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\})$
603		nfcv	$⊢ \underline{Ⅎ} n (y + 1 \dots N)$
604	598 603	nfima	$⊢ \underline{Ⅎ} n (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)]$
605		nfcv	$⊢ \underline{Ⅎ} n \{0\}$
606	604 605	nfxp	$⊢ \underline{Ⅎ} n ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})$
607	602 606	nfun	$⊢ \underline{Ⅎ} n (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}))$
608	607	dffn5f	$⊢ (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) Fn (1 \dots N) \leftrightarrow ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}) = (n \in (1 \dots N) ⟼ (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n))$
609	595 608	sylib	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}) = (n \in (1 \dots N) ⟼ (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n))$
610	90 592 593 594 609	offval2	$⊢ (φ \land y \in (0 \dots N - 1)) \to (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) + if (n = 2^{nd} (1^{st} (T)) (1), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) = (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) + if (n = 2^{nd} (1^{st} (T)) (1), 1, 0) + (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) (n))$
611	568 591 610	3eqtr4rd	$⊢ (φ \land y \in (0 \dots N - 1)) \to (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) + if (n = 2^{nd} (1^{st} (T)) (1), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
612	611	mpteq2dva	$⊢ φ \to (y \in (0 \dots N - 1) ⟼ (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) + if (n = 2^{nd} (1^{st} (T)) (1), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\}))) = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
613	23 612	eqtr4d	$⊢ φ \to F = (y \in (0 \dots N - 1) ⟼ (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) + if (n = 2^{nd} (1^{st} (T)) (1), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(1 \dots y)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = N, 1, n + 1))) [(y + 1 \dots N)] \times \{0\})))$

Metamath Proof Explorer

Theorem poimirlem16

Proof