poimirlem22

Description: Lemma for poimir , that a given face belongs to exactly two simplices, provided it's not on the boundary of the cube. (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	poimir.0	$⊢ φ \to N \in ℕ$
	poimirlem22.s	$⊢ S = \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\}$
	poimirlem22.1	$⊢ φ \to F : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
	poimirlem22.2	$⊢ φ \to T \in S$
	poimirlem22.3	$⊢ (φ \land n \in (1 \dots N)) \to \exists p \in ran F p (n) \neq 0$
	poimirlem22.4	$⊢ (φ \land n \in (1 \dots N)) \to \exists p \in ran F p (n) \neq K$
Assertion	poimirlem22	$⊢ φ \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		poimirlem22.4	$⊢ (φ \land n \in (1 \dots N)) \to \exists p \in ran F p (n) \neq K$
7	1	adantr	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to N \in ℕ$
8	3	adantr	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to F : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
9	4	adantr	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to T \in S$
10		simpr	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to 2^{nd} (T) \in (1 \dots N - 1)$
11	7 2 8 9 10	poimirlem15	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \in S$
12		fveq2	$⊢ t = T \to 2^{nd} (t) = 2^{nd} (T)$
13	12	breq2d	$⊢ t = T \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (T))$
14	13	ifbid	$⊢ t = T \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (T), y, y + 1)$
15	14	csbeq1d	$⊢ 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\})))$
16		2fveq3	$⊢ t = T \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T))$
17		2fveq3	$⊢ t = T \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T))$
18	17	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots j)]$
19	18	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}$
20	17	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)]$
21	20	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\}$
22	19 21	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\})$
23	16 22	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\}))$
24	23	csbeq2dv	$⊢ 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\})))$
25	15 24	eqtrd	$⊢ 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\})))$
26	25	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\}))))$
27	26	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\})))))$
28	27 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\})))))$
29	28	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\}))))$
30	4 29	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\}))))$
31	30	adantr	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \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\}))))$
32		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))$
33	32 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))$
34	4 33	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))$
35		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)\})$
36	34 35	syl	$⊢ φ \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
37		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)})$
38	36 37	syl	$⊢ φ \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
39		elmapi	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
40	38 39	syl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
41		elfzoelz	$⊢ n \in (0 ..^K) \to n \in ℤ$
42	41	ssriv	$⊢ (0 ..^K) \subseteq ℤ$
43		fss	$⊢ (1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K) \land (0 ..^K) \subseteq ℤ) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ ℤ$
44	40 42 43	sylancl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ ℤ$
45	44	adantr	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ ℤ$
46		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)\}$
47	36 46	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
48		fvex	$⊢ 2^{nd} (1^{st} (T)) \in V$
49		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))$
50	48 49	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)$
51	47 50	sylib	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
52	51	adantr	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
53	7 31 45 52 10	poimirlem1	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to \neg \exists^{*} n \in (1 \dots N) F (2^{nd} (T) - 1) (n) \neq F (2^{nd} (T)) (n)$
54	53	adantr	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to \neg \exists^{*} n \in (1 \dots N) F (2^{nd} (T) - 1) (n) \neq F (2^{nd} (T)) (n)$
55	1	ad3antrrr	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land 2^{nd} (z) \neq 2^{nd} (T)) \to N \in ℕ$
56		fveq2	$⊢ t = z \to 2^{nd} (t) = 2^{nd} (z)$
57	56	breq2d	$⊢ t = z \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (z))$
58	57	ifbid	$⊢ t = z \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (z), y, y + 1)$
59	58	csbeq1d	$⊢ t = z \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} (z), 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\})))$
60		2fveq3	$⊢ t = z \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (z))$
61		2fveq3	$⊢ t = z \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (z))$
62	61	imaeq1d	$⊢ t = z \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (z)) [(1 \dots j)]$
63	62	xpeq1d	$⊢ t = z \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}$
64	61	imaeq1d	$⊢ t = z \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (z)) [(j + 1 \dots N)]$
65	64	xpeq1d	$⊢ t = z \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}$
66	63 65	uneq12d	$⊢ t = z \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} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\})$
67	60 66	oveq12d	$⊢ t = z \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} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}))$
68	67	csbeq2dv	$⊢ t = z \to ⦋ if (y < 2^{nd} (z), 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} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\})))$
69	59 68	eqtrd	$⊢ t = z \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} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\})))$
70	69	mpteq2dv	$⊢ t = z \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} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}))))$
71	70	eqeq2d	$⊢ t = z \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} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\})))))$
72	71 2	elrab2	$⊢ z \in S \leftrightarrow (z \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} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\})))))$
73	72	simprbi	$⊢ z \in S \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}))))$
74	73	ad2antlr	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land 2^{nd} (z) \neq 2^{nd} (T)) \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}))))$
75		elrabi	$⊢ z \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 z \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
76	75 2	eleq2s	$⊢ z \in S \to z \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
77		xp1st	$⊢ z \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} (z) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
78	76 77	syl	$⊢ z \in S \to 1^{st} (z) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
79		xp1st	$⊢ 1^{st} (z) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 1^{st} (1^{st} (z)) \in ({(0 ..^K)}^{(1 \dots N)})$
80	78 79	syl	$⊢ z \in S \to 1^{st} (1^{st} (z)) \in ({(0 ..^K)}^{(1 \dots N)})$
81		elmapi	$⊢ 1^{st} (1^{st} (z)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ (0 ..^K)$
82	80 81	syl	$⊢ z \in S \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ (0 ..^K)$
83		fss	$⊢ (1^{st} (1^{st} (z)) : (1 \dots N) ⟶ (0 ..^K) \land (0 ..^K) \subseteq ℤ) \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ ℤ$
84	82 42 83	sylancl	$⊢ z \in S \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ ℤ$
85	84	ad2antlr	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land 2^{nd} (z) \neq 2^{nd} (T)) \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ ℤ$
86		xp2nd	$⊢ 1^{st} (z) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 2^{nd} (1^{st} (z)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
87	78 86	syl	$⊢ z \in S \to 2^{nd} (1^{st} (z)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
88		fvex	$⊢ 2^{nd} (1^{st} (z)) \in V$
89		f1oeq1	$⊢ f = 2^{nd} (1^{st} (z)) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
90	88 89	elab	$⊢ 2^{nd} (1^{st} (z)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
91	87 90	sylib	$⊢ z \in S \to 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
92	91	ad2antlr	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land 2^{nd} (z) \neq 2^{nd} (T)) \to 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
93		simpllr	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land 2^{nd} (z) \neq 2^{nd} (T)) \to 2^{nd} (T) \in (1 \dots N - 1)$
94		xp2nd	$⊢ z \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \to 2^{nd} (z) \in (0 \dots N)$
95	76 94	syl	$⊢ z \in S \to 2^{nd} (z) \in (0 \dots N)$
96	95	adantl	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to 2^{nd} (z) \in (0 \dots N)$
97		eldifsn	$⊢ 2^{nd} (z) \in ((0 \dots N) ∖ \{2^{nd} (T)\}) \leftrightarrow (2^{nd} (z) \in (0 \dots N) \land 2^{nd} (z) \neq 2^{nd} (T))$
98	97	biimpri	$⊢ (2^{nd} (z) \in (0 \dots N) \land 2^{nd} (z) \neq 2^{nd} (T)) \to 2^{nd} (z) \in ((0 \dots N) ∖ \{2^{nd} (T)\})$
99	96 98	sylan	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land 2^{nd} (z) \neq 2^{nd} (T)) \to 2^{nd} (z) \in ((0 \dots N) ∖ \{2^{nd} (T)\})$
100	55 74 85 92 93 99	poimirlem2	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land 2^{nd} (z) \neq 2^{nd} (T)) \to \exists^{*} n \in (1 \dots N) F (2^{nd} (T) - 1) (n) \neq F (2^{nd} (T)) (n)$
101	100	ex	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to (2^{nd} (z) \neq 2^{nd} (T) \to \exists^{*} n \in (1 \dots N) F (2^{nd} (T) - 1) (n) \neq F (2^{nd} (T)) (n))$
102	101	necon1bd	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to (\neg \exists^{*} n \in (1 \dots N) F (2^{nd} (T) - 1) (n) \neq F (2^{nd} (T)) (n) \to 2^{nd} (z) = 2^{nd} (T))$
103	54 102	mpd	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to 2^{nd} (z) = 2^{nd} (T)$
104		eleq1	$⊢ 2^{nd} (z) = 2^{nd} (T) \to (2^{nd} (z) \in (1 \dots N - 1) \leftrightarrow 2^{nd} (T) \in (1 \dots N - 1))$
105	104	biimparc	$⊢ (2^{nd} (T) \in (1 \dots N - 1) \land 2^{nd} (z) = 2^{nd} (T)) \to 2^{nd} (z) \in (1 \dots N - 1)$
106	105	anim2i	$⊢ (φ \land (2^{nd} (T) \in (1 \dots N - 1) \land 2^{nd} (z) = 2^{nd} (T))) \to (φ \land 2^{nd} (z) \in (1 \dots N - 1))$
107	106	anassrs	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land 2^{nd} (z) = 2^{nd} (T)) \to (φ \land 2^{nd} (z) \in (1 \dots N - 1))$
108	73	adantl	$⊢ ((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land z \in S) \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}))))$
109		breq1	$⊢ y = 0 \to (y < 2^{nd} (z) \leftrightarrow 0 < 2^{nd} (z))$
110		id	$⊢ y = 0 \to y = 0$
111	109 110	ifbieq1d	$⊢ y = 0 \to if (y < 2^{nd} (z), y, y + 1) = if (0 < 2^{nd} (z), 0, y + 1)$
112		elfznn	$⊢ 2^{nd} (z) \in (1 \dots N - 1) \to 2^{nd} (z) \in ℕ$
113	112	nngt0d	$⊢ 2^{nd} (z) \in (1 \dots N - 1) \to 0 < 2^{nd} (z)$
114	113	iftrued	$⊢ 2^{nd} (z) \in (1 \dots N - 1) \to if (0 < 2^{nd} (z), 0, y + 1) = 0$
115	114	ad2antlr	$⊢ ((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land z \in S) \to if (0 < 2^{nd} (z), 0, y + 1) = 0$
116	111 115	sylan9eqr	$⊢ (((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land z \in S) \land y = 0) \to if (y < 2^{nd} (z), y, y + 1) = 0$
117	116	csbeq1d	$⊢ (((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land z \in S) \land y = 0) \to ⦋ if (y < 2^{nd} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ 0 / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\})))$
118		c0ex	$⊢ 0 \in V$
119		oveq2	$⊢ j = 0 \to (1 \dots j) = (1 \dots 0)$
120		fz10	$⊢ (1 \dots 0) = \emptyset$
121	119 120	eqtrdi	$⊢ j = 0 \to (1 \dots j) = \emptyset$
122	121	imaeq2d	$⊢ j = 0 \to 2^{nd} (1^{st} (z)) [(1 \dots j)] = 2^{nd} (1^{st} (z)) [\emptyset]$
123	122	xpeq1d	$⊢ j = 0 \to 2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (z)) [\emptyset] \times \{1\}$
124		oveq1	$⊢ j = 0 \to j + 1 = 0 + 1$
125		0p1e1	$⊢ 0 + 1 = 1$
126	124 125	eqtrdi	$⊢ j = 0 \to j + 1 = 1$
127	126	oveq1d	$⊢ j = 0 \to (j + 1 \dots N) = (1 \dots N)$
128	127	imaeq2d	$⊢ j = 0 \to 2^{nd} (1^{st} (z)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (z)) [(1 \dots N)]$
129	128	xpeq1d	$⊢ j = 0 \to 2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (z)) [(1 \dots N)] \times \{0\}$
130	123 129	uneq12d	$⊢ j = 0 \to (2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (z)) [\emptyset] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(1 \dots N)] \times \{0\})$
131		ima0	$⊢ 2^{nd} (1^{st} (z)) [\emptyset] = \emptyset$
132	131	xpeq1i	$⊢ 2^{nd} (1^{st} (z)) [\emptyset] \times \{1\} = \emptyset \times \{1\}$
133		0xp	$⊢ \emptyset \times \{1\} = \emptyset$
134	132 133	eqtri	$⊢ 2^{nd} (1^{st} (z)) [\emptyset] \times \{1\} = \emptyset$
135	134	uneq1i	$⊢ (2^{nd} (1^{st} (z)) [\emptyset] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(1 \dots N)] \times \{0\}) = \emptyset \cup (2^{nd} (1^{st} (z)) [(1 \dots N)] \times \{0\})$
136		uncom	$⊢ \emptyset \cup (2^{nd} (1^{st} (z)) [(1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (z)) [(1 \dots N)] \times \{0\}) \cup \emptyset$
137		un0	$⊢ (2^{nd} (1^{st} (z)) [(1 \dots N)] \times \{0\}) \cup \emptyset = 2^{nd} (1^{st} (z)) [(1 \dots N)] \times \{0\}$
138	135 136 137	3eqtri	$⊢ (2^{nd} (1^{st} (z)) [\emptyset] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(1 \dots N)] \times \{0\}) = 2^{nd} (1^{st} (z)) [(1 \dots N)] \times \{0\}$
139	130 138	eqtrdi	$⊢ j = 0 \to (2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}) = 2^{nd} (1^{st} (z)) [(1 \dots N)] \times \{0\}$
140	139	oveq2d	$⊢ j = 0 \to 1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (z)) +_{f} (2^{nd} (1^{st} (z)) [(1 \dots N)] \times \{0\})$
141	118 140	csbie	$⊢ ⦋ 0 / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (z)) +_{f} (2^{nd} (1^{st} (z)) [(1 \dots N)] \times \{0\})$
142		f1ofo	$⊢ 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
143	91 142	syl	$⊢ z \in S \to 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
144		foima	$⊢ 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (z)) [(1 \dots N)] = (1 \dots N)$
145	143 144	syl	$⊢ z \in S \to 2^{nd} (1^{st} (z)) [(1 \dots N)] = (1 \dots N)$
146	145	xpeq1d	$⊢ z \in S \to 2^{nd} (1^{st} (z)) [(1 \dots N)] \times \{0\} = (1 \dots N) \times \{0\}$
147	146	oveq2d	$⊢ z \in S \to 1^{st} (1^{st} (z)) +_{f} (2^{nd} (1^{st} (z)) [(1 \dots N)] \times \{0\}) = 1^{st} (1^{st} (z)) +_{f} ((1 \dots N) \times \{0\})$
148		ovexd	$⊢ z \in S \to (1 \dots N) \in V$
149	82	ffnd	$⊢ z \in S \to 1^{st} (1^{st} (z)) Fn (1 \dots N)$
150		fnconstg	$⊢ 0 \in V \to ((1 \dots N) \times \{0\}) Fn (1 \dots N)$
151	118 150	mp1i	$⊢ z \in S \to ((1 \dots N) \times \{0\}) Fn (1 \dots N)$
152		eqidd	$⊢ (z \in S \land n \in (1 \dots N)) \to 1^{st} (1^{st} (z)) (n) = 1^{st} (1^{st} (z)) (n)$
153	118	fvconst2	$⊢ n \in (1 \dots N) \to ((1 \dots N) \times \{0\}) (n) = 0$
154	153	adantl	$⊢ (z \in S \land n \in (1 \dots N)) \to ((1 \dots N) \times \{0\}) (n) = 0$
155	82	ffvelrnda	$⊢ (z \in S \land n \in (1 \dots N)) \to 1^{st} (1^{st} (z)) (n) \in (0 ..^K)$
156		elfzonn0	$⊢ 1^{st} (1^{st} (z)) (n) \in (0 ..^K) \to 1^{st} (1^{st} (z)) (n) \in ℕ_{0}$
157	155 156	syl	$⊢ (z \in S \land n \in (1 \dots N)) \to 1^{st} (1^{st} (z)) (n) \in ℕ_{0}$
158	157	nn0cnd	$⊢ (z \in S \land n \in (1 \dots N)) \to 1^{st} (1^{st} (z)) (n) \in ℂ$
159	158	addid1d	$⊢ (z \in S \land n \in (1 \dots N)) \to 1^{st} (1^{st} (z)) (n) + 0 = 1^{st} (1^{st} (z)) (n)$
160	148 149 151 149 152 154 159	offveq	$⊢ z \in S \to 1^{st} (1^{st} (z)) +_{f} ((1 \dots N) \times \{0\}) = 1^{st} (1^{st} (z))$
161	147 160	eqtrd	$⊢ z \in S \to 1^{st} (1^{st} (z)) +_{f} (2^{nd} (1^{st} (z)) [(1 \dots N)] \times \{0\}) = 1^{st} (1^{st} (z))$
162	141 161	syl5eq	$⊢ z \in S \to ⦋ 0 / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (z))$
163	162	ad2antlr	$⊢ (((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land z \in S) \land y = 0) \to ⦋ 0 / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (z))$
164	117 163	eqtrd	$⊢ (((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land z \in S) \land y = 0) \to ⦋ if (y < 2^{nd} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (z))$
165		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
166	1 165	syl	$⊢ φ \to N - 1 \in ℕ_{0}$
167		0elfz	$⊢ N - 1 \in ℕ_{0} \to 0 \in (0 \dots N - 1)$
168	166 167	syl	$⊢ φ \to 0 \in (0 \dots N - 1)$
169	168	ad2antrr	$⊢ ((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land z \in S) \to 0 \in (0 \dots N - 1)$
170		fvexd	$⊢ ((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land z \in S) \to 1^{st} (1^{st} (z)) \in V$
171	108 164 169 170	fvmptd	$⊢ ((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land z \in S) \to F (0) = 1^{st} (1^{st} (z))$
172	107 171	sylan	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land 2^{nd} (z) = 2^{nd} (T)) \land z \in S) \to F (0) = 1^{st} (1^{st} (z))$
173	172	an32s	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land 2^{nd} (z) = 2^{nd} (T)) \to F (0) = 1^{st} (1^{st} (z))$
174	103 173	mpdan	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to F (0) = 1^{st} (1^{st} (z))$
175		fveq2	$⊢ z = T \to 2^{nd} (z) = 2^{nd} (T)$
176	175	eleq1d	$⊢ z = T \to (2^{nd} (z) \in (1 \dots N - 1) \leftrightarrow 2^{nd} (T) \in (1 \dots N - 1))$
177	176	anbi2d	$⊢ z = T \to ((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \leftrightarrow (φ \land 2^{nd} (T) \in (1 \dots N - 1)))$
178		2fveq3	$⊢ z = T \to 1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T))$
179	178	eqeq2d	$⊢ z = T \to (F (0) = 1^{st} (1^{st} (z)) \leftrightarrow F (0) = 1^{st} (1^{st} (T)))$
180	177 179	imbi12d	$⊢ z = T \to (((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \to F (0) = 1^{st} (1^{st} (z))) \leftrightarrow ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to F (0) = 1^{st} (1^{st} (T))))$
181	171	expcom	$⊢ z \in S \to ((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \to F (0) = 1^{st} (1^{st} (z)))$
182	180 181	vtoclga	$⊢ T \in S \to ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to F (0) = 1^{st} (1^{st} (T)))$
183	9 182	mpcom	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to F (0) = 1^{st} (1^{st} (T))$
184	183	adantr	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to F (0) = 1^{st} (1^{st} (T))$
185	174 184	eqtr3d	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to 1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T))$
186	185	adantr	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land z \neq T) \to 1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T))$
187	1	ad3antrrr	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land z \neq T) \to N \in ℕ$
188	4	ad3antrrr	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land z \neq T) \to T \in S$
189		simpllr	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land z \neq T) \to 2^{nd} (T) \in (1 \dots N - 1)$
190		simplr	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land z \neq T) \to z \in S$
191	36	adantr	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
192		xpopth	$⊢ (1^{st} (z) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land 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} (z)) = 1^{st} (1^{st} (T)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T))) \leftrightarrow 1^{st} (z) = 1^{st} (T))$
193	78 191 192	syl2anr	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to ((1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T))) \leftrightarrow 1^{st} (z) = 1^{st} (T))$
194	34	adantr	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \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))$
195		xpopth	$⊢ (z \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \land 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} (z) = 1^{st} (T) \land 2^{nd} (z) = 2^{nd} (T)) \leftrightarrow z = T)$
196	195	biimpd	$⊢ (z \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \land 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} (z) = 1^{st} (T) \land 2^{nd} (z) = 2^{nd} (T)) \to z = T)$
197	76 194 196	syl2anr	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to ((1^{st} (z) = 1^{st} (T) \land 2^{nd} (z) = 2^{nd} (T)) \to z = T)$
198	103 197	mpan2d	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to (1^{st} (z) = 1^{st} (T) \to z = T)$
199	193 198	sylbid	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to ((1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T))) \to z = T)$
200	185 199	mpand	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to (2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T)) \to z = T)$
201	200	necon3d	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to (z \neq T \to 2^{nd} (1^{st} (z)) \neq 2^{nd} (1^{st} (T)))$
202	201	imp	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land z \neq T) \to 2^{nd} (1^{st} (z)) \neq 2^{nd} (1^{st} (T))$
203	187 2 188 189 190 202	poimirlem9	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land z \neq T) \to 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))$
204	103	adantr	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land z \neq T) \to 2^{nd} (z) = 2^{nd} (T)$
205	186 203 204	jca31	$⊢ (((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \land z \neq T) \to ((1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) \land 2^{nd} (z) = 2^{nd} (T))$
206	205	ex	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to (z \neq T \to ((1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) \land 2^{nd} (z) = 2^{nd} (T)))$
207		simplr	$⊢ ((1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) \land 2^{nd} (z) = 2^{nd} (T)) \to 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))$
208		elfznn	$⊢ 2^{nd} (T) \in (1 \dots N - 1) \to 2^{nd} (T) \in ℕ$
209	208	nnred	$⊢ 2^{nd} (T) \in (1 \dots N - 1) \to 2^{nd} (T) \in ℝ$
210	209	ltp1d	$⊢ 2^{nd} (T) \in (1 \dots N - 1) \to 2^{nd} (T) < 2^{nd} (T) + 1$
211	209 210	ltned	$⊢ 2^{nd} (T) \in (1 \dots N - 1) \to 2^{nd} (T) \neq 2^{nd} (T) + 1$
212	211	adantl	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to 2^{nd} (T) \neq 2^{nd} (T) + 1$
213		fveq1	$⊢ 2^{nd} (1^{st} (T)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) \to 2^{nd} (1^{st} (T)) (2^{nd} (T)) = (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) (2^{nd} (T))$
214		id	$⊢ 2^{nd} (T) \in ℝ \to 2^{nd} (T) \in ℝ$
215		ltp1	$⊢ 2^{nd} (T) \in ℝ \to 2^{nd} (T) < 2^{nd} (T) + 1$
216	214 215	ltned	$⊢ 2^{nd} (T) \in ℝ \to 2^{nd} (T) \neq 2^{nd} (T) + 1$
217		fvex	$⊢ 2^{nd} (T) \in V$
218		ovex	$⊢ 2^{nd} (T) + 1 \in V$
219	217 218 218 217	fpr	$⊢ 2^{nd} (T) \neq 2^{nd} (T) + 1 \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ \{2^{nd} (T) + 1, 2^{nd} (T)\}$
220	216 219	syl	$⊢ 2^{nd} (T) \in ℝ \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ \{2^{nd} (T) + 1, 2^{nd} (T)\}$
221		f1oi	$⊢ ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) : (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
222		f1of	$⊢ ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) : (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \underset{1-1 onto}{⟶} (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \to ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) : (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
223	221 222	ax-mp	$⊢ ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) : (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
224		disjdif	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} \cap ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = \emptyset$
225		fun	$⊢ ((\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ \{2^{nd} (T) + 1, 2^{nd} (T)\} \land ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) : (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \land \{2^{nd} (T), 2^{nd} (T) + 1\} \cap ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = \emptyset) \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) : \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) ⟶ \{2^{nd} (T) + 1, 2^{nd} (T)\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
226	224 225	mpan2	$⊢ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} : \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ \{2^{nd} (T) + 1, 2^{nd} (T)\} \land ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) : (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} ⟶ (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) : \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) ⟶ \{2^{nd} (T) + 1, 2^{nd} (T)\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
227	220 223 226	sylancl	$⊢ 2^{nd} (T) \in ℝ \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) : \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) ⟶ \{2^{nd} (T) + 1, 2^{nd} (T)\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
228	217	prid1	$⊢ 2^{nd} (T) \in \{2^{nd} (T), 2^{nd} (T) + 1\}$
229		elun1	$⊢ 2^{nd} (T) \in \{2^{nd} (T), 2^{nd} (T) + 1\} \to 2^{nd} (T) \in (\{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}))$
230	228 229	ax-mp	$⊢ 2^{nd} (T) \in (\{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}))$
231		fvco3	$⊢ ((\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) : \{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) ⟶ \{2^{nd} (T) + 1, 2^{nd} (T)\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \land 2^{nd} (T) \in (\{2^{nd} (T), 2^{nd} (T) + 1\} \cup ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}))) \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) (2^{nd} (T)) = 2^{nd} (1^{st} (T)) ((\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) (2^{nd} (T)))$
232	227 230 231	sylancl	$⊢ 2^{nd} (T) \in ℝ \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) (2^{nd} (T)) = 2^{nd} (1^{st} (T)) ((\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) (2^{nd} (T)))$
233	220	ffnd	$⊢ 2^{nd} (T) \in ℝ \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} Fn \{2^{nd} (T), 2^{nd} (T) + 1\}$
234		fnresi	$⊢ ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) Fn ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
235	224 228	pm3.2i	$⊢ (\{2^{nd} (T), 2^{nd} (T) + 1\} \cap ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = \emptyset \land 2^{nd} (T) \in \{2^{nd} (T), 2^{nd} (T) + 1\})$
236		fvun1	$⊢ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} Fn \{2^{nd} (T), 2^{nd} (T) + 1\} \land ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) Fn ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \land (\{2^{nd} (T), 2^{nd} (T) + 1\} \cap ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = \emptyset \land 2^{nd} (T) \in \{2^{nd} (T), 2^{nd} (T) + 1\})) \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) (2^{nd} (T)) = \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} (2^{nd} (T))$
237	234 235 236	mp3an23	$⊢ \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} Fn \{2^{nd} (T), 2^{nd} (T) + 1\} \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) (2^{nd} (T)) = \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} (2^{nd} (T))$
238	233 237	syl	$⊢ 2^{nd} (T) \in ℝ \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) (2^{nd} (T)) = \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} (2^{nd} (T))$
239	217 218	fvpr1	$⊢ 2^{nd} (T) \neq 2^{nd} (T) + 1 \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} (2^{nd} (T)) = 2^{nd} (T) + 1$
240	216 239	syl	$⊢ 2^{nd} (T) \in ℝ \to \{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} (2^{nd} (T)) = 2^{nd} (T) + 1$
241	238 240	eqtrd	$⊢ 2^{nd} (T) \in ℝ \to (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) (2^{nd} (T)) = 2^{nd} (T) + 1$
242	241	fveq2d	$⊢ 2^{nd} (T) \in ℝ \to 2^{nd} (1^{st} (T)) ((\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) (2^{nd} (T))) = 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)$
243	232 242	eqtrd	$⊢ 2^{nd} (T) \in ℝ \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) (2^{nd} (T)) = 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)$
244	209 243	syl	$⊢ 2^{nd} (T) \in (1 \dots N - 1) \to (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) (2^{nd} (T)) = 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1)$
245	244	eqeq2d	$⊢ 2^{nd} (T) \in (1 \dots N - 1) \to (2^{nd} (1^{st} (T)) (2^{nd} (T)) = (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) (2^{nd} (T)) \leftrightarrow 2^{nd} (1^{st} (T)) (2^{nd} (T)) = 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1))$
246	245	adantl	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to (2^{nd} (1^{st} (T)) (2^{nd} (T)) = (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) (2^{nd} (T)) \leftrightarrow 2^{nd} (1^{st} (T)) (2^{nd} (T)) = 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1))$
247		f1of1	$⊢ 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{1-1}{⟶} (1 \dots N)$
248	51 247	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1}{⟶} (1 \dots N)$
249	248	adantr	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1}{⟶} (1 \dots N)$
250	1	nncnd	$⊢ φ \to N \in ℂ$
251		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
252	250 251	syl	$⊢ φ \to N - 1 + 1 = N$
253	166	nn0zd	$⊢ φ \to N - 1 \in ℤ$
254		uzid	$⊢ N - 1 \in ℤ \to N - 1 \in ℤ_{\geq (N - 1)}$
255	253 254	syl	$⊢ φ \to N - 1 \in ℤ_{\geq (N - 1)}$
256		peano2uz	$⊢ N - 1 \in ℤ_{\geq (N - 1)} \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
257	255 256	syl	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
258	252 257	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq (N - 1)}$
259		fzss2	$⊢ N \in ℤ_{\geq (N - 1)} \to (1 \dots N - 1) \subseteq (1 \dots N)$
260	258 259	syl	$⊢ φ \to (1 \dots N - 1) \subseteq (1 \dots N)$
261	260	sselda	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to 2^{nd} (T) \in (1 \dots N)$
262		fzp1elp1	$⊢ 2^{nd} (T) \in (1 \dots N - 1) \to 2^{nd} (T) + 1 \in (1 \dots N - 1 + 1)$
263	262	adantl	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to 2^{nd} (T) + 1 \in (1 \dots N - 1 + 1)$
264	252	oveq2d	$⊢ φ \to (1 \dots N - 1 + 1) = (1 \dots N)$
265	264	adantr	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to (1 \dots N - 1 + 1) = (1 \dots N)$
266	263 265	eleqtrd	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to 2^{nd} (T) + 1 \in (1 \dots N)$
267		f1veqaeq	$⊢ (2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1}{⟶} (1 \dots N) \land (2^{nd} (T) \in (1 \dots N) \land 2^{nd} (T) + 1 \in (1 \dots N))) \to (2^{nd} (1^{st} (T)) (2^{nd} (T)) = 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1) \to 2^{nd} (T) = 2^{nd} (T) + 1)$
268	249 261 266 267	syl12anc	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to (2^{nd} (1^{st} (T)) (2^{nd} (T)) = 2^{nd} (1^{st} (T)) (2^{nd} (T) + 1) \to 2^{nd} (T) = 2^{nd} (T) + 1)$
269	246 268	sylbid	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to (2^{nd} (1^{st} (T)) (2^{nd} (T)) = (2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) (2^{nd} (T)) \to 2^{nd} (T) = 2^{nd} (T) + 1)$
270	213 269	syl5	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to (2^{nd} (1^{st} (T)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) \to 2^{nd} (T) = 2^{nd} (T) + 1)$
271	270	necon3d	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to (2^{nd} (T) \neq 2^{nd} (T) + 1 \to 2^{nd} (1^{st} (T)) \neq 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})))$
272	212 271	mpd	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to 2^{nd} (1^{st} (T)) \neq 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))$
273		2fveq3	$⊢ z = T \to 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T))$
274	273	neeq1d	$⊢ z = T \to (2^{nd} (1^{st} (z)) \neq 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) \leftrightarrow 2^{nd} (1^{st} (T)) \neq 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})))$
275	272 274	syl5ibrcom	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to (z = T \to 2^{nd} (1^{st} (z)) \neq 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})))$
276	275	necon2d	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to (2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})})) \to z \neq T)$
277	207 276	syl5	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to (((1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) \land 2^{nd} (z) = 2^{nd} (T)) \to z \neq T)$
278	277	adantr	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to (((1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) \land 2^{nd} (z) = 2^{nd} (T)) \to z \neq T)$
279	206 278	impbid	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to (z \neq T \leftrightarrow ((1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) \land 2^{nd} (z) = 2^{nd} (T)))$
280		eqop	$⊢ z \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \to (z = ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \leftrightarrow (1^{st} (z) = ⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩ \land 2^{nd} (z) = 2^{nd} (T)))$
281		eqop	$⊢ 1^{st} (z) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to (1^{st} (z) = ⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩ \leftrightarrow (1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))))$
282	77 281	syl	$⊢ z \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} (z) = ⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩ \leftrightarrow (1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))))$
283	282	anbi1d	$⊢ z \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} (z) = ⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩ \land 2^{nd} (z) = 2^{nd} (T)) \leftrightarrow ((1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) \land 2^{nd} (z) = 2^{nd} (T)))$
284	280 283	bitrd	$⊢ z \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \to (z = ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \leftrightarrow ((1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) \land 2^{nd} (z) = 2^{nd} (T)))$
285	76 284	syl	$⊢ z \in S \to (z = ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \leftrightarrow ((1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) \land 2^{nd} (z) = 2^{nd} (T)))$
286	285	adantl	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to (z = ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \leftrightarrow ((1^{st} (1^{st} (z)) = 1^{st} (1^{st} (T)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))) \land 2^{nd} (z) = 2^{nd} (T)))$
287	279 286	bitr4d	$⊢ ((φ \land 2^{nd} (T) \in (1 \dots N - 1)) \land z \in S) \to (z \neq T \leftrightarrow z = ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩)$
288	287	ralrimiva	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to \forall z \in S (z \neq T \leftrightarrow z = ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩)$
289		reu6i	$⊢ (⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩ \in S \land \forall z \in S (z \neq T \leftrightarrow z = ⟨⟨1^{st} (1^{st} (T)), 2^{nd} (1^{st} (T)) \circ (\{⟨2^{nd} (T), 2^{nd} (T) + 1⟩, ⟨2^{nd} (T) + 1, 2^{nd} (T)⟩\} \cup ({I ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}))⟩, 2^{nd} (T)⟩)) \to \exists! z \in S z \neq T$
290	11 288 289	syl2anc	$⊢ (φ \land 2^{nd} (T) \in (1 \dots N - 1)) \to \exists! z \in S z \neq T$
291		xp2nd	$⊢ 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 2^{nd} (T) \in (0 \dots N)$
292	34 291	syl	$⊢ φ \to 2^{nd} (T) \in (0 \dots N)$
293	292	biantrurd	$⊢ φ \to (\neg 2^{nd} (T) \in (1 \dots N - 1) \leftrightarrow (2^{nd} (T) \in (0 \dots N) \land \neg 2^{nd} (T) \in (1 \dots N - 1)))$
294	1	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
295		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
296	294 295	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
297		fzpred	$⊢ N \in ℤ_{\geq 0} \to (0 \dots N) = \{0\} \cup (0 + 1 \dots N)$
298	296 297	syl	$⊢ φ \to (0 \dots N) = \{0\} \cup (0 + 1 \dots N)$
299	125	oveq1i	$⊢ (0 + 1 \dots N) = (1 \dots N)$
300	299	uneq2i	$⊢ \{0\} \cup (0 + 1 \dots N) = \{0\} \cup (1 \dots N)$
301	298 300	eqtrdi	$⊢ φ \to (0 \dots N) = \{0\} \cup (1 \dots N)$
302	301	difeq1d	$⊢ φ \to (0 \dots N) ∖ (1 \dots N - 1) = (\{0\} \cup (1 \dots N)) ∖ (1 \dots N - 1)$
303		difundir	$⊢ (\{0\} \cup (1 \dots N)) ∖ (1 \dots N - 1) = (\{0\} ∖ (1 \dots N - 1)) \cup ((1 \dots N) ∖ (1 \dots N - 1))$
304		0lt1	$⊢ 0 < 1$
305		0re	$⊢ 0 \in ℝ$
306		1re	$⊢ 1 \in ℝ$
307	305 306	ltnlei	$⊢ 0 < 1 \leftrightarrow \neg 1 \leq 0$
308	304 307	mpbi	$⊢ \neg 1 \leq 0$
309		elfzle1	$⊢ 0 \in (1 \dots N - 1) \to 1 \leq 0$
310	308 309	mto	$⊢ \neg 0 \in (1 \dots N - 1)$
311		incom	$⊢ (1 \dots N - 1) \cap \{0\} = \{0\} \cap (1 \dots N - 1)$
312	311	eqeq1i	$⊢ (1 \dots N - 1) \cap \{0\} = \emptyset \leftrightarrow \{0\} \cap (1 \dots N - 1) = \emptyset$
313		disjsn	$⊢ (1 \dots N - 1) \cap \{0\} = \emptyset \leftrightarrow \neg 0 \in (1 \dots N - 1)$
314		disj3	$⊢ \{0\} \cap (1 \dots N - 1) = \emptyset \leftrightarrow \{0\} = \{0\} ∖ (1 \dots N - 1)$
315	312 313 314	3bitr3i	$⊢ \neg 0 \in (1 \dots N - 1) \leftrightarrow \{0\} = \{0\} ∖ (1 \dots N - 1)$
316	310 315	mpbi	$⊢ \{0\} = \{0\} ∖ (1 \dots N - 1)$
317	316	uneq1i	$⊢ \{0\} \cup ((1 \dots N) ∖ (1 \dots N - 1)) = (\{0\} ∖ (1 \dots N - 1)) \cup ((1 \dots N) ∖ (1 \dots N - 1))$
318	303 317	eqtr4i	$⊢ (\{0\} \cup (1 \dots N)) ∖ (1 \dots N - 1) = \{0\} \cup ((1 \dots N) ∖ (1 \dots N - 1))$
319		difundir	$⊢ ((1 \dots N - 1) \cup \{N\}) ∖ (1 \dots N - 1) = ((1 \dots N - 1) ∖ (1 \dots N - 1)) \cup (\{N\} ∖ (1 \dots N - 1))$
320		difid	$⊢ (1 \dots N - 1) ∖ (1 \dots N - 1) = \emptyset$
321	320	uneq1i	$⊢ ((1 \dots N - 1) ∖ (1 \dots N - 1)) \cup (\{N\} ∖ (1 \dots N - 1)) = \emptyset \cup (\{N\} ∖ (1 \dots N - 1))$
322		uncom	$⊢ \emptyset \cup (\{N\} ∖ (1 \dots N - 1)) = (\{N\} ∖ (1 \dots N - 1)) \cup \emptyset$
323		un0	$⊢ (\{N\} ∖ (1 \dots N - 1)) \cup \emptyset = \{N\} ∖ (1 \dots N - 1)$
324	322 323	eqtri	$⊢ \emptyset \cup (\{N\} ∖ (1 \dots N - 1)) = \{N\} ∖ (1 \dots N - 1)$
325	319 321 324	3eqtri	$⊢ ((1 \dots N - 1) \cup \{N\}) ∖ (1 \dots N - 1) = \{N\} ∖ (1 \dots N - 1)$
326		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
327	1 326	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
328	252 327	eqeltrd	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq 1}$
329		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)$
330	328 258 329	syl2anc	$⊢ φ \to (1 \dots N) = (1 \dots N - 1) \cup (N - 1 + 1 \dots N)$
331	252	oveq1d	$⊢ φ \to (N - 1 + 1 \dots N) = (N \dots N)$
332	1	nnzd	$⊢ φ \to N \in ℤ$
333		fzsn	$⊢ N \in ℤ \to (N \dots N) = \{N\}$
334	332 333	syl	$⊢ φ \to (N \dots N) = \{N\}$
335	331 334	eqtrd	$⊢ φ \to (N - 1 + 1 \dots N) = \{N\}$
336	335	uneq2d	$⊢ φ \to (1 \dots N - 1) \cup (N - 1 + 1 \dots N) = (1 \dots N - 1) \cup \{N\}$
337	330 336	eqtrd	$⊢ φ \to (1 \dots N) = (1 \dots N - 1) \cup \{N\}$
338	337	difeq1d	$⊢ φ \to (1 \dots N) ∖ (1 \dots N - 1) = ((1 \dots N - 1) \cup \{N\}) ∖ (1 \dots N - 1)$
339	1	nnred	$⊢ φ \to N \in ℝ$
340	339	ltm1d	$⊢ φ \to N - 1 < N$
341	166	nn0red	$⊢ φ \to N - 1 \in ℝ$
342	341 339	ltnled	$⊢ φ \to (N - 1 < N \leftrightarrow \neg N \leq N - 1)$
343	340 342	mpbid	$⊢ φ \to \neg N \leq N - 1$
344		elfzle2	$⊢ N \in (1 \dots N - 1) \to N \leq N - 1$
345	343 344	nsyl	$⊢ φ \to \neg N \in (1 \dots N - 1)$
346		incom	$⊢ (1 \dots N - 1) \cap \{N\} = \{N\} \cap (1 \dots N - 1)$
347	346	eqeq1i	$⊢ (1 \dots N - 1) \cap \{N\} = \emptyset \leftrightarrow \{N\} \cap (1 \dots N - 1) = \emptyset$
348		disjsn	$⊢ (1 \dots N - 1) \cap \{N\} = \emptyset \leftrightarrow \neg N \in (1 \dots N - 1)$
349		disj3	$⊢ \{N\} \cap (1 \dots N - 1) = \emptyset \leftrightarrow \{N\} = \{N\} ∖ (1 \dots N - 1)$
350	347 348 349	3bitr3i	$⊢ \neg N \in (1 \dots N - 1) \leftrightarrow \{N\} = \{N\} ∖ (1 \dots N - 1)$
351	345 350	sylib	$⊢ φ \to \{N\} = \{N\} ∖ (1 \dots N - 1)$
352	325 338 351	3eqtr4a	$⊢ φ \to (1 \dots N) ∖ (1 \dots N - 1) = \{N\}$
353	352	uneq2d	$⊢ φ \to \{0\} \cup ((1 \dots N) ∖ (1 \dots N - 1)) = \{0\} \cup \{N\}$
354	318 353	syl5eq	$⊢ φ \to (\{0\} \cup (1 \dots N)) ∖ (1 \dots N - 1) = \{0\} \cup \{N\}$
355	302 354	eqtrd	$⊢ φ \to (0 \dots N) ∖ (1 \dots N - 1) = \{0\} \cup \{N\}$
356	355	eleq2d	$⊢ φ \to (2^{nd} (T) \in ((0 \dots N) ∖ (1 \dots N - 1)) \leftrightarrow 2^{nd} (T) \in (\{0\} \cup \{N\}))$
357		eldif	$⊢ 2^{nd} (T) \in ((0 \dots N) ∖ (1 \dots N - 1)) \leftrightarrow (2^{nd} (T) \in (0 \dots N) \land \neg 2^{nd} (T) \in (1 \dots N - 1))$
358		elun	$⊢ 2^{nd} (T) \in (\{0\} \cup \{N\}) \leftrightarrow (2^{nd} (T) \in \{0\} \lor 2^{nd} (T) \in \{N\})$
359	217	elsn	$⊢ 2^{nd} (T) \in \{0\} \leftrightarrow 2^{nd} (T) = 0$
360	217	elsn	$⊢ 2^{nd} (T) \in \{N\} \leftrightarrow 2^{nd} (T) = N$
361	359 360	orbi12i	$⊢ (2^{nd} (T) \in \{0\} \lor 2^{nd} (T) \in \{N\}) \leftrightarrow (2^{nd} (T) = 0 \lor 2^{nd} (T) = N)$
362	358 361	bitri	$⊢ 2^{nd} (T) \in (\{0\} \cup \{N\}) \leftrightarrow (2^{nd} (T) = 0 \lor 2^{nd} (T) = N)$
363	356 357 362	3bitr3g	$⊢ φ \to ((2^{nd} (T) \in (0 \dots N) \land \neg 2^{nd} (T) \in (1 \dots N - 1)) \leftrightarrow (2^{nd} (T) = 0 \lor 2^{nd} (T) = N))$
364	293 363	bitrd	$⊢ φ \to (\neg 2^{nd} (T) \in (1 \dots N - 1) \leftrightarrow (2^{nd} (T) = 0 \lor 2^{nd} (T) = N))$
365	364	biimpa	$⊢ (φ \land \neg 2^{nd} (T) \in (1 \dots N - 1)) \to (2^{nd} (T) = 0 \lor 2^{nd} (T) = N)$
366	1	adantr	$⊢ (φ \land 2^{nd} (T) = 0) \to N \in ℕ$
367	3	adantr	$⊢ (φ \land 2^{nd} (T) = 0) \to F : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
368	4	adantr	$⊢ (φ \land 2^{nd} (T) = 0) \to T \in S$
369	6	adantlr	$⊢ ((φ \land 2^{nd} (T) = 0) \land n \in (1 \dots N)) \to \exists p \in ran F p (n) \neq K$
370		simpr	$⊢ (φ \land 2^{nd} (T) = 0) \to 2^{nd} (T) = 0$
371	366 2 367 368 369 370	poimirlem18	$⊢ (φ \land 2^{nd} (T) = 0) \to \exists! z \in S z \neq T$
372	1	adantr	$⊢ (φ \land 2^{nd} (T) = N) \to N \in ℕ$
373	3	adantr	$⊢ (φ \land 2^{nd} (T) = N) \to F : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
374	4	adantr	$⊢ (φ \land 2^{nd} (T) = N) \to T \in S$
375	5	adantlr	$⊢ ((φ \land 2^{nd} (T) = N) \land n \in (1 \dots N)) \to \exists p \in ran F p (n) \neq 0$
376		simpr	$⊢ (φ \land 2^{nd} (T) = N) \to 2^{nd} (T) = N$
377	372 2 373 374 375 376	poimirlem21	$⊢ (φ \land 2^{nd} (T) = N) \to \exists! z \in S z \neq T$
378	371 377	jaodan	$⊢ (φ \land (2^{nd} (T) = 0 \lor 2^{nd} (T) = N)) \to \exists! z \in S z \neq T$
379	365 378	syldan	$⊢ (φ \land \neg 2^{nd} (T) \in (1 \dots N - 1)) \to \exists! z \in S z \neq T$
380	290 379	pm2.61dan	$⊢ φ \to \exists! z \in S z \neq T$

Metamath Proof Explorer

Theorem poimirlem22

Proof