poimirlem8

Description: Lemma for poimir , establishing that away from the opposite vertex the walks in poimirlem9 yield the same vertices. (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\}))))\}$
	poimirlem9.1	$⊢ φ \to T \in S$
	poimirlem9.2	$⊢ φ \to 2^{nd} (T) \in (1 \dots N - 1)$
	poimirlem9.3	$⊢ φ \to U \in S$
Assertion	poimirlem8	$⊢ φ \to {2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})} = {2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}$

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		poimirlem9.1	$⊢ φ \to T \in S$
4		poimirlem9.2	$⊢ φ \to 2^{nd} (T) \in (1 \dots N - 1)$
5		poimirlem9.3	$⊢ φ \to U \in S$
6		elrabi	$⊢ U \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 U \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
7	6 2	eleq2s	$⊢ U \in S \to U \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
8	5 7	syl	$⊢ φ \to U \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
9		xp1st	$⊢ U \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} (U) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
10	8 9	syl	$⊢ φ \to 1^{st} (U) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
11		xp2nd	$⊢ 1^{st} (U) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 2^{nd} (1^{st} (U)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
12	10 11	syl	$⊢ φ \to 2^{nd} (1^{st} (U)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
13		fvex	$⊢ 2^{nd} (1^{st} (U)) \in V$
14		f1oeq1	$⊢ f = 2^{nd} (1^{st} (U)) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
15	13 14	elab	$⊢ 2^{nd} (1^{st} (U)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
16	12 15	sylib	$⊢ φ \to 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
17		f1ofn	$⊢ 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (U)) Fn (1 \dots N)$
18	16 17	syl	$⊢ φ \to 2^{nd} (1^{st} (U)) Fn (1 \dots N)$
19		difss	$⊢ (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots N)$
20		fnssres	$⊢ (2^{nd} (1^{st} (U)) Fn (1 \dots N) \land (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots N)) \to ({2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) Fn ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
21	18 19 20	sylancl	$⊢ φ \to ({2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) Fn ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
22		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))$
23	22 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))$
24	3 23	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))$
25		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)\})$
26	24 25	syl	$⊢ φ \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
27		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)\}$
28	26 27	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
29		fvex	$⊢ 2^{nd} (1^{st} (T)) \in V$
30		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))$
31	29 30	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)$
32	28 31	sylib	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
33		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)$
34	32 33	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) Fn (1 \dots N)$
35		fnssres	$⊢ (2^{nd} (1^{st} (T)) Fn (1 \dots N) \land (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} \subseteq (1 \dots N)) \to ({2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) Fn ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
36	34 19 35	sylancl	$⊢ φ \to ({2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) Fn ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
37		fzp1elp1	$⊢ 2^{nd} (T) \in (1 \dots N - 1) \to 2^{nd} (T) + 1 \in (1 \dots N - 1 + 1)$
38	4 37	syl	$⊢ φ \to 2^{nd} (T) + 1 \in (1 \dots N - 1 + 1)$
39	1	nncnd	$⊢ φ \to N \in ℂ$
40		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
41	39 40	syl	$⊢ φ \to N - 1 + 1 = N$
42	41	oveq2d	$⊢ φ \to (1 \dots N - 1 + 1) = (1 \dots N)$
43	38 42	eleqtrd	$⊢ φ \to 2^{nd} (T) + 1 \in (1 \dots N)$
44		fzsplit	$⊢ 2^{nd} (T) + 1 \in (1 \dots N) \to (1 \dots N) = (1 \dots 2^{nd} (T) + 1) \cup (2^{nd} (T) + 1 + 1 \dots N)$
45	43 44	syl	$⊢ φ \to (1 \dots N) = (1 \dots 2^{nd} (T) + 1) \cup (2^{nd} (T) + 1 + 1 \dots N)$
46	45	difeq1d	$⊢ φ \to (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} = ((1 \dots 2^{nd} (T) + 1) \cup (2^{nd} (T) + 1 + 1 \dots N)) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
47		difundir	$⊢ ((1 \dots 2^{nd} (T) + 1) \cup (2^{nd} (T) + 1 + 1 \dots N)) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} = ((1 \dots 2^{nd} (T) + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \cup ((2^{nd} (T) + 1 + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})$
48		elfznn	$⊢ 2^{nd} (T) \in (1 \dots N - 1) \to 2^{nd} (T) \in ℕ$
49	4 48	syl	$⊢ φ \to 2^{nd} (T) \in ℕ$
50	49	nncnd	$⊢ φ \to 2^{nd} (T) \in ℂ$
51		npcan1	$⊢ 2^{nd} (T) \in ℂ \to 2^{nd} (T) - 1 + 1 = 2^{nd} (T)$
52	50 51	syl	$⊢ φ \to 2^{nd} (T) - 1 + 1 = 2^{nd} (T)$
53		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
54	49 53	eleqtrdi	$⊢ φ \to 2^{nd} (T) \in ℤ_{\geq 1}$
55	52 54	eqeltrd	$⊢ φ \to 2^{nd} (T) - 1 + 1 \in ℤ_{\geq 1}$
56	49	nnzd	$⊢ φ \to 2^{nd} (T) \in ℤ$
57		peano2zm	$⊢ 2^{nd} (T) \in ℤ \to 2^{nd} (T) - 1 \in ℤ$
58	56 57	syl	$⊢ φ \to 2^{nd} (T) - 1 \in ℤ$
59		uzid	$⊢ 2^{nd} (T) - 1 \in ℤ \to 2^{nd} (T) - 1 \in ℤ_{\geq (2^{nd} (T) - 1)}$
60		peano2uz	$⊢ 2^{nd} (T) - 1 \in ℤ_{\geq (2^{nd} (T) - 1)} \to 2^{nd} (T) - 1 + 1 \in ℤ_{\geq (2^{nd} (T) - 1)}$
61	58 59 60	3syl	$⊢ φ \to 2^{nd} (T) - 1 + 1 \in ℤ_{\geq (2^{nd} (T) - 1)}$
62	52 61	eqeltrrd	$⊢ φ \to 2^{nd} (T) \in ℤ_{\geq (2^{nd} (T) - 1)}$
63		peano2uz	$⊢ 2^{nd} (T) \in ℤ_{\geq (2^{nd} (T) - 1)} \to 2^{nd} (T) + 1 \in ℤ_{\geq (2^{nd} (T) - 1)}$
64	62 63	syl	$⊢ φ \to 2^{nd} (T) + 1 \in ℤ_{\geq (2^{nd} (T) - 1)}$
65		fzsplit2	$⊢ (2^{nd} (T) - 1 + 1 \in ℤ_{\geq 1} \land 2^{nd} (T) + 1 \in ℤ_{\geq (2^{nd} (T) - 1)}) \to (1 \dots 2^{nd} (T) + 1) = (1 \dots 2^{nd} (T) - 1) \cup (2^{nd} (T) - 1 + 1 \dots 2^{nd} (T) + 1)$
66	55 64 65	syl2anc	$⊢ φ \to (1 \dots 2^{nd} (T) + 1) = (1 \dots 2^{nd} (T) - 1) \cup (2^{nd} (T) - 1 + 1 \dots 2^{nd} (T) + 1)$
67	52	oveq1d	$⊢ φ \to (2^{nd} (T) - 1 + 1 \dots 2^{nd} (T) + 1) = (2^{nd} (T) \dots 2^{nd} (T) + 1)$
68		fzpr	$⊢ 2^{nd} (T) \in ℤ \to (2^{nd} (T) \dots 2^{nd} (T) + 1) = \{2^{nd} (T), 2^{nd} (T) + 1\}$
69	56 68	syl	$⊢ φ \to (2^{nd} (T) \dots 2^{nd} (T) + 1) = \{2^{nd} (T), 2^{nd} (T) + 1\}$
70	67 69	eqtrd	$⊢ φ \to (2^{nd} (T) - 1 + 1 \dots 2^{nd} (T) + 1) = \{2^{nd} (T), 2^{nd} (T) + 1\}$
71	70	uneq2d	$⊢ φ \to (1 \dots 2^{nd} (T) - 1) \cup (2^{nd} (T) - 1 + 1 \dots 2^{nd} (T) + 1) = (1 \dots 2^{nd} (T) - 1) \cup \{2^{nd} (T), 2^{nd} (T) + 1\}$
72	66 71	eqtrd	$⊢ φ \to (1 \dots 2^{nd} (T) + 1) = (1 \dots 2^{nd} (T) - 1) \cup \{2^{nd} (T), 2^{nd} (T) + 1\}$
73	72	difeq1d	$⊢ φ \to (1 \dots 2^{nd} (T) + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} = ((1 \dots 2^{nd} (T) - 1) \cup \{2^{nd} (T), 2^{nd} (T) + 1\}) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
74	49	nnred	$⊢ φ \to 2^{nd} (T) \in ℝ$
75	74	ltm1d	$⊢ φ \to 2^{nd} (T) - 1 < 2^{nd} (T)$
76	58	zred	$⊢ φ \to 2^{nd} (T) - 1 \in ℝ$
77	76 74	ltnled	$⊢ φ \to (2^{nd} (T) - 1 < 2^{nd} (T) \leftrightarrow \neg 2^{nd} (T) \leq 2^{nd} (T) - 1)$
78	75 77	mpbid	$⊢ φ \to \neg 2^{nd} (T) \leq 2^{nd} (T) - 1$
79		elfzle2	$⊢ 2^{nd} (T) \in (1 \dots 2^{nd} (T) - 1) \to 2^{nd} (T) \leq 2^{nd} (T) - 1$
80	78 79	nsyl	$⊢ φ \to \neg 2^{nd} (T) \in (1 \dots 2^{nd} (T) - 1)$
81		difsn	$⊢ \neg 2^{nd} (T) \in (1 \dots 2^{nd} (T) - 1) \to (1 \dots 2^{nd} (T) - 1) ∖ \{2^{nd} (T)\} = (1 \dots 2^{nd} (T) - 1)$
82	80 81	syl	$⊢ φ \to (1 \dots 2^{nd} (T) - 1) ∖ \{2^{nd} (T)\} = (1 \dots 2^{nd} (T) - 1)$
83		peano2re	$⊢ 2^{nd} (T) \in ℝ \to 2^{nd} (T) + 1 \in ℝ$
84	74 83	syl	$⊢ φ \to 2^{nd} (T) + 1 \in ℝ$
85	74	ltp1d	$⊢ φ \to 2^{nd} (T) < 2^{nd} (T) + 1$
86	76 74 84 75 85	lttrd	$⊢ φ \to 2^{nd} (T) - 1 < 2^{nd} (T) + 1$
87	76 84	ltnled	$⊢ φ \to (2^{nd} (T) - 1 < 2^{nd} (T) + 1 \leftrightarrow \neg 2^{nd} (T) + 1 \leq 2^{nd} (T) - 1)$
88	86 87	mpbid	$⊢ φ \to \neg 2^{nd} (T) + 1 \leq 2^{nd} (T) - 1$
89		elfzle2	$⊢ 2^{nd} (T) + 1 \in (1 \dots 2^{nd} (T) - 1) \to 2^{nd} (T) + 1 \leq 2^{nd} (T) - 1$
90	88 89	nsyl	$⊢ φ \to \neg 2^{nd} (T) + 1 \in (1 \dots 2^{nd} (T) - 1)$
91		difsn	$⊢ \neg 2^{nd} (T) + 1 \in (1 \dots 2^{nd} (T) - 1) \to (1 \dots 2^{nd} (T) - 1) ∖ \{2^{nd} (T) + 1\} = (1 \dots 2^{nd} (T) - 1)$
92	90 91	syl	$⊢ φ \to (1 \dots 2^{nd} (T) - 1) ∖ \{2^{nd} (T) + 1\} = (1 \dots 2^{nd} (T) - 1)$
93	82 92	ineq12d	$⊢ φ \to ((1 \dots 2^{nd} (T) - 1) ∖ \{2^{nd} (T)\}) \cap ((1 \dots 2^{nd} (T) - 1) ∖ \{2^{nd} (T) + 1\}) = (1 \dots 2^{nd} (T) - 1) \cap (1 \dots 2^{nd} (T) - 1)$
94		difun2	$⊢ ((1 \dots 2^{nd} (T) - 1) \cup \{2^{nd} (T), 2^{nd} (T) + 1\}) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} = (1 \dots 2^{nd} (T) - 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
95		df-pr	$⊢ \{2^{nd} (T), 2^{nd} (T) + 1\} = \{2^{nd} (T)\} \cup \{2^{nd} (T) + 1\}$
96	95	difeq2i	$⊢ (1 \dots 2^{nd} (T) - 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} = (1 \dots 2^{nd} (T) - 1) ∖ (\{2^{nd} (T)\} \cup \{2^{nd} (T) + 1\})$
97		difundi	$⊢ (1 \dots 2^{nd} (T) - 1) ∖ (\{2^{nd} (T)\} \cup \{2^{nd} (T) + 1\}) = ((1 \dots 2^{nd} (T) - 1) ∖ \{2^{nd} (T)\}) \cap ((1 \dots 2^{nd} (T) - 1) ∖ \{2^{nd} (T) + 1\})$
98	94 96 97	3eqtrri	$⊢ ((1 \dots 2^{nd} (T) - 1) ∖ \{2^{nd} (T)\}) \cap ((1 \dots 2^{nd} (T) - 1) ∖ \{2^{nd} (T) + 1\}) = ((1 \dots 2^{nd} (T) - 1) \cup \{2^{nd} (T), 2^{nd} (T) + 1\}) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
99		inidm	$⊢ (1 \dots 2^{nd} (T) - 1) \cap (1 \dots 2^{nd} (T) - 1) = (1 \dots 2^{nd} (T) - 1)$
100	93 98 99	3eqtr3g	$⊢ φ \to ((1 \dots 2^{nd} (T) - 1) \cup \{2^{nd} (T), 2^{nd} (T) + 1\}) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} = (1 \dots 2^{nd} (T) - 1)$
101	73 100	eqtrd	$⊢ φ \to (1 \dots 2^{nd} (T) + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} = (1 \dots 2^{nd} (T) - 1)$
102		peano2re	$⊢ 2^{nd} (T) + 1 \in ℝ \to 2^{nd} (T) + 1 + 1 \in ℝ$
103	84 102	syl	$⊢ φ \to 2^{nd} (T) + 1 + 1 \in ℝ$
104	84	ltp1d	$⊢ φ \to 2^{nd} (T) + 1 < 2^{nd} (T) + 1 + 1$
105	74 84 103 85 104	lttrd	$⊢ φ \to 2^{nd} (T) < 2^{nd} (T) + 1 + 1$
106	74 103	ltnled	$⊢ φ \to (2^{nd} (T) < 2^{nd} (T) + 1 + 1 \leftrightarrow \neg 2^{nd} (T) + 1 + 1 \leq 2^{nd} (T))$
107	105 106	mpbid	$⊢ φ \to \neg 2^{nd} (T) + 1 + 1 \leq 2^{nd} (T)$
108		elfzle1	$⊢ 2^{nd} (T) \in (2^{nd} (T) + 1 + 1 \dots N) \to 2^{nd} (T) + 1 + 1 \leq 2^{nd} (T)$
109	107 108	nsyl	$⊢ φ \to \neg 2^{nd} (T) \in (2^{nd} (T) + 1 + 1 \dots N)$
110		difsn	$⊢ \neg 2^{nd} (T) \in (2^{nd} (T) + 1 + 1 \dots N) \to (2^{nd} (T) + 1 + 1 \dots N) ∖ \{2^{nd} (T)\} = (2^{nd} (T) + 1 + 1 \dots N)$
111	109 110	syl	$⊢ φ \to (2^{nd} (T) + 1 + 1 \dots N) ∖ \{2^{nd} (T)\} = (2^{nd} (T) + 1 + 1 \dots N)$
112	84 103	ltnled	$⊢ φ \to (2^{nd} (T) + 1 < 2^{nd} (T) + 1 + 1 \leftrightarrow \neg 2^{nd} (T) + 1 + 1 \leq 2^{nd} (T) + 1)$
113	104 112	mpbid	$⊢ φ \to \neg 2^{nd} (T) + 1 + 1 \leq 2^{nd} (T) + 1$
114		elfzle1	$⊢ 2^{nd} (T) + 1 \in (2^{nd} (T) + 1 + 1 \dots N) \to 2^{nd} (T) + 1 + 1 \leq 2^{nd} (T) + 1$
115	113 114	nsyl	$⊢ φ \to \neg 2^{nd} (T) + 1 \in (2^{nd} (T) + 1 + 1 \dots N)$
116		difsn	$⊢ \neg 2^{nd} (T) + 1 \in (2^{nd} (T) + 1 + 1 \dots N) \to (2^{nd} (T) + 1 + 1 \dots N) ∖ \{2^{nd} (T) + 1\} = (2^{nd} (T) + 1 + 1 \dots N)$
117	115 116	syl	$⊢ φ \to (2^{nd} (T) + 1 + 1 \dots N) ∖ \{2^{nd} (T) + 1\} = (2^{nd} (T) + 1 + 1 \dots N)$
118	111 117	ineq12d	$⊢ φ \to ((2^{nd} (T) + 1 + 1 \dots N) ∖ \{2^{nd} (T)\}) \cap ((2^{nd} (T) + 1 + 1 \dots N) ∖ \{2^{nd} (T) + 1\}) = (2^{nd} (T) + 1 + 1 \dots N) \cap (2^{nd} (T) + 1 + 1 \dots N)$
119	95	difeq2i	$⊢ (2^{nd} (T) + 1 + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} = (2^{nd} (T) + 1 + 1 \dots N) ∖ (\{2^{nd} (T)\} \cup \{2^{nd} (T) + 1\})$
120		difundi	$⊢ (2^{nd} (T) + 1 + 1 \dots N) ∖ (\{2^{nd} (T)\} \cup \{2^{nd} (T) + 1\}) = ((2^{nd} (T) + 1 + 1 \dots N) ∖ \{2^{nd} (T)\}) \cap ((2^{nd} (T) + 1 + 1 \dots N) ∖ \{2^{nd} (T) + 1\})$
121	119 120	eqtr2i	$⊢ ((2^{nd} (T) + 1 + 1 \dots N) ∖ \{2^{nd} (T)\}) \cap ((2^{nd} (T) + 1 + 1 \dots N) ∖ \{2^{nd} (T) + 1\}) = (2^{nd} (T) + 1 + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}$
122		inidm	$⊢ (2^{nd} (T) + 1 + 1 \dots N) \cap (2^{nd} (T) + 1 + 1 \dots N) = (2^{nd} (T) + 1 + 1 \dots N)$
123	118 121 122	3eqtr3g	$⊢ φ \to (2^{nd} (T) + 1 + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} = (2^{nd} (T) + 1 + 1 \dots N)$
124	101 123	uneq12d	$⊢ φ \to ((1 \dots 2^{nd} (T) + 1) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \cup ((2^{nd} (T) + 1 + 1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) = (1 \dots 2^{nd} (T) - 1) \cup (2^{nd} (T) + 1 + 1 \dots N)$
125	47 124	syl5eq	$⊢ φ \to ((1 \dots 2^{nd} (T) + 1) \cup (2^{nd} (T) + 1 + 1 \dots N)) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} = (1 \dots 2^{nd} (T) - 1) \cup (2^{nd} (T) + 1 + 1 \dots N)$
126	46 125	eqtrd	$⊢ φ \to (1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\} = (1 \dots 2^{nd} (T) - 1) \cup (2^{nd} (T) + 1 + 1 \dots N)$
127	126	eleq2d	$⊢ φ \to (k \in ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \leftrightarrow k \in ((1 \dots 2^{nd} (T) - 1) \cup (2^{nd} (T) + 1 + 1 \dots N)))$
128		elun	$⊢ k \in ((1 \dots 2^{nd} (T) - 1) \cup (2^{nd} (T) + 1 + 1 \dots N)) \leftrightarrow (k \in (1 \dots 2^{nd} (T) - 1) \lor k \in (2^{nd} (T) + 1 + 1 \dots N))$
129	127 128	bitrdi	$⊢ φ \to (k \in ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \leftrightarrow (k \in (1 \dots 2^{nd} (T) - 1) \lor k \in (2^{nd} (T) + 1 + 1 \dots N)))$
130	129	biimpa	$⊢ (φ \land k \in ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})) \to (k \in (1 \dots 2^{nd} (T) - 1) \lor k \in (2^{nd} (T) + 1 + 1 \dots N))$
131		fveq2	$⊢ t = T \to 2^{nd} (t) = 2^{nd} (T)$
132	131	breq2d	$⊢ t = T \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (T))$
133	132	ifbid	$⊢ t = T \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (T), y, y + 1)$
134	133	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\})))$
135		2fveq3	$⊢ t = T \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T))$
136		2fveq3	$⊢ t = T \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T))$
137	136	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots j)]$
138	137	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}$
139	136	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)]$
140	139	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\}$
141	138 140	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\})$
142	135 141	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\}))$
143	142	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\})))$
144	134 143	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\})))$
145	144	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\}))))$
146	145	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\})))))$
147	146 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\})))))$
148	147	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\}))))$
149	3 148	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\}))))$
150		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)})$
151	26 150	syl	$⊢ φ \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
152		elmapi	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
153	151 152	syl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
154		elfzoelz	$⊢ n \in (0 ..^K) \to n \in ℤ$
155	154	ssriv	$⊢ (0 ..^K) \subseteq ℤ$
156		fss	$⊢ (1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K) \land (0 ..^K) \subseteq ℤ) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ ℤ$
157	153 155 156	sylancl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ ℤ$
158	1 149 157 32 4	poimirlem1	$⊢ φ \to \neg \exists^{*} n \in (1 \dots N) F (2^{nd} (T) - 1) (n) \neq F (2^{nd} (T)) (n)$
159	1	adantr	$⊢ (φ \land 2^{nd} (U) \neq 2^{nd} (T)) \to N \in ℕ$
160		fveq2	$⊢ t = U \to 2^{nd} (t) = 2^{nd} (U)$
161	160	breq2d	$⊢ t = U \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (U))$
162	161	ifbid	$⊢ t = U \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (U), y, y + 1)$
163	162	csbeq1d	$⊢ t = U \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} (U), 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\})))$
164		2fveq3	$⊢ t = U \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (U))$
165		2fveq3	$⊢ t = U \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (U))$
166	165	imaeq1d	$⊢ t = U \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (U)) [(1 \dots j)]$
167	166	xpeq1d	$⊢ t = U \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}$
168	165	imaeq1d	$⊢ t = U \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (U)) [(j + 1 \dots N)]$
169	168	xpeq1d	$⊢ t = U \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\}$
170	167 169	uneq12d	$⊢ t = U \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} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\})$
171	164 170	oveq12d	$⊢ t = U \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} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\}))$
172	171	csbeq2dv	$⊢ t = U \to ⦋ if (y < 2^{nd} (U), 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} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\})))$
173	163 172	eqtrd	$⊢ t = U \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} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\})))$
174	173	mpteq2dv	$⊢ t = U \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} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\}))))$
175	174	eqeq2d	$⊢ t = U \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} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\})))))$
176	175 2	elrab2	$⊢ U \in S \leftrightarrow (U \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} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\})))))$
177	176	simprbi	$⊢ U \in S \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\}))))$
178	5 177	syl	$⊢ φ \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\}))))$
179	178	adantr	$⊢ (φ \land 2^{nd} (U) \neq 2^{nd} (T)) \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (U), y, y + 1) / j ⦌ (1^{st} (1^{st} (U)) +_{f} ((2^{nd} (1^{st} (U)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (U)) [(j + 1 \dots N)] \times \{0\}))))$
180		xp1st	$⊢ 1^{st} (U) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 1^{st} (1^{st} (U)) \in ({(0 ..^K)}^{(1 \dots N)})$
181	10 180	syl	$⊢ φ \to 1^{st} (1^{st} (U)) \in ({(0 ..^K)}^{(1 \dots N)})$
182		elmapi	$⊢ 1^{st} (1^{st} (U)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (U)) : (1 \dots N) ⟶ (0 ..^K)$
183	181 182	syl	$⊢ φ \to 1^{st} (1^{st} (U)) : (1 \dots N) ⟶ (0 ..^K)$
184		fss	$⊢ (1^{st} (1^{st} (U)) : (1 \dots N) ⟶ (0 ..^K) \land (0 ..^K) \subseteq ℤ) \to 1^{st} (1^{st} (U)) : (1 \dots N) ⟶ ℤ$
185	183 155 184	sylancl	$⊢ φ \to 1^{st} (1^{st} (U)) : (1 \dots N) ⟶ ℤ$
186	185	adantr	$⊢ (φ \land 2^{nd} (U) \neq 2^{nd} (T)) \to 1^{st} (1^{st} (U)) : (1 \dots N) ⟶ ℤ$
187	16	adantr	$⊢ (φ \land 2^{nd} (U) \neq 2^{nd} (T)) \to 2^{nd} (1^{st} (U)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
188	4	adantr	$⊢ (φ \land 2^{nd} (U) \neq 2^{nd} (T)) \to 2^{nd} (T) \in (1 \dots N - 1)$
189		xp2nd	$⊢ U \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} (U) \in (0 \dots N)$
190	8 189	syl	$⊢ φ \to 2^{nd} (U) \in (0 \dots N)$
191		eldifsn	$⊢ 2^{nd} (U) \in ((0 \dots N) ∖ \{2^{nd} (T)\}) \leftrightarrow (2^{nd} (U) \in (0 \dots N) \land 2^{nd} (U) \neq 2^{nd} (T))$
192	191	biimpri	$⊢ (2^{nd} (U) \in (0 \dots N) \land 2^{nd} (U) \neq 2^{nd} (T)) \to 2^{nd} (U) \in ((0 \dots N) ∖ \{2^{nd} (T)\})$
193	190 192	sylan	$⊢ (φ \land 2^{nd} (U) \neq 2^{nd} (T)) \to 2^{nd} (U) \in ((0 \dots N) ∖ \{2^{nd} (T)\})$
194	159 179 186 187 188 193	poimirlem2	$⊢ (φ \land 2^{nd} (U) \neq 2^{nd} (T)) \to \exists^{*} n \in (1 \dots N) F (2^{nd} (T) - 1) (n) \neq F (2^{nd} (T)) (n)$
195	194	ex	$⊢ φ \to (2^{nd} (U) \neq 2^{nd} (T) \to \exists^{*} n \in (1 \dots N) F (2^{nd} (T) - 1) (n) \neq F (2^{nd} (T)) (n))$
196	195	necon1bd	$⊢ φ \to (\neg \exists^{*} n \in (1 \dots N) F (2^{nd} (T) - 1) (n) \neq F (2^{nd} (T)) (n) \to 2^{nd} (U) = 2^{nd} (T))$
197	158 196	mpd	$⊢ φ \to 2^{nd} (U) = 2^{nd} (T)$
198	197	oveq1d	$⊢ φ \to 2^{nd} (U) - 1 = 2^{nd} (T) - 1$
199	198	oveq2d	$⊢ φ \to (1 \dots 2^{nd} (U) - 1) = (1 \dots 2^{nd} (T) - 1)$
200	199	eleq2d	$⊢ φ \to (k \in (1 \dots 2^{nd} (U) - 1) \leftrightarrow k \in (1 \dots 2^{nd} (T) - 1))$
201	200	biimpar	$⊢ (φ \land k \in (1 \dots 2^{nd} (T) - 1)) \to k \in (1 \dots 2^{nd} (U) - 1)$
202	1	adantr	$⊢ (φ \land k \in (1 \dots 2^{nd} (U) - 1)) \to N \in ℕ$
203	5	adantr	$⊢ (φ \land k \in (1 \dots 2^{nd} (U) - 1)) \to U \in S$
204	197 4	eqeltrd	$⊢ φ \to 2^{nd} (U) \in (1 \dots N - 1)$
205	204	adantr	$⊢ (φ \land k \in (1 \dots 2^{nd} (U) - 1)) \to 2^{nd} (U) \in (1 \dots N - 1)$
206		simpr	$⊢ (φ \land k \in (1 \dots 2^{nd} (U) - 1)) \to k \in (1 \dots 2^{nd} (U) - 1)$
207	202 2 203 205 206	poimirlem6	$⊢ (φ \land k \in (1 \dots 2^{nd} (U) - 1)) \to (ι n \in (1 \dots N) \| F (k - 1) (n) \neq F (k) (n)) = 2^{nd} (1^{st} (U)) (k)$
208	201 207	syldan	$⊢ (φ \land k \in (1 \dots 2^{nd} (T) - 1)) \to (ι n \in (1 \dots N) \| F (k - 1) (n) \neq F (k) (n)) = 2^{nd} (1^{st} (U)) (k)$
209	1	adantr	$⊢ (φ \land k \in (1 \dots 2^{nd} (T) - 1)) \to N \in ℕ$
210	3	adantr	$⊢ (φ \land k \in (1 \dots 2^{nd} (T) - 1)) \to T \in S$
211	4	adantr	$⊢ (φ \land k \in (1 \dots 2^{nd} (T) - 1)) \to 2^{nd} (T) \in (1 \dots N - 1)$
212		simpr	$⊢ (φ \land k \in (1 \dots 2^{nd} (T) - 1)) \to k \in (1 \dots 2^{nd} (T) - 1)$
213	209 2 210 211 212	poimirlem6	$⊢ (φ \land k \in (1 \dots 2^{nd} (T) - 1)) \to (ι n \in (1 \dots N) \| F (k - 1) (n) \neq F (k) (n)) = 2^{nd} (1^{st} (T)) (k)$
214	208 213	eqtr3d	$⊢ (φ \land k \in (1 \dots 2^{nd} (T) - 1)) \to 2^{nd} (1^{st} (U)) (k) = 2^{nd} (1^{st} (T)) (k)$
215	197	oveq1d	$⊢ φ \to 2^{nd} (U) + 1 = 2^{nd} (T) + 1$
216	215	oveq1d	$⊢ φ \to 2^{nd} (U) + 1 + 1 = 2^{nd} (T) + 1 + 1$
217	216	oveq1d	$⊢ φ \to (2^{nd} (U) + 1 + 1 \dots N) = (2^{nd} (T) + 1 + 1 \dots N)$
218	217	eleq2d	$⊢ φ \to (k \in (2^{nd} (U) + 1 + 1 \dots N) \leftrightarrow k \in (2^{nd} (T) + 1 + 1 \dots N))$
219	218	biimpar	$⊢ (φ \land k \in (2^{nd} (T) + 1 + 1 \dots N)) \to k \in (2^{nd} (U) + 1 + 1 \dots N)$
220	1	adantr	$⊢ (φ \land k \in (2^{nd} (U) + 1 + 1 \dots N)) \to N \in ℕ$
221	5	adantr	$⊢ (φ \land k \in (2^{nd} (U) + 1 + 1 \dots N)) \to U \in S$
222	204	adantr	$⊢ (φ \land k \in (2^{nd} (U) + 1 + 1 \dots N)) \to 2^{nd} (U) \in (1 \dots N - 1)$
223		simpr	$⊢ (φ \land k \in (2^{nd} (U) + 1 + 1 \dots N)) \to k \in (2^{nd} (U) + 1 + 1 \dots N)$
224	220 2 221 222 223	poimirlem7	$⊢ (φ \land k \in (2^{nd} (U) + 1 + 1 \dots N)) \to (ι n \in (1 \dots N) \| F (k - 2) (n) \neq F (k - 1) (n)) = 2^{nd} (1^{st} (U)) (k)$
225	219 224	syldan	$⊢ (φ \land k \in (2^{nd} (T) + 1 + 1 \dots N)) \to (ι n \in (1 \dots N) \| F (k - 2) (n) \neq F (k - 1) (n)) = 2^{nd} (1^{st} (U)) (k)$
226	1	adantr	$⊢ (φ \land k \in (2^{nd} (T) + 1 + 1 \dots N)) \to N \in ℕ$
227	3	adantr	$⊢ (φ \land k \in (2^{nd} (T) + 1 + 1 \dots N)) \to T \in S$
228	4	adantr	$⊢ (φ \land k \in (2^{nd} (T) + 1 + 1 \dots N)) \to 2^{nd} (T) \in (1 \dots N - 1)$
229		simpr	$⊢ (φ \land k \in (2^{nd} (T) + 1 + 1 \dots N)) \to k \in (2^{nd} (T) + 1 + 1 \dots N)$
230	226 2 227 228 229	poimirlem7	$⊢ (φ \land k \in (2^{nd} (T) + 1 + 1 \dots N)) \to (ι n \in (1 \dots N) \| F (k - 2) (n) \neq F (k - 1) (n)) = 2^{nd} (1^{st} (T)) (k)$
231	225 230	eqtr3d	$⊢ (φ \land k \in (2^{nd} (T) + 1 + 1 \dots N)) \to 2^{nd} (1^{st} (U)) (k) = 2^{nd} (1^{st} (T)) (k)$
232	214 231	jaodan	$⊢ (φ \land (k \in (1 \dots 2^{nd} (T) - 1) \lor k \in (2^{nd} (T) + 1 + 1 \dots N))) \to 2^{nd} (1^{st} (U)) (k) = 2^{nd} (1^{st} (T)) (k)$
233	130 232	syldan	$⊢ (φ \land k \in ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})) \to 2^{nd} (1^{st} (U)) (k) = 2^{nd} (1^{st} (T)) (k)$
234		fvres	$⊢ k \in ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \to ({2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) (k) = 2^{nd} (1^{st} (U)) (k)$
235	234	adantl	$⊢ (φ \land k \in ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})) \to ({2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) (k) = 2^{nd} (1^{st} (U)) (k)$
236		fvres	$⊢ k \in ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\}) \to ({2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) (k) = 2^{nd} (1^{st} (T)) (k)$
237	236	adantl	$⊢ (φ \land k \in ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})) \to ({2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) (k) = 2^{nd} (1^{st} (T)) (k)$
238	233 235 237	3eqtr4d	$⊢ (φ \land k \in ((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})) \to ({2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) (k) = ({2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}) (k)$
239	21 36 238	eqfnfvd	$⊢ φ \to {2^{nd} (1^{st} (U)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})} = {2^{nd} (1^{st} (T)) ↾}_{((1 \dots N) ∖ \{2^{nd} (T), 2^{nd} (T) + 1\})}$

Metamath Proof Explorer

Theorem poimirlem8

Proof