poimirlem17

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

Metamath Proof Explorer

Theorem poimirlem17

Proof