poimirlem20

	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$
	poimirlem22.3	$⊢ (φ \land n \in (1 \dots N)) \to \exists p \in ran F p (n) \neq 0$
	poimirlem21.4	$⊢ φ \to 2^{nd} (T) = N$
Assertion	poimirlem20	$⊢ φ \to \exists z \in S z \neq T$

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		poimirlem22.3	$⊢ (φ \land n \in (1 \dots N)) \to \exists p \in ran F p (n) \neq 0$
6		poimirlem21.4	$⊢ φ \to 2^{nd} (T) = N$
7		oveq2	$⊢ 1 = if (n = 2^{nd} (1^{st} (T)) (N), 1, 0) \to 1^{st} (1^{st} (T)) (n) - 1 = 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)$
8	7	eleq1d	$⊢ 1 = if (n = 2^{nd} (1^{st} (T)) (N), 1, 0) \to (1^{st} (1^{st} (T)) (n) - 1 \in (0 ..^K) \leftrightarrow 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0) \in (0 ..^K))$
9		oveq2	$⊢ 0 = if (n = 2^{nd} (1^{st} (T)) (N), 1, 0) \to 1^{st} (1^{st} (T)) (n) - 0 = 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)$
10	9	eleq1d	$⊢ 0 = if (n = 2^{nd} (1^{st} (T)) (N), 1, 0) \to (1^{st} (1^{st} (T)) (n) - 0 \in (0 ..^K) \leftrightarrow 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0) \in (0 ..^K))$
11		fveq2	$⊢ n = 2^{nd} (1^{st} (T)) (N) \to 1^{st} (1^{st} (T)) (n) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N))$
12	11	oveq1d	$⊢ n = 2^{nd} (1^{st} (T)) (N) \to 1^{st} (1^{st} (T)) (n) - 1 = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) - 1$
13	12	adantl	$⊢ (φ \land n = 2^{nd} (1^{st} (T)) (N)) \to 1^{st} (1^{st} (T)) (n) - 1 = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) - 1$
14		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))$
15	14 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))$
16	4 15	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))$
17		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)\})$
18	16 17	syl	$⊢ φ \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
19		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)})$
20	18 19	syl	$⊢ φ \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
21		elmapi	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
22	20 21	syl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
23		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)\}$
24	18 23	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
25		fvex	$⊢ 2^{nd} (1^{st} (T)) \in V$
26		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))$
27	25 26	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)$
28	24 27	sylib	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
29		f1of	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) : (1 \dots N) ⟶ (1 \dots N)$
30	28 29	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) ⟶ (1 \dots N)$
31		elfz1end	$⊢ N \in ℕ \leftrightarrow N \in (1 \dots N)$
32	1 31	sylib	$⊢ φ \to N \in (1 \dots N)$
33	30 32	ffvelcdmd	$⊢ φ \to 2^{nd} (1^{st} (T)) (N) \in (1 \dots N)$
34	22 33	ffvelcdmd	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \in (0 ..^K)$
35		elfzonn0	$⊢ 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \in (0 ..^K) \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \in ℕ_{0}$
36	34 35	syl	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \in ℕ_{0}$
37		fvex	$⊢ 2^{nd} (1^{st} (T)) (N) \in V$
38		eleq1	$⊢ n = 2^{nd} (1^{st} (T)) (N) \to (n \in (1 \dots N) \leftrightarrow 2^{nd} (1^{st} (T)) (N) \in (1 \dots N))$
39	38	anbi2d	$⊢ n = 2^{nd} (1^{st} (T)) (N) \to ((φ \land n \in (1 \dots N)) \leftrightarrow (φ \land 2^{nd} (1^{st} (T)) (N) \in (1 \dots N)))$
40		fveq2	$⊢ n = 2^{nd} (1^{st} (T)) (N) \to p (n) = p (2^{nd} (1^{st} (T)) (N))$
41	40	neeq1d	$⊢ n = 2^{nd} (1^{st} (T)) (N) \to (p (n) \neq 0 \leftrightarrow p (2^{nd} (1^{st} (T)) (N)) \neq 0)$
42	41	rexbidv	$⊢ n = 2^{nd} (1^{st} (T)) (N) \to (\exists p \in ran F p (n) \neq 0 \leftrightarrow \exists p \in ran F p (2^{nd} (1^{st} (T)) (N)) \neq 0)$
43	39 42	imbi12d	$⊢ n = 2^{nd} (1^{st} (T)) (N) \to (((φ \land n \in (1 \dots N)) \to \exists p \in ran F p (n) \neq 0) \leftrightarrow ((φ \land 2^{nd} (1^{st} (T)) (N) \in (1 \dots N)) \to \exists p \in ran F p (2^{nd} (1^{st} (T)) (N)) \neq 0))$
44	37 43 5	vtocl	$⊢ (φ \land 2^{nd} (1^{st} (T)) (N) \in (1 \dots N)) \to \exists p \in ran F p (2^{nd} (1^{st} (T)) (N)) \neq 0$
45	33 44	mpdan	$⊢ φ \to \exists p \in ran F p (2^{nd} (1^{st} (T)) (N)) \neq 0$
46		fveq1	$⊢ p = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})) \to p (2^{nd} (1^{st} (T)) (N)) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))) (2^{nd} (1^{st} (T)) (N))$
47	22	ffnd	$⊢ φ \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
48	47	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
49		1ex	$⊢ 1 \in V$
50		fnconstg	$⊢ 1 \in V \to (2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots y)]$
51	49 50	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots y)]$
52		c0ex	$⊢ 0 \in V$
53		fnconstg	$⊢ 0 \in V \to (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(y + 1 \dots N)]$
54	52 53	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(y + 1 \dots N)]$
55	51 54	pm3.2i	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots y)] \land (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(y + 1 \dots N)])$
56		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})$
57	56	simprbi	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun {2^{nd} (1^{st} (T))}^{-1}$
58	28 57	syl	$⊢ φ \to Fun {2^{nd} (1^{st} (T))}^{-1}$
59		imain	$⊢ Fun {2^{nd} (1^{st} (T))}^{-1} \to 2^{nd} (1^{st} (T)) [(1 \dots y) \cap (y + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots y)] \cap 2^{nd} (1^{st} (T)) [(y + 1 \dots N)]$
60	58 59	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots y) \cap (y + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots y)] \cap 2^{nd} (1^{st} (T)) [(y + 1 \dots N)]$
61		elfznn0	$⊢ y \in (0 \dots N - 1) \to y \in ℕ_{0}$
62	61	nn0red	$⊢ y \in (0 \dots N - 1) \to y \in ℝ$
63	62	ltp1d	$⊢ y \in (0 \dots N - 1) \to y < y + 1$
64		fzdisj	$⊢ y < y + 1 \to (1 \dots y) \cap (y + 1 \dots N) = \emptyset$
65	63 64	syl	$⊢ y \in (0 \dots N - 1) \to (1 \dots y) \cap (y + 1 \dots N) = \emptyset$
66	65	imaeq2d	$⊢ y \in (0 \dots N - 1) \to 2^{nd} (1^{st} (T)) [(1 \dots y) \cap (y + 1 \dots N)] = 2^{nd} (1^{st} (T)) [\emptyset]$
67		ima0	$⊢ 2^{nd} (1^{st} (T)) [\emptyset] = \emptyset$
68	66 67	eqtrdi	$⊢ y \in (0 \dots N - 1) \to 2^{nd} (1^{st} (T)) [(1 \dots y) \cap (y + 1 \dots N)] = \emptyset$
69	60 68	sylan9req	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 \dots y)] \cap 2^{nd} (1^{st} (T)) [(y + 1 \dots N)] = \emptyset$
70		fnun	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots y)] \land (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(y + 1 \dots N)]) \land 2^{nd} (1^{st} (T)) [(1 \dots y)] \cap 2^{nd} (1^{st} (T)) [(y + 1 \dots N)] = \emptyset) \to ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots y)] \cup 2^{nd} (1^{st} (T)) [(y + 1 \dots N)])$
71	55 69 70	sylancr	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots y)] \cup 2^{nd} (1^{st} (T)) [(y + 1 \dots N)])$
72		imaundi	$⊢ 2^{nd} (1^{st} (T)) [(1 \dots y) \cup (y + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots y)] \cup 2^{nd} (1^{st} (T)) [(y + 1 \dots N)]$
73		nn0p1nn	$⊢ y \in ℕ_{0} \to y + 1 \in ℕ$
74		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
75	73 74	eleqtrdi	$⊢ y \in ℕ_{0} \to y + 1 \in ℤ_{\geq 1}$
76	61 75	syl	$⊢ y \in (0 \dots N - 1) \to y + 1 \in ℤ_{\geq 1}$
77	76	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to y + 1 \in ℤ_{\geq 1}$
78	1	nncnd	$⊢ φ \to N \in ℂ$
79		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
80	78 79	syl	$⊢ φ \to N - 1 + 1 = N$
81	80	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to N - 1 + 1 = N$
82		elfzuz3	$⊢ y \in (0 \dots N - 1) \to N - 1 \in ℤ_{\geq y}$
83		peano2uz	$⊢ N - 1 \in ℤ_{\geq y} \to N - 1 + 1 \in ℤ_{\geq y}$
84	82 83	syl	$⊢ y \in (0 \dots N - 1) \to N - 1 + 1 \in ℤ_{\geq y}$
85	84	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to N - 1 + 1 \in ℤ_{\geq y}$
86	81 85	eqeltrrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to N \in ℤ_{\geq y}$
87		fzsplit2	$⊢ (y + 1 \in ℤ_{\geq 1} \land N \in ℤ_{\geq y}) \to (1 \dots N) = (1 \dots y) \cup (y + 1 \dots N)$
88	77 86 87	syl2anc	$⊢ (φ \land y \in (0 \dots N - 1)) \to (1 \dots N) = (1 \dots y) \cup (y + 1 \dots N)$
89	88	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) \cup (y + 1 \dots N)]$
90		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)$
91		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)$
92	28 90 91	3syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = (1 \dots N)$
93	92	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = (1 \dots N)$
94	89 93	eqtr3d	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 \dots y) \cup (y + 1 \dots N)] = (1 \dots N)$
95	72 94	eqtr3id	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) [(1 \dots y)] \cup 2^{nd} (1^{st} (T)) [(y + 1 \dots N)] = (1 \dots N)$
96	95	fneq2d	$⊢ (φ \land y \in (0 \dots N - 1)) \to (((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots y)] \cup 2^{nd} (1^{st} (T)) [(y + 1 \dots N)]) \leftrightarrow ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})) Fn (1 \dots N))$
97	71 96	mpbid	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
98		ovex	$⊢ (1 \dots N) \in V$
99	98	a1i	$⊢ (φ \land y \in (0 \dots N - 1)) \to (1 \dots N) \in V$
100		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
101		eqidd	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (1^{st} (T)) (N) \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N))$
102		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)$
103	28 102	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) Fn (1 \dots N)$
104	103	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) Fn (1 \dots N)$
105		fzss1	$⊢ y + 1 \in ℤ_{\geq 1} \to (y + 1 \dots N) \subseteq (1 \dots N)$
106	76 105	syl	$⊢ y \in (0 \dots N - 1) \to (y + 1 \dots N) \subseteq (1 \dots N)$
107	106	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to (y + 1 \dots N) \subseteq (1 \dots N)$
108		eluzp1p1	$⊢ N - 1 \in ℤ_{\geq y} \to N - 1 + 1 \in ℤ_{\geq (y + 1)}$
109		uzss	$⊢ N - 1 + 1 \in ℤ_{\geq (y + 1)} \to ℤ_{\geq (N - 1 + 1)} \subseteq ℤ_{\geq (y + 1)}$
110	82 108 109	3syl	$⊢ y \in (0 \dots N - 1) \to ℤ_{\geq (N - 1 + 1)} \subseteq ℤ_{\geq (y + 1)}$
111	110	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to ℤ_{\geq (N - 1 + 1)} \subseteq ℤ_{\geq (y + 1)}$
112	1	nnzd	$⊢ φ \to N \in ℤ$
113	112	uzidd	$⊢ φ \to N \in ℤ_{\geq N}$
114	80	fveq2d	$⊢ φ \to ℤ_{\geq (N - 1 + 1)} = ℤ_{\geq N}$
115	113 114	eleqtrrd	$⊢ φ \to N \in ℤ_{\geq (N - 1 + 1)}$
116	115	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to N \in ℤ_{\geq (N - 1 + 1)}$
117	111 116	sseldd	$⊢ (φ \land y \in (0 \dots N - 1)) \to N \in ℤ_{\geq (y + 1)}$
118		eluzfz2	$⊢ N \in ℤ_{\geq (y + 1)} \to N \in (y + 1 \dots N)$
119	117 118	syl	$⊢ (φ \land y \in (0 \dots N - 1)) \to N \in (y + 1 \dots N)$
120		fnfvima	$⊢ (2^{nd} (1^{st} (T)) Fn (1 \dots N) \land (y + 1 \dots N) \subseteq (1 \dots N) \land N \in (y + 1 \dots N)) \to 2^{nd} (1^{st} (T)) (N) \in 2^{nd} (1^{st} (T)) [(y + 1 \dots N)]$
121	104 107 119 120	syl3anc	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (T)) (N) \in 2^{nd} (1^{st} (T)) [(y + 1 \dots N)]$
122		fvun2	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots y)] \land (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \land (2^{nd} (1^{st} (T)) [(1 \dots y)] \cap 2^{nd} (1^{st} (T)) [(y + 1 \dots N)] = \emptyset \land 2^{nd} (1^{st} (T)) (N) \in 2^{nd} (1^{st} (T)) [(y + 1 \dots N)])) \to ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (N)) = (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (N))$
123	51 54 122	mp3an12	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots y)] \cap 2^{nd} (1^{st} (T)) [(y + 1 \dots N)] = \emptyset \land 2^{nd} (1^{st} (T)) (N) \in 2^{nd} (1^{st} (T)) [(y + 1 \dots N)]) \to ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (N)) = (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (N))$
124	69 121 123	syl2anc	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (N)) = (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (N))$
125	52	fvconst2	$⊢ 2^{nd} (1^{st} (T)) (N) \in 2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \to (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (N)) = 0$
126	121 125	syl	$⊢ (φ \land y \in (0 \dots N - 1)) \to (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (N)) = 0$
127	124 126	eqtrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (N)) = 0$
128	127	adantr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (1^{st} (T)) (N) \in (1 \dots N)) \to ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (N)) = 0$
129	48 97 99 99 100 101 128	ofval	$⊢ ((φ \land y \in (0 \dots N - 1)) \land 2^{nd} (1^{st} (T)) (N) \in (1 \dots N)) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))) (2^{nd} (1^{st} (T)) (N)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) + 0$
130	33 129	mpidan	$⊢ (φ \land y \in (0 \dots N - 1)) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))) (2^{nd} (1^{st} (T)) (N)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) + 0$
131	36	nn0cnd	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \in ℂ$
132	131	addridd	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) + 0 = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N))$
133	132	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) + 0 = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N))$
134	130 133	eqtrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))) (2^{nd} (1^{st} (T)) (N)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N))$
135	46 134	sylan9eqr	$⊢ ((φ \land y \in (0 \dots N - 1)) \land p = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))) \to p (2^{nd} (1^{st} (T)) (N)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N))$
136	135	adantllr	$⊢ (((φ \land p \in ran F) \land y \in (0 \dots N - 1)) \land p = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))) \to p (2^{nd} (1^{st} (T)) (N)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N))$
137		fveq2	$⊢ t = T \to 2^{nd} (t) = 2^{nd} (T)$
138	137	breq2d	$⊢ t = T \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (T))$
139	138	ifbid	$⊢ t = T \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (T), y, y + 1)$
140		2fveq3	$⊢ t = T \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T))$
141		2fveq3	$⊢ t = T \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T))$
142	141	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots j)]$
143	142	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}$
144	141	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)]$
145	144	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\}$
146	143 145	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\})$
147	140 146	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\}))$
148	139 147	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\})))$
149	148	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\}))))$
150	149	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\})))))$
151	150 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\})))))$
152	151	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\}))))$
153	4 152	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\}))))$
154	62	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to y \in ℝ$
155		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
156	112 155	syl	$⊢ φ \to N - 1 \in ℤ$
157	156	zred	$⊢ φ \to N - 1 \in ℝ$
158	157	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to N - 1 \in ℝ$
159	1	nnred	$⊢ φ \to N \in ℝ$
160	159	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to N \in ℝ$
161		elfzle2	$⊢ y \in (0 \dots N - 1) \to y \leq N - 1$
162	161	adantl	$⊢ (φ \land y \in (0 \dots N - 1)) \to y \leq N - 1$
163	159	ltm1d	$⊢ φ \to N - 1 < N$
164	163	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to N - 1 < N$
165	154 158 160 162 164	lelttrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to y < N$
166	6	adantr	$⊢ (φ \land y \in (0 \dots N - 1)) \to 2^{nd} (T) = N$
167	165 166	breqtrrd	$⊢ (φ \land y \in (0 \dots N - 1)) \to y < 2^{nd} (T)$
168	167	iftrued	$⊢ (φ \land y \in (0 \dots N - 1)) \to if (y < 2^{nd} (T), y, y + 1) = y$
169	168	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 / 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\})))$
170		vex	$⊢ y \in V$
171		oveq2	$⊢ j = y \to (1 \dots j) = (1 \dots y)$
172	171	imaeq2d	$⊢ j = y \to 2^{nd} (1^{st} (T)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots y)]$
173	172	xpeq1d	$⊢ j = y \to 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}$
174		oveq1	$⊢ j = y \to j + 1 = y + 1$
175	174	oveq1d	$⊢ j = y \to (j + 1 \dots N) = (y + 1 \dots N)$
176	175	imaeq2d	$⊢ j = y \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(y + 1 \dots N)]$
177	176	xpeq1d	$⊢ j = y \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}$
178	173 177	uneq12d	$⊢ j = y \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)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})$
179	178	oveq2d	$⊢ j = y \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)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))$
180	170 179	csbie	$⊢ ⦋ y / 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)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))$
181	169 180	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)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))$
182	181	mpteq2dva	$⊢ φ \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) ⟼ 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})))$
183	153 182	eqtrd	$⊢ φ \to F = (y \in (0 \dots N - 1) ⟼ 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})))$
184	183	rneqd	$⊢ φ \to ran F = ran (y \in (0 \dots N - 1) ⟼ 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})))$
185	184	eleq2d	$⊢ φ \to (p \in ran F \leftrightarrow p \in ran (y \in (0 \dots N - 1) ⟼ 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))))$
186		eqid	$⊢ (y \in (0 \dots N - 1) ⟼ 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))) = (y \in (0 \dots N - 1) ⟼ 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})))$
187		ovex	$⊢ 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})) \in V$
188	186 187	elrnmpti	$⊢ p \in ran (y \in (0 \dots N - 1) ⟼ 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))) \leftrightarrow \exists y \in (0 \dots N - 1) p = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))$
189	185 188	bitrdi	$⊢ φ \to (p \in ran F \leftrightarrow \exists y \in (0 \dots N - 1) p = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\})))$
190	189	biimpa	$⊢ (φ \land p \in ran F) \to \exists y \in (0 \dots N - 1) p = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots y)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(y + 1 \dots N)] \times \{0\}))$
191	136 190	r19.29a	$⊢ (φ \land p \in ran F) \to p (2^{nd} (1^{st} (T)) (N)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N))$
192	191	neeq1d	$⊢ (φ \land p \in ran F) \to (p (2^{nd} (1^{st} (T)) (N)) \neq 0 \leftrightarrow 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \neq 0)$
193	192	biimpd	$⊢ (φ \land p \in ran F) \to (p (2^{nd} (1^{st} (T)) (N)) \neq 0 \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \neq 0)$
194	193	rexlimdva	$⊢ φ \to (\exists p \in ran F p (2^{nd} (1^{st} (T)) (N)) \neq 0 \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \neq 0)$
195	45 194	mpd	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \neq 0$
196		elnnne0	$⊢ 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \in ℕ \leftrightarrow (1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \in ℕ_{0} \land 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \neq 0)$
197	36 195 196	sylanbrc	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \in ℕ$
198		nnm1nn0	$⊢ 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \in ℕ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) - 1 \in ℕ_{0}$
199	197 198	syl	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) - 1 \in ℕ_{0}$
200		elfzo0	$⊢ 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \in (0 ..^K) \leftrightarrow (1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \in ℕ_{0} \land K \in ℕ \land 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) < K)$
201	34 200	sylib	$⊢ φ \to (1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \in ℕ_{0} \land K \in ℕ \land 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) < K)$
202	201	simp2d	$⊢ φ \to K \in ℕ$
203	199	nn0red	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) - 1 \in ℝ$
204	36	nn0red	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \in ℝ$
205	202	nnred	$⊢ φ \to K \in ℝ$
206	204	ltm1d	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) - 1 < 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N))$
207		elfzolt2	$⊢ 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) \in (0 ..^K) \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) < K$
208	34 207	syl	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) < K$
209	203 204 205 206 208	lttrd	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) - 1 < K$
210		elfzo0	$⊢ 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) - 1 \in (0 ..^K) \leftrightarrow (1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) - 1 \in ℕ_{0} \land K \in ℕ \land 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) - 1 < K)$
211	199 202 209 210	syl3anbrc	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) - 1 \in (0 ..^K)$
212	211	adantr	$⊢ (φ \land n = 2^{nd} (1^{st} (T)) (N)) \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (N)) - 1 \in (0 ..^K)$
213	13 212	eqeltrd	$⊢ (φ \land n = 2^{nd} (1^{st} (T)) (N)) \to 1^{st} (1^{st} (T)) (n) - 1 \in (0 ..^K)$
214	213	adantlr	$⊢ ((φ \land n \in (1 \dots N)) \land n = 2^{nd} (1^{st} (T)) (N)) \to 1^{st} (1^{st} (T)) (n) - 1 \in (0 ..^K)$
215	22	ffvelcdmda	$⊢ (φ \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) \in (0 ..^K)$
216		elfzonn0	$⊢ 1^{st} (1^{st} (T)) (n) \in (0 ..^K) \to 1^{st} (1^{st} (T)) (n) \in ℕ_{0}$
217	215 216	syl	$⊢ (φ \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) \in ℕ_{0}$
218	217	nn0cnd	$⊢ (φ \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) \in ℂ$
219	218	subid1d	$⊢ (φ \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) - 0 = 1^{st} (1^{st} (T)) (n)$
220	219 215	eqeltrd	$⊢ (φ \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) - 0 \in (0 ..^K)$
221	220	adantr	$⊢ ((φ \land n \in (1 \dots N)) \land \neg n = 2^{nd} (1^{st} (T)) (N)) \to 1^{st} (1^{st} (T)) (n) - 0 \in (0 ..^K)$
222	8 10 214 221	ifbothda	$⊢ (φ \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0) \in (0 ..^K)$
223	222	fmpttd	$⊢ φ \to (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) : (1 \dots N) ⟶ (0 ..^K)$
224		ovex	$⊢ (0 ..^K) \in V$
225	224 98	elmap	$⊢ (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) \in ({(0 ..^K)}^{(1 \dots N)}) \leftrightarrow (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) : (1 \dots N) ⟶ (0 ..^K)$
226	223 225	sylibr	$⊢ φ \to (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) \in ({(0 ..^K)}^{(1 \dots N)})$
227		simpr	$⊢ (φ \land n \in (1 + 1 \dots N)) \to n \in (1 + 1 \dots N)$
228		1z	$⊢ 1 \in ℤ$
229		peano2z	$⊢ 1 \in ℤ \to 1 + 1 \in ℤ$
230	228 229	ax-mp	$⊢ 1 + 1 \in ℤ$
231	112 230	jctil	$⊢ φ \to (1 + 1 \in ℤ \land N \in ℤ)$
232		elfzelz	$⊢ n \in (1 + 1 \dots N) \to n \in ℤ$
233	232 228	jctir	$⊢ n \in (1 + 1 \dots N) \to (n \in ℤ \land 1 \in ℤ)$
234		fzsubel	$⊢ ((1 + 1 \in ℤ \land N \in ℤ) \land (n \in ℤ \land 1 \in ℤ)) \to (n \in (1 + 1 \dots N) \leftrightarrow n - 1 \in (1 + 1 - 1 \dots N - 1))$
235	231 233 234	syl2an	$⊢ (φ \land n \in (1 + 1 \dots N)) \to (n \in (1 + 1 \dots N) \leftrightarrow n - 1 \in (1 + 1 - 1 \dots N - 1))$
236	227 235	mpbid	$⊢ (φ \land n \in (1 + 1 \dots N)) \to n - 1 \in (1 + 1 - 1 \dots N - 1)$
237		ax-1cn	$⊢ 1 \in ℂ$
238	237 237	pncan3oi	$⊢ 1 + 1 - 1 = 1$
239	238	oveq1i	$⊢ (1 + 1 - 1 \dots N - 1) = (1 \dots N - 1)$
240	236 239	eleqtrdi	$⊢ (φ \land n \in (1 + 1 \dots N)) \to n - 1 \in (1 \dots N - 1)$
241	240	ralrimiva	$⊢ φ \to \forall n \in (1 + 1 \dots N) n - 1 \in (1 \dots N - 1)$
242		simpr	$⊢ (φ \land y \in (1 \dots N - 1)) \to y \in (1 \dots N - 1)$
243	156 228	jctil	$⊢ φ \to (1 \in ℤ \land N - 1 \in ℤ)$
244		elfzelz	$⊢ y \in (1 \dots N - 1) \to y \in ℤ$
245	244 228	jctir	$⊢ y \in (1 \dots N - 1) \to (y \in ℤ \land 1 \in ℤ)$
246		fzaddel	$⊢ ((1 \in ℤ \land N - 1 \in ℤ) \land (y \in ℤ \land 1 \in ℤ)) \to (y \in (1 \dots N - 1) \leftrightarrow y + 1 \in (1 + 1 \dots N - 1 + 1))$
247	243 245 246	syl2an	$⊢ (φ \land y \in (1 \dots N - 1)) \to (y \in (1 \dots N - 1) \leftrightarrow y + 1 \in (1 + 1 \dots N - 1 + 1))$
248	242 247	mpbid	$⊢ (φ \land y \in (1 \dots N - 1)) \to y + 1 \in (1 + 1 \dots N - 1 + 1)$
249	80	oveq2d	$⊢ φ \to (1 + 1 \dots N - 1 + 1) = (1 + 1 \dots N)$
250	249	adantr	$⊢ (φ \land y \in (1 \dots N - 1)) \to (1 + 1 \dots N - 1 + 1) = (1 + 1 \dots N)$
251	248 250	eleqtrd	$⊢ (φ \land y \in (1 \dots N - 1)) \to y + 1 \in (1 + 1 \dots N)$
252	232	zcnd	$⊢ n \in (1 + 1 \dots N) \to n \in ℂ$
253	244	zcnd	$⊢ y \in (1 \dots N - 1) \to y \in ℂ$
254		subadd2	$⊢ (n \in ℂ \land 1 \in ℂ \land y \in ℂ) \to (n - 1 = y \leftrightarrow y + 1 = n)$
255	237 254	mp3an2	$⊢ (n \in ℂ \land y \in ℂ) \to (n - 1 = y \leftrightarrow y + 1 = n)$
256		eqcom	$⊢ y = n - 1 \leftrightarrow n - 1 = y$
257		eqcom	$⊢ n = y + 1 \leftrightarrow y + 1 = n$
258	255 256 257	3bitr4g	$⊢ (n \in ℂ \land y \in ℂ) \to (y = n - 1 \leftrightarrow n = y + 1)$
259	252 253 258	syl2anr	$⊢ (y \in (1 \dots N - 1) \land n \in (1 + 1 \dots N)) \to (y = n - 1 \leftrightarrow n = y + 1)$
260	259	ralrimiva	$⊢ y \in (1 \dots N - 1) \to \forall n \in (1 + 1 \dots N) (y = n - 1 \leftrightarrow n = y + 1)$
261	260	adantl	$⊢ (φ \land y \in (1 \dots N - 1)) \to \forall n \in (1 + 1 \dots N) (y = n - 1 \leftrightarrow n = y + 1)$
262		reu6i	$⊢ (y + 1 \in (1 + 1 \dots N) \land \forall n \in (1 + 1 \dots N) (y = n - 1 \leftrightarrow n = y + 1)) \to \exists! n \in (1 + 1 \dots N) y = n - 1$
263	251 261 262	syl2anc	$⊢ (φ \land y \in (1 \dots N - 1)) \to \exists! n \in (1 + 1 \dots N) y = n - 1$
264	263	ralrimiva	$⊢ φ \to \forall y \in (1 \dots N - 1) \exists! n \in (1 + 1 \dots N) y = n - 1$
265		eqid	$⊢ (n \in (1 + 1 \dots N) ⟼ n - 1) = (n \in (1 + 1 \dots N) ⟼ n - 1)$
266	265	f1ompt	$⊢ (n \in (1 + 1 \dots N) ⟼ n - 1) : (1 + 1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N - 1) \leftrightarrow (\forall n \in (1 + 1 \dots N) n - 1 \in (1 \dots N - 1) \land \forall y \in (1 \dots N - 1) \exists! n \in (1 + 1 \dots N) y = n - 1)$
267	241 264 266	sylanbrc	$⊢ φ \to (n \in (1 + 1 \dots N) ⟼ n - 1) : (1 + 1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N - 1)$
268		f1osng	$⊢ (1 \in V \land N \in ℕ) \to \{⟨1, N⟩\} : \{1\} \underset{1-1 onto}{⟶} \{N\}$
269	49 1 268	sylancr	$⊢ φ \to \{⟨1, N⟩\} : \{1\} \underset{1-1 onto}{⟶} \{N\}$
270	157 159	ltnled	$⊢ φ \to (N - 1 < N \leftrightarrow \neg N \leq N - 1)$
271	163 270	mpbid	$⊢ φ \to \neg N \leq N - 1$
272		elfzle2	$⊢ N \in (1 \dots N - 1) \to N \leq N - 1$
273	271 272	nsyl	$⊢ φ \to \neg N \in (1 \dots N - 1)$
274		disjsn	$⊢ (1 \dots N - 1) \cap \{N\} = \emptyset \leftrightarrow \neg N \in (1 \dots N - 1)$
275	273 274	sylibr	$⊢ φ \to (1 \dots N - 1) \cap \{N\} = \emptyset$
276		1re	$⊢ 1 \in ℝ$
277	276	ltp1i	$⊢ 1 < 1 + 1$
278	230	zrei	$⊢ 1 + 1 \in ℝ$
279	276 278	ltnlei	$⊢ 1 < 1 + 1 \leftrightarrow \neg 1 + 1 \leq 1$
280	277 279	mpbi	$⊢ \neg 1 + 1 \leq 1$
281		elfzle1	$⊢ 1 \in (1 + 1 \dots N) \to 1 + 1 \leq 1$
282	280 281	mto	$⊢ \neg 1 \in (1 + 1 \dots N)$
283		disjsn	$⊢ (1 + 1 \dots N) \cap \{1\} = \emptyset \leftrightarrow \neg 1 \in (1 + 1 \dots N)$
284	282 283	mpbir	$⊢ (1 + 1 \dots N) \cap \{1\} = \emptyset$
285		f1oun	$⊢ (((n \in (1 + 1 \dots N) ⟼ n - 1) : (1 + 1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N - 1) \land \{⟨1, N⟩\} : \{1\} \underset{1-1 onto}{⟶} \{N\}) \land ((1 + 1 \dots N) \cap \{1\} = \emptyset \land (1 \dots N - 1) \cap \{N\} = \emptyset)) \to ((n \in (1 + 1 \dots N) ⟼ n - 1) \cup \{⟨1, N⟩\}) : (1 + 1 \dots N) \cup \{1\} \underset{1-1 onto}{⟶} (1 \dots N - 1) \cup \{N\}$
286	284 285	mpanr1	$⊢ (((n \in (1 + 1 \dots N) ⟼ n - 1) : (1 + 1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N - 1) \land \{⟨1, N⟩\} : \{1\} \underset{1-1 onto}{⟶} \{N\}) \land (1 \dots N - 1) \cap \{N\} = \emptyset) \to ((n \in (1 + 1 \dots N) ⟼ n - 1) \cup \{⟨1, N⟩\}) : (1 + 1 \dots N) \cup \{1\} \underset{1-1 onto}{⟶} (1 \dots N - 1) \cup \{N\}$
287	267 269 275 286	syl21anc	$⊢ φ \to ((n \in (1 + 1 \dots N) ⟼ n - 1) \cup \{⟨1, N⟩\}) : (1 + 1 \dots N) \cup \{1\} \underset{1-1 onto}{⟶} (1 \dots N - 1) \cup \{N\}$
288		eleq1	$⊢ n = 1 \to (n \in (1 + 1 \dots N) \leftrightarrow 1 \in (1 + 1 \dots N))$
289	282 288	mtbiri	$⊢ n = 1 \to \neg n \in (1 + 1 \dots N)$
290	289	necon2ai	$⊢ n \in (1 + 1 \dots N) \to n \neq 1$
291		ifnefalse	$⊢ n \neq 1 \to if (n = 1, N, n - 1) = n - 1$
292	290 291	syl	$⊢ n \in (1 + 1 \dots N) \to if (n = 1, N, n - 1) = n - 1$
293	292	mpteq2ia	$⊢ (n \in (1 + 1 \dots N) ⟼ if (n = 1, N, n - 1)) = (n \in (1 + 1 \dots N) ⟼ n - 1)$
294	293	uneq1i	$⊢ (n \in (1 + 1 \dots N) ⟼ if (n = 1, N, n - 1)) \cup \{⟨1, N⟩\} = (n \in (1 + 1 \dots N) ⟼ n - 1) \cup \{⟨1, N⟩\}$
295	49	a1i	$⊢ φ \to 1 \in V$
296	1 74	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
297		fzpred	$⊢ N \in ℤ_{\geq 1} \to (1 \dots N) = \{1\} \cup (1 + 1 \dots N)$
298	296 297	syl	$⊢ φ \to (1 \dots N) = \{1\} \cup (1 + 1 \dots N)$
299		uncom	$⊢ \{1\} \cup (1 + 1 \dots N) = (1 + 1 \dots N) \cup \{1\}$
300	298 299	eqtr2di	$⊢ φ \to (1 + 1 \dots N) \cup \{1\} = (1 \dots N)$
301		iftrue	$⊢ n = 1 \to if (n = 1, N, n - 1) = N$
302	301	adantl	$⊢ (φ \land n = 1) \to if (n = 1, N, n - 1) = N$
303	295 1 300 302	fmptapd	$⊢ φ \to (n \in (1 + 1 \dots N) ⟼ if (n = 1, N, n - 1)) \cup \{⟨1, N⟩\} = (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))$
304	294 303	eqtr3id	$⊢ φ \to (n \in (1 + 1 \dots N) ⟼ n - 1) \cup \{⟨1, N⟩\} = (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))$
305	80 296	eqeltrd	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq 1}$
306		uzid	$⊢ N - 1 \in ℤ \to N - 1 \in ℤ_{\geq (N - 1)}$
307		peano2uz	$⊢ N - 1 \in ℤ_{\geq (N - 1)} \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
308	156 306 307	3syl	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
309	80 308	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq (N - 1)}$
310		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)$
311	305 309 310	syl2anc	$⊢ φ \to (1 \dots N) = (1 \dots N - 1) \cup (N - 1 + 1 \dots N)$
312	80	oveq1d	$⊢ φ \to (N - 1 + 1 \dots N) = (N \dots N)$
313		fzsn	$⊢ N \in ℤ \to (N \dots N) = \{N\}$
314	112 313	syl	$⊢ φ \to (N \dots N) = \{N\}$
315	312 314	eqtrd	$⊢ φ \to (N - 1 + 1 \dots N) = \{N\}$
316	315	uneq2d	$⊢ φ \to (1 \dots N - 1) \cup (N - 1 + 1 \dots N) = (1 \dots N - 1) \cup \{N\}$
317	311 316	eqtr2d	$⊢ φ \to (1 \dots N - 1) \cup \{N\} = (1 \dots N)$
318	304 300 317	f1oeq123d	$⊢ φ \to (((n \in (1 + 1 \dots N) ⟼ n - 1) \cup \{⟨1, N⟩\}) : (1 + 1 \dots N) \cup \{1\} \underset{1-1 onto}{⟶} (1 \dots N - 1) \cup \{N\} \leftrightarrow (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
319	287 318	mpbid	$⊢ φ \to (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
320		f1oco	$⊢ (2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land (n \in (1 \dots N) ⟼ if (n = 1, N, 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 = 1, N, n - 1))) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
321	28 319 320	syl2anc	$⊢ φ \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
322	98	mptex	$⊢ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1)) \in V$
323	25 322	coex	$⊢ 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1)) \in V$
324		f1oeq1	$⊢ f = 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1)) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
325	323 324	elab	$⊢ 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
326	321 325	sylibr	$⊢ φ \to 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
327	226 326	opelxpd	$⊢ φ \to ⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩ \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
328	1	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
329		0elfz	$⊢ N \in ℕ_{0} \to 0 \in (0 \dots N)$
330	328 329	syl	$⊢ φ \to 0 \in (0 \dots N)$
331	327 330	opelxpd	$⊢ φ \to ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
332	1 2 3 4 5 6	poimirlem19	$⊢ φ \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)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots y + 1)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(y + 1 + 1 \dots N)] \times \{0\})))$
333		elfzle1	$⊢ y \in (0 \dots N - 1) \to 0 \leq y$
334		0re	$⊢ 0 \in ℝ$
335		lenlt	$⊢ (0 \in ℝ \land y \in ℝ) \to (0 \leq y \leftrightarrow \neg y < 0)$
336	334 62 335	sylancr	$⊢ y \in (0 \dots N - 1) \to (0 \leq y \leftrightarrow \neg y < 0)$
337	333 336	mpbid	$⊢ y \in (0 \dots N - 1) \to \neg y < 0$
338	337	iffalsed	$⊢ y \in (0 \dots N - 1) \to if (y < 0, y, y + 1) = y + 1$
339	338	csbeq1d	$⊢ y \in (0 \dots N - 1) \to ⦋ if (y < 0, y, y + 1) / j ⦌ ((n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] \times \{0\}))) = ⦋ (y + 1) / j ⦌ ((n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] \times \{0\})))$
340		ovex	$⊢ y + 1 \in V$
341		oveq2	$⊢ j = y + 1 \to (1 \dots j) = (1 \dots y + 1)$
342	341	imaeq2d	$⊢ j = y + 1 \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] = (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots y + 1)]$
343	342	xpeq1d	$⊢ j = y + 1 \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] \times \{1\} = (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots y + 1)] \times \{1\}$
344		oveq1	$⊢ j = y + 1 \to j + 1 = y + 1 + 1$
345	344	oveq1d	$⊢ j = y + 1 \to (j + 1 \dots N) = (y + 1 + 1 \dots N)$
346	345	imaeq2d	$⊢ j = y + 1 \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] = (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(y + 1 + 1 \dots N)]$
347	346	xpeq1d	$⊢ j = y + 1 \to (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] \times \{0\} = (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(y + 1 + 1 \dots N)] \times \{0\}$
348	343 347	uneq12d	$⊢ j = y + 1 \to ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] \times \{0\}) = ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots y + 1)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(y + 1 + 1 \dots N)] \times \{0\})$
349	348	oveq2d	$⊢ j = y + 1 \to (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] \times \{0\})) = (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots y + 1)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(y + 1 + 1 \dots N)] \times \{0\}))$
350	340 349	csbie	$⊢ ⦋ (y + 1) / j ⦌ ((n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] \times \{0\}))) = (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots y + 1)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(y + 1 + 1 \dots N)] \times \{0\}))$
351	339 350	eqtrdi	$⊢ y \in (0 \dots N - 1) \to ⦋ if (y < 0, y, y + 1) / j ⦌ ((n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] \times \{0\}))) = (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots y + 1)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(y + 1 + 1 \dots N)] \times \{0\}))$
352	351	mpteq2ia	$⊢ (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 0, y, y + 1) / j ⦌ ((n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] \times \{0\})))) = (y \in (0 \dots N - 1) ⟼ (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots y + 1)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(y + 1 + 1 \dots N)] \times \{0\})))$
353	332 352	eqtr4di	$⊢ φ \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 0, y, y + 1) / j ⦌ ((n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] \times \{0\}))))$
354		opex	$⊢ ⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩ \in V$
355	354 52	op2ndd	$⊢ t = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \to 2^{nd} (t) = 0$
356	355	breq2d	$⊢ t = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \to (y < 2^{nd} (t) \leftrightarrow y < 0)$
357	356	ifbid	$⊢ t = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \to if (y < 2^{nd} (t), y, y + 1) = if (y < 0, y, y + 1)$
358	354 52	op1std	$⊢ t = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \to 1^{st} (t) = ⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩$
359	98	mptex	$⊢ (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) \in V$
360	359 323	op1std	$⊢ 1^{st} (t) = ⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩ \to 1^{st} (1^{st} (t)) = (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0))$
361	358 360	syl	$⊢ t = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \to 1^{st} (1^{st} (t)) = (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0))$
362	359 323	op2ndd	$⊢ 1^{st} (t) = ⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩ \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))$
363	358 362	syl	$⊢ t = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))$
364	363	imaeq1d	$⊢ t = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)]$
365	364	xpeq1d	$⊢ t = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] \times \{1\}$
366	363	imaeq1d	$⊢ t = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)]$
367	366	xpeq1d	$⊢ t = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\} = (2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] \times \{0\}$
368	365 367	uneq12d	$⊢ t = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \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)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] \times \{0\})$
369	361 368	oveq12d	$⊢ t = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \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\})) = (n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] \times \{0\}))$
370	357 369	csbeq12dv	$⊢ t = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \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 < 0, y, y + 1) / j ⦌ ((n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] \times \{0\})))$
371	370	mpteq2dv	$⊢ t = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \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 < 0, y, y + 1) / j ⦌ ((n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] \times \{0\}))))$
372	371	eqeq2d	$⊢ t = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \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 < 0, y, y + 1) / j ⦌ ((n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] \times \{0\})))))$
373	372 2	elrab2	$⊢ ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \in S \leftrightarrow (⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \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 < 0, y, y + 1) / j ⦌ ((n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)) +_{f} (((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(1 \dots j)] \times \{1\}) \cup ((2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))) [(j + 1 \dots N)] \times \{0\})))))$
374	331 353 373	sylanbrc	$⊢ φ \to ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \in S$
375	354 52	op2ndd	$⊢ T = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \to 2^{nd} (T) = 0$
376	375	eqcoms	$⊢ ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ = T \to 2^{nd} (T) = 0$
377	1	nnne0d	$⊢ φ \to N \neq 0$
378	377	necomd	$⊢ φ \to 0 \neq N$
379		neeq1	$⊢ 2^{nd} (T) = 0 \to (2^{nd} (T) \neq N \leftrightarrow 0 \neq N)$
380	378 379	syl5ibrcom	$⊢ φ \to (2^{nd} (T) = 0 \to 2^{nd} (T) \neq N)$
381	376 380	syl5	$⊢ φ \to (⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ = T \to 2^{nd} (T) \neq N)$
382	381	necon2d	$⊢ φ \to (2^{nd} (T) = N \to ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \neq T)$
383	6 382	mpd	$⊢ φ \to ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \neq T$
384		neeq1	$⊢ z = ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \to (z \neq T \leftrightarrow ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \neq T)$
385	384	rspcev	$⊢ (⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \in S \land ⟨⟨(n \in (1 \dots N) ⟼ 1^{st} (1^{st} (T)) (n) - if (n = 2^{nd} (1^{st} (T)) (N), 1, 0)), 2^{nd} (1^{st} (T)) \circ (n \in (1 \dots N) ⟼ if (n = 1, N, n - 1))⟩, 0⟩ \neq T) \to \exists z \in S z \neq T$
386	374 383 385	syl2anc	$⊢ φ \to \exists z \in S z \neq T$

Metamath Proof Explorer

Theorem poimirlem20

Proof