poimirlem22 - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > poimirlem22		Structured version Visualization version GIF version

Theorem poimirlem22 36498

Description: Lemma for poimir 36509, 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.)

**Hypotheses**
Ref	Expression
poimir.0	⊢ (𝜑 → 𝑁 ∈ ℕ)
poimirlem22.s	⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
poimirlem22.1	⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_m (1...𝑁)))
poimirlem22.2	⊢ (𝜑 → 𝑇 ∈ 𝑆)
poimirlem22.3	⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)
poimirlem22.4	⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)

**Assertion**
Ref	Expression
poimirlem22	⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)

Distinct variable groups: 𝑓,𝑗,𝑛,𝑝,𝑡,𝑦,𝑧 𝜑,𝑗,𝑛,𝑦 𝑗,𝐹,𝑛,𝑦 𝑗,𝑁,𝑛,𝑦 𝑇,𝑗,𝑛,𝑦 𝜑,𝑝,𝑡 𝑓,𝐾,𝑗,𝑛,𝑝,𝑡 𝑓,𝑁,𝑝,𝑡 𝑇,𝑓,𝑝 𝜑,𝑧 𝑓,𝐹,𝑝,𝑡,𝑧 𝑧,𝐾 𝑧,𝑁 𝑡,𝑇,𝑧 𝑆,𝑗,𝑛,𝑝,𝑡,𝑦,𝑧 Allowed substitution hints: 𝜑(𝑓) 𝑆(𝑓) 𝐾(𝑦)

**Proof of Theorem poimirlem22**
Step	Hyp	Ref	Expression
1		poimir.0	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ)
2	1	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ)
3		poimirlem22.s	. . . 4 ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
4		poimirlem22.1	. . . . 5 ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_m (1...𝑁)))
5	4	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_m (1...𝑁)))
6		poimirlem22.2	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ 𝑆)
7	6	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → 𝑇 ∈ 𝑆)
8		simpr 485	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
9	2, 3, 5, 7, 8	poimirlem15 36491	. . 3 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ∈ 𝑆)
10		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
11	10	breq2d 5159	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
12	11	ifbid 4550	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
13	12	csbeq1d 3896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
14		2fveq3 6893	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
15		2fveq3 6893	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
16	15	imaeq1d 6056	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
17	16	xpeq1d 5704	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
18	15	imaeq1d 6056	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
19	18	xpeq1d 5704	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
20	17, 19	uneq12d 4163	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑇 → ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
21	14, 20	oveq12d 7423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑇 → ((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
22	21	csbeq2dv 3899	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
23	13, 22	eqtrd 2772	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
24	23	mpteq2dv 5249	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
25	24	eqeq2d 2743	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
26	25, 3	elrab2 3685	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
27	26	simprbi 497	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
28	6, 27	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
29	28	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_f + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
30		elrabi 3676	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
31	30, 3	eleq2s 2851	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
32	6, 31	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
33		xp1st 8003	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
35		xp1st 8003	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
36	34, 35	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
37		elmapi 8839	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
38	36, 37	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
39		elfzoelz 13628	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ)
40	39	ssriv 3985	. . . . . . . . . . . . . . . 16 ⊢ (0..^𝐾) ⊆ ℤ
41		fss 6731	. . . . . . . . . . . . . . . 16 ⊢ (((1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶ℤ)
42	38, 40, 41	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶ℤ)
43	42	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶ℤ)
44		xp2nd 8004	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
45	34, 44	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
46		fvex 6901	. . . . . . . . . . . . . . . . 17 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
47		f1oeq1 6818	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
48	46, 47	elab 3667	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
49	45, 48	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
50	49	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
51	2, 29, 43, 50, 8	poimirlem1 36477	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛))
52	51	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛))
53	1	ad3antrrr 728	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → 𝑁 ∈ ℕ)
54		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → (2^nd ‘𝑡) = (2^nd ‘𝑧))
55	54	breq2d 5159	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑧)))
56	55	ifbid 4550	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)))
57	56	csbeq1d 3896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
58		2fveq3 6893	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑧)))
59		2fveq3 6893	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑧 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑧)))
60	59	imaeq1d 6056	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑧 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)))
61	60	xpeq1d 5704	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}))
62	59	imaeq1d 6056	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑧 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)))
63	62	xpeq1d 5704	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))
64	61, 63	uneq12d 4163	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))
65	58, 64	oveq12d 7423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → ((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
66	65	csbeq2dv 3899	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
67	57, 66	eqtrd 2772	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
68	67	mpteq2dv 5249	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑧 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
69	68	eqeq2d 2743	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑧 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
70	69, 3	elrab2 3685	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 ↔ (𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
71	70	simprbi 497	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
72	71	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
73		elrabi 3676	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_f + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
74	73, 3	eleq2s 2851	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
75		xp1st 8003	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑧) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘𝑧) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
77		xp1st 8003	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑧) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑧)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
78	76, 77	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘(1^st ‘𝑧)) ∈ ((0..^𝐾) ↑_m (1...𝑁)))
79		elmapi 8839	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘(1^st ‘𝑧)) ∈ ((0..^𝐾) ↑_m (1...𝑁)) → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶(0..^𝐾))
80	78, 79	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶(0..^𝐾))
81		fss 6731	. . . . . . . . . . . . . . . . 17 ⊢ (((1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶ℤ)
82	80, 40, 81	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶ℤ)
83	82	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶ℤ)
84		xp2nd 8004	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑧) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
85	76, 84	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 → (2^nd ‘(1^st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
86		fvex 6901	. . . . . . . . . . . . . . . . . 18 ⊢ (2^nd ‘(1^st ‘𝑧)) ∈ V
87		f1oeq1 6818	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)))
88	86, 87	elab 3667	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘(1^st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
89	85, 88	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 → (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
90	89	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
91		simpllr 774	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
92		xp2nd 8004	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2^nd ‘𝑧) ∈ (0...𝑁))
93	74, 92	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 → (2^nd ‘𝑧) ∈ (0...𝑁))
94	93	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (2^nd ‘𝑧) ∈ (0...𝑁))
95		eldifsn 4789	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘𝑧) ∈ ((0...𝑁) ∖ {(2^nd ‘𝑇)}) ↔ ((2^nd ‘𝑧) ∈ (0...𝑁) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)))
96	95	biimpri 227	. . . . . . . . . . . . . . . 16 ⊢ (((2^nd ‘𝑧) ∈ (0...𝑁) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (2^nd ‘𝑧) ∈ ((0...𝑁) ∖ {(2^nd ‘𝑇)}))
97	94, 96	sylan 580	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (2^nd ‘𝑧) ∈ ((0...𝑁) ∖ {(2^nd ‘𝑇)}))
98	53, 72, 83, 90, 91, 97	poimirlem2 36478	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛))
99	98	ex 413	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ((2^nd ‘𝑧) ≠ (2^nd ‘𝑇) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛)))
100	99	necon1bd 2958	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛) → (2^nd ‘𝑧) = (2^nd ‘𝑇)))
101	52, 100	mpd 15	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (2^nd ‘𝑧) = (2^nd ‘𝑇))
102		eleq1 2821	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘𝑧) = (2^nd ‘𝑇) → ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))))
103	102	biimparc 480	. . . . . . . . . . . . . . 15 ⊢ (((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → (2^nd ‘𝑧) ∈ (1...(𝑁 − 1)))
104	103	anim2i 617	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇))) → (𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))))
105	104	anassrs 468	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → (𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))))
106	71	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
107		breq1 5150	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 0 → (𝑦 < (2^nd ‘𝑧) ↔ 0 < (2^nd ‘𝑧)))
108		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 0 → 𝑦 = 0)
109	107, 108	ifbieq1d 4551	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 0 → if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) = if(0 < (2^nd ‘𝑧), 0, (𝑦 + 1)))
110		elfznn 13526	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑧) ∈ ℕ)
111	110	nngt0d 12257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → 0 < (2^nd ‘𝑧))
112	111	iftrued 4535	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → if(0 < (2^nd ‘𝑧), 0, (𝑦 + 1)) = 0)
113	112	ad2antlr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → if(0 < (2^nd ‘𝑧), 0, (𝑦 + 1)) = 0)
114	109, 113	sylan9eqr 2794	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) = 0)
115	114	csbeq1d 3896	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋0 / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
116		c0ex 11204	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ V
117		oveq2 7413	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = 0 → (1...𝑗) = (1...0))
118		fz10 13518	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1...0) = ∅
119	117, 118	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 0 → (1...𝑗) = ∅)
120	119	imaeq2d 6057	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 0 → ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑧)) “ ∅))
121	120	xpeq1d 5704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}))
122		oveq1 7412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = 0 → (𝑗 + 1) = (0 + 1))
123		0p1e1 12330	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 + 1) = 1
124	122, 123	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = 0 → (𝑗 + 1) = 1)
125	124	oveq1d 7420	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 0 → ((𝑗 + 1)...𝑁) = (1...𝑁))
126	125	imaeq2d 6057	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 0 → ((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)))
127	126	xpeq1d 5704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
128	121, 127	uneq12d 4163	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 0 → ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})))
129		ima0 6073	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2^nd ‘(1^st ‘𝑧)) “ ∅) = ∅
130	129	xpeq1i 5701	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) = (∅ × {1})
131		0xp 5772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∅ × {1}) = ∅
132	130, 131	eqtri 2760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) = ∅
133	132	uneq1i 4158	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = (∅ ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
134		uncom 4152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∅ ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}) ∪ ∅)
135		un0 4389	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}) ∪ ∅) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})
136	133, 134, 135	3eqtri 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})
137	128, 136	eqtrdi 2788	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 0 → ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
138	137	oveq2d 7421	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 0 → ((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑧)) ∘_f + (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})))
139	116, 138	csbie 3928	. . . . . . . . . . . . . . . . 17 ⊢ ⦋0 / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑧)) ∘_f + (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
140		f1ofo 6837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–onto→(1...𝑁))
141	89, 140	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ 𝑆 → (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–onto→(1...𝑁))
142		foima 6807	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2^nd ‘(1^st ‘𝑧)):(1...𝑁)–onto→(1...𝑁) → ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) = (1...𝑁))
143	141, 142	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝑆 → ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) = (1...𝑁))
144	143	xpeq1d 5704	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}) = ((1...𝑁) × {0}))
145	144	oveq2d 7421	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑆 → ((1^st ‘(1^st ‘𝑧)) ∘_f + (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = ((1^st ‘(1^st ‘𝑧)) ∘_f + ((1...𝑁) × {0})))
146		ovexd 7440	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (1...𝑁) ∈ V)
147	80	ffnd 6715	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘(1^st ‘𝑧)) Fn (1...𝑁))
148		fnconstg 6776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
149	116, 148	mp1i 13	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → ((1...𝑁) × {0}) Fn (1...𝑁))
150		eqidd 2733	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) = ((1^st ‘(1^st ‘𝑧))‘𝑛))
151	116	fvconst2 7201	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
152	151	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
153	80	ffvelcdmda 7083	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ (0..^𝐾))
154		elfzonn0 13673	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ ℕ₀)
155	153, 154	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ ℕ₀)
156	155	nn0cnd 12530	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ ℂ)
157	156	addridd 11410	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑧))‘𝑛) + 0) = ((1^st ‘(1^st ‘𝑧))‘𝑛))
158	146, 147, 149, 147, 150, 152, 157	offveq 7690	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑆 → ((1^st ‘(1^st ‘𝑧)) ∘_f + ((1...𝑁) × {0})) = (1^st ‘(1^st ‘𝑧)))
159	145, 158	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 → ((1^st ‘(1^st ‘𝑧)) ∘_f + (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = (1^st ‘(1^st ‘𝑧)))
160	139, 159	eqtrid 2784	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 → ⦋0 / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1^st ‘(1^st ‘𝑧)))
161	160	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → ⦋0 / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1^st ‘(1^st ‘𝑧)))
162	115, 161	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_f + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1^st ‘(1^st ‘𝑧)))
163		nnm1nn0 12509	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
164	1, 163	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
165		0elfz 13594	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 − 1) ∈ ℕ₀ → 0 ∈ (0...(𝑁 − 1)))
166	164, 165	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ (0...(𝑁 − 1)))
167	166	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → 0 ∈ (0...(𝑁 − 1)))
168		fvexd 6903	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (1^st ‘(1^st ‘𝑧)) ∈ V)
169	106, 162, 167, 168	fvmptd 7002	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧)))
170	105, 169	sylan 580	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) ∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧)))
171	170	an32s 650	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧)))
172	101, 171	mpdan 685	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧)))
173		fveq2 6888	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑇 → (2^nd ‘𝑧) = (2^nd ‘𝑇))
174	173	eleq1d 2818	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑇 → ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))))
175	174	anbi2d 629	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑇 → ((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ↔ (𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))))
176		2fveq3 6893	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑇 → (1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)))
177	176	eqeq2d 2743	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑇 → ((𝐹‘0) = (1^st ‘(1^st ‘𝑧)) ↔ (𝐹‘0) = (1^st ‘(1^st ‘𝑇))))
178	175, 177	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑇 → (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧))) ↔ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^st ‘(1^st ‘𝑇)))))
179	169	expcom 414	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑆 → ((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧))))
180	178, 179	vtoclga 3565	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ 𝑆 → ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^st ‘(1^st ‘𝑇))))
181	7, 180	mpcom 38	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^st ‘(1^st ‘𝑇)))
182	181	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^st ‘(1^st ‘𝑇)))
183	172, 182	eqtr3d 2774	. . . . . . . . 9 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)))
184	183	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)))
185	1	ad3antrrr 728	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑁 ∈ ℕ)
186	6	ad3antrrr 728	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑇 ∈ 𝑆)
187		simpllr 774	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
188		simplr 767	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑧 ∈ 𝑆)
189	34	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
190		xpopth 8012	. . . . . . . . . . . . . 14 ⊢ (((1^st ‘𝑧) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) → (((1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑧)) = (2^nd ‘(1^st ‘𝑇))) ↔ (1^st ‘𝑧) = (1^st ‘𝑇)))
191	76, 189, 190	syl2anr 597	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (((1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑧)) = (2^nd ‘(1^st ‘𝑇))) ↔ (1^st ‘𝑧) = (1^st ‘𝑇)))
192	32	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
193		xpopth 8012	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1^st ‘𝑧) = (1^st ‘𝑇) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) ↔ 𝑧 = 𝑇))
194	193	biimpd 228	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1^st ‘𝑧) = (1^st ‘𝑇) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → 𝑧 = 𝑇))
195	74, 192, 194	syl2anr 597	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (((1^st ‘𝑧) = (1^st ‘𝑇) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → 𝑧 = 𝑇))
196	101, 195	mpan2d 692	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ((1^st ‘𝑧) = (1^st ‘𝑇) → 𝑧 = 𝑇))
197	191, 196	sylbid 239	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (((1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑧)) = (2^nd ‘(1^st ‘𝑇))) → 𝑧 = 𝑇))
198	183, 197	mpand 693	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ((2^nd ‘(1^st ‘𝑧)) = (2^nd ‘(1^st ‘𝑇)) → 𝑧 = 𝑇))
199	198	necon3d 2961	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (2^nd ‘(1^st ‘𝑧)) ≠ (2^nd ‘(1^st ‘𝑇))))
200	199	imp 407	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^nd ‘(1^st ‘𝑧)) ≠ (2^nd ‘(1^st ‘𝑇)))
201	185, 3, 186, 187, 188, 200	poimirlem9 36485	. . . . . . . 8 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^nd ‘(1^st ‘𝑧)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))))
202	101	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^nd ‘𝑧) = (2^nd ‘𝑇))
203	184, 201, 202	jca31 515	. . . . . . 7 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (((1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑧)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)))
204	203	ex 413	. . . . . 6 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (((1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑧)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇))))
205		simplr 767	. . . . . . . 8 ⊢ ((((1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑧)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → (2^nd ‘(1^st ‘𝑧)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))))
206		elfznn 13526	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ∈ ℕ)
207	206	nnred 12223	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ∈ ℝ)
208	207	ltp1d 12140	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
209	207, 208	ltned 11346	. . . . . . . . . . . 12 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
210	209	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
211		fveq1 6887	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘(1^st ‘𝑇)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) → ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) = (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))‘(2^nd ‘𝑇)))
212		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2^nd ‘𝑇) ∈ ℝ → (2^nd ‘𝑇) ∈ ℝ)
213		ltp1 12050	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2^nd ‘𝑇) ∈ ℝ → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
214	212, 213	ltned 11346	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2^nd ‘𝑇) ∈ ℝ → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
215		fvex 6901	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2^nd ‘𝑇) ∈ V
216		ovex 7438	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2^nd ‘𝑇) + 1) ∈ V
217	215, 216, 216, 215	fpr 7148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1) → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)})
218	214, 217	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑇) ∈ ℝ → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)})
219		f1oi 6868	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})):((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})–1-1-onto→((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
220		f1of 6830	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})):((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})–1-1-onto→((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) → ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})):((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})⟶((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
221	219, 220	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})):((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})⟶((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
222		disjdif 4470	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅
223		fun 6750	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} ∧ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})):((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})⟶((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) ∧ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))⟶({((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
224	222, 223	mpan2 689	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} ∧ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})):((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})⟶((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))⟶({((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
225	218, 221, 224	sylancl 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑇) ∈ ℝ → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))⟶({((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
226	215	prid1 4765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2^nd ‘𝑇) ∈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}
227		elun1 4175	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑇) ∈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} → (2^nd ‘𝑇) ∈ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
228	226, 227	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (2^nd ‘𝑇) ∈ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
229		fvco3 6987	. . . . . . . . . . . . . . . . . . 19 ⊢ ((({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))):({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))⟶({((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) ∧ (2^nd ‘𝑇) ∈ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))) → (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))‘(2^nd ‘𝑇)) = ((2^nd ‘(1^st ‘𝑇))‘(({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))‘(2^nd ‘𝑇))))
230	225, 228, 229	sylancl 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑇) ∈ ℝ → (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))‘(2^nd ‘𝑇)) = ((2^nd ‘(1^st ‘𝑇))‘(({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))‘(2^nd ‘𝑇))))
231	218	ffnd 6715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2^nd ‘𝑇) ∈ ℝ → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
232		fnresi 6676	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) Fn ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
233	222, 226	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅ ∧ (2^nd ‘𝑇) ∈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
234		fvun1 6979	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∧ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) Fn ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}) ∧ (({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅ ∧ (2^nd ‘𝑇) ∈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))‘(2^nd ‘𝑇)) = ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}‘(2^nd ‘𝑇)))
235	232, 233, 234	mp3an23 1453	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))‘(2^nd ‘𝑇)) = ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}‘(2^nd ‘𝑇)))
236	231, 235	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑇) ∈ ℝ → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))‘(2^nd ‘𝑇)) = ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}‘(2^nd ‘𝑇)))
237	215, 216	fvpr1 7187	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}‘(2^nd ‘𝑇)) = ((2^nd ‘𝑇) + 1))
238	214, 237	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑇) ∈ ℝ → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}‘(2^nd ‘𝑇)) = ((2^nd ‘𝑇) + 1))
239	236, 238	eqtrd 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑇) ∈ ℝ → (({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))‘(2^nd ‘𝑇)) = ((2^nd ‘𝑇) + 1))
240	239	fveq2d 6892	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑇) ∈ ℝ → ((2^nd ‘(1^st ‘𝑇))‘(({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))‘(2^nd ‘𝑇))) = ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)))
241	230, 240	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘𝑇) ∈ ℝ → (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))‘(2^nd ‘𝑇)) = ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)))
242	207, 241	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))‘(2^nd ‘𝑇)) = ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)))
243	242	eqeq2d 2743	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) = (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))‘(2^nd ‘𝑇)) ↔ ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) = ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))))
244	243	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) = (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))‘(2^nd ‘𝑇)) ↔ ((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) = ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1))))
245		f1of1 6829	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁))
246	49, 245	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁))
247	246	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁))
248	1	nncnd 12224	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℂ)
249		npcan1 11635	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
250	248, 249	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
251	164	nn0zd 12580	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
252		uzid 12833	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
253	251, 252	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
254		peano2uz 12881	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
255	253, 254	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
256	250, 255	eqeltrrd 2834	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
257		fzss2 13537	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
258	256, 257	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
259	258	sselda 3981	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘𝑇) ∈ (1...𝑁))
260		fzp1elp1 13550	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → ((2^nd ‘𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
261	260	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((2^nd ‘𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
262	250	oveq2d 7421	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
263	262	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (1...((𝑁 − 1) + 1)) = (1...𝑁))
264	261, 263	eleqtrd 2835	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((2^nd ‘𝑇) + 1) ∈ (1...𝑁))
265		f1veqaeq 7252	. . . . . . . . . . . . . . 15 ⊢ (((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ ((2^nd ‘𝑇) ∈ (1...𝑁) ∧ ((2^nd ‘𝑇) + 1) ∈ (1...𝑁))) → (((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) = ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) → (2^nd ‘𝑇) = ((2^nd ‘𝑇) + 1)))
266	247, 259, 264, 265	syl12anc 835	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) = ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) → (2^nd ‘𝑇) = ((2^nd ‘𝑇) + 1)))
267	244, 266	sylbid 239	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) = (((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))‘(2^nd ‘𝑇)) → (2^nd ‘𝑇) = ((2^nd ‘𝑇) + 1)))
268	211, 267	syl5 34	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((2^nd ‘(1^st ‘𝑇)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) → (2^nd ‘𝑇) = ((2^nd ‘𝑇) + 1)))
269	268	necon3d 2961	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1) → (2^nd ‘(1^st ‘𝑇)) ≠ ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))))
270	210, 269	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘(1^st ‘𝑇)) ≠ ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))))
271		2fveq3 6893	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑇 → (2^nd ‘(1^st ‘𝑧)) = (2^nd ‘(1^st ‘𝑇)))
272	271	neeq1d 3000	. . . . . . . . . 10 ⊢ (𝑧 = 𝑇 → ((2^nd ‘(1^st ‘𝑧)) ≠ ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) ↔ (2^nd ‘(1^st ‘𝑇)) ≠ ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))))
273	270, 272	syl5ibrcom 246	. . . . . . . . 9 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (𝑧 = 𝑇 → (2^nd ‘(1^st ‘𝑧)) ≠ ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))))
274	273	necon2d 2963	. . . . . . . 8 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((2^nd ‘(1^st ‘𝑧)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))) → 𝑧 ≠ 𝑇))
275	205, 274	syl5 34	. . . . . . 7 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((((1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑧)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → 𝑧 ≠ 𝑇))
276	275	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ((((1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑧)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → 𝑧 ≠ 𝑇))
277	204, 276	impbid 211	. . . . 5 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 ↔ (((1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑧)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇))))
278		eqop 8013	. . . . . . . 8 ⊢ (𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (𝑧 = ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ↔ ((1^st ‘𝑧) = ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇))))
279		eqop 8013	. . . . . . . . . 10 ⊢ ((1^st ‘𝑧) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ((1^st ‘𝑧) = ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ ↔ ((1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑧)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))))))
280	75, 279	syl 17	. . . . . . . . 9 ⊢ (𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → ((1^st ‘𝑧) = ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ ↔ ((1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑧)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))))))
281	280	anbi1d 630	. . . . . . . 8 ⊢ (𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (((1^st ‘𝑧) = ⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩ ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) ↔ (((1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑧)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇))))
282	278, 281	bitrd 278	. . . . . . 7 ⊢ (𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (𝑧 = ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ↔ (((1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑧)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇))))
283	74, 282	syl 17	. . . . . 6 ⊢ (𝑧 ∈ 𝑆 → (𝑧 = ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ↔ (((1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑧)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇))))
284	283	adantl 482	. . . . 5 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝑧 = ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ↔ (((1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑧)) = ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇))))
285	277, 284	bitr4d 281	. . . 4 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 ↔ 𝑧 = ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩))
286	285	ralrimiva 3146	. . 3 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ∀𝑧 ∈ 𝑆 (𝑧 ≠ 𝑇 ↔ 𝑧 = ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩))
287		reu6i 3723	. . 3 ⊢ ((⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩ ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 (𝑧 ≠ 𝑇 ↔ 𝑧 = ⟨⟨(1^st ‘(1^st ‘𝑇)), ((2^nd ‘(1^st ‘𝑇)) ∘ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))))⟩, (2^nd ‘𝑇)⟩)) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
288	9, 286, 287	syl2anc 584	. 2 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
289		xp2nd 8004	. . . . . . 7 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2^nd ‘𝑇) ∈ (0...𝑁))
290	32, 289	syl 17	. . . . . 6 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (0...𝑁))
291	290	biantrurd 533	. . . . 5 ⊢ (𝜑 → (¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) ↔ ((2^nd ‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))))
292	1	nnnn0d 12528	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
293		nn0uz 12860	. . . . . . . . . . . 12 ⊢ ℕ₀ = (ℤ_≥‘0)
294	292, 293	eleqtrdi 2843	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
295		fzpred 13545	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘0) → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
296	294, 295	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
297	123	oveq1i 7415	. . . . . . . . . . 11 ⊢ ((0 + 1)...𝑁) = (1...𝑁)
298	297	uneq2i 4159	. . . . . . . . . 10 ⊢ ({0} ∪ ((0 + 1)...𝑁)) = ({0} ∪ (1...𝑁))
299	296, 298	eqtrdi 2788	. . . . . . . . 9 ⊢ (𝜑 → (0...𝑁) = ({0} ∪ (1...𝑁)))
300	299	difeq1d 4120	. . . . . . . 8 ⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))))
301		difundir 4279	. . . . . . . . . 10 ⊢ (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = (({0} ∖ (1...(𝑁 − 1))) ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
302		0lt1 11732	. . . . . . . . . . . . . 14 ⊢ 0 < 1
303		0re 11212	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
304		1re 11210	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
305	303, 304	ltnlei 11331	. . . . . . . . . . . . . 14 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
306	302, 305	mpbi 229	. . . . . . . . . . . . 13 ⊢ ¬ 1 ≤ 0
307		elfzle1 13500	. . . . . . . . . . . . 13 ⊢ (0 ∈ (1...(𝑁 − 1)) → 1 ≤ 0)
308	306, 307	mto 196	. . . . . . . . . . . 12 ⊢ ¬ 0 ∈ (1...(𝑁 − 1))
309		incom 4200	. . . . . . . . . . . . . 14 ⊢ ((1...(𝑁 − 1)) ∩ {0}) = ({0} ∩ (1...(𝑁 − 1)))
310	309	eqeq1i 2737	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {0}) = ∅ ↔ ({0} ∩ (1...(𝑁 − 1))) = ∅)
311		disjsn 4714	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (1...(𝑁 − 1)))
312		disj3 4452	. . . . . . . . . . . . 13 ⊢ (({0} ∩ (1...(𝑁 − 1))) = ∅ ↔ {0} = ({0} ∖ (1...(𝑁 − 1))))
313	310, 311, 312	3bitr3i 300	. . . . . . . . . . . 12 ⊢ (¬ 0 ∈ (1...(𝑁 − 1)) ↔ {0} = ({0} ∖ (1...(𝑁 − 1))))
314	308, 313	mpbi 229	. . . . . . . . . . 11 ⊢ {0} = ({0} ∖ (1...(𝑁 − 1)))
315	314	uneq1i 4158	. . . . . . . . . 10 ⊢ ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1)))) = (({0} ∖ (1...(𝑁 − 1))) ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
316	301, 315	eqtr4i 2763	. . . . . . . . 9 ⊢ (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
317		difundir 4279	. . . . . . . . . . . 12 ⊢ (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))) = (((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) ∪ ({𝑁} ∖ (1...(𝑁 − 1))))
318		difid 4369	. . . . . . . . . . . . 13 ⊢ ((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) = ∅
319	318	uneq1i 4158	. . . . . . . . . . . 12 ⊢ (((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1))))
320		uncom 4152	. . . . . . . . . . . . 13 ⊢ (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = (({𝑁} ∖ (1...(𝑁 − 1))) ∪ ∅)
321		un0 4389	. . . . . . . . . . . . 13 ⊢ (({𝑁} ∖ (1...(𝑁 − 1))) ∪ ∅) = ({𝑁} ∖ (1...(𝑁 − 1)))
322	320, 321	eqtri 2760	. . . . . . . . . . . 12 ⊢ (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = ({𝑁} ∖ (1...(𝑁 − 1)))
323	317, 319, 322	3eqtri 2764	. . . . . . . . . . 11 ⊢ (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))) = ({𝑁} ∖ (1...(𝑁 − 1)))
324		nnuz 12861	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
325	1, 324	eleqtrdi 2843	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
326	250, 325	eqeltrd 2833	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘1))
327		fzsplit2 13522	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 − 1) + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
328	326, 256, 327	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
329	250	oveq1d 7420	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
330	1	nnzd 12581	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℤ)
331		fzsn 13539	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
332	330, 331	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁...𝑁) = {𝑁})
333	329, 332	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
334	333	uneq2d 4162	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁}))
335	328, 334	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁}))
336	335	difeq1d 4120	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))))
337	1	nnred 12223	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℝ)
338	337	ltm1d 12142	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
339	164	nn0red 12529	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
340	339, 337	ltnled 11357	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
341	338, 340	mpbid 231	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
342		elfzle2 13501	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
343	341, 342	nsyl 140	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
344		incom 4200	. . . . . . . . . . . . . 14 ⊢ ((1...(𝑁 − 1)) ∩ {𝑁}) = ({𝑁} ∩ (1...(𝑁 − 1)))
345	344	eqeq1i 2737	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ({𝑁} ∩ (1...(𝑁 − 1))) = ∅)
346		disjsn 4714	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1)))
347		disj3 4452	. . . . . . . . . . . . 13 ⊢ (({𝑁} ∩ (1...(𝑁 − 1))) = ∅ ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1))))
348	345, 346, 347	3bitr3i 300	. . . . . . . . . . . 12 ⊢ (¬ 𝑁 ∈ (1...(𝑁 − 1)) ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1))))
349	343, 348	sylib 217	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1))))
350	323, 336, 349	3eqtr4a 2798	. . . . . . . . . 10 ⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = {𝑁})
351	350	uneq2d 4162	. . . . . . . . 9 ⊢ (𝜑 → ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1)))) = ({0} ∪ {𝑁}))
352	316, 351	eqtrid 2784	. . . . . . . 8 ⊢ (𝜑 → (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = ({0} ∪ {𝑁}))
353	300, 352	eqtrd 2772	. . . . . . 7 ⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = ({0} ∪ {𝑁}))
354	353	eleq2d 2819	. . . . . 6 ⊢ (𝜑 → ((2^nd ‘𝑇) ∈ ((0...𝑁) ∖ (1...(𝑁 − 1))) ↔ (2^nd ‘𝑇) ∈ ({0} ∪ {𝑁})))
355		eldif 3957	. . . . . 6 ⊢ ((2^nd ‘𝑇) ∈ ((0...𝑁) ∖ (1...(𝑁 − 1))) ↔ ((2^nd ‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))))
356		elun 4147	. . . . . . 7 ⊢ ((2^nd ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2^nd ‘𝑇) ∈ {0} ∨ (2^nd ‘𝑇) ∈ {𝑁}))
357	215	elsn 4642	. . . . . . . 8 ⊢ ((2^nd ‘𝑇) ∈ {0} ↔ (2^nd ‘𝑇) = 0)
358	215	elsn 4642	. . . . . . . 8 ⊢ ((2^nd ‘𝑇) ∈ {𝑁} ↔ (2^nd ‘𝑇) = 𝑁)
359	357, 358	orbi12i 913	. . . . . . 7 ⊢ (((2^nd ‘𝑇) ∈ {0} ∨ (2^nd ‘𝑇) ∈ {𝑁}) ↔ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁))
360	356, 359	bitri 274	. . . . . 6 ⊢ ((2^nd ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁))
361	354, 355, 360	3bitr3g 312	. . . . 5 ⊢ (𝜑 → (((2^nd ‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ↔ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁)))
362	291, 361	bitrd 278	. . . 4 ⊢ (𝜑 → (¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) ↔ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁)))
363	362	biimpa 477	. . 3 ⊢ ((𝜑 ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁))
364	1	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → 𝑁 ∈ ℕ)
365	4	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_m (1...𝑁)))
366	6	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → 𝑇 ∈ 𝑆)
367		poimirlem22.4	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)
368	367	adantlr 713	. . . . 5 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) = 0) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)
369		simpr 485	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → (2^nd ‘𝑇) = 0)
370	364, 3, 365, 366, 368, 369	poimirlem18 36494	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
371	1	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → 𝑁 ∈ ℕ)
372	4	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_m (1...𝑁)))
373	6	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → 𝑇 ∈ 𝑆)
374		poimirlem22.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)
375	374	adantlr 713	. . . . 5 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)
376		simpr 485	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → (2^nd ‘𝑇) = 𝑁)
377	371, 3, 372, 373, 375, 376	poimirlem21 36497	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
378	370, 377	jaodan 956	. . 3 ⊢ ((𝜑 ∧ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁)) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
379	363, 378	syldan 591	. 2 ⊢ ((𝜑 ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
380	288, 379	pm2.61dan 811	1 ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 = wceq 1541 ∈ wcel 2106 {cab 2709 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 ∃!wreu 3374 ∃*wrmo 3375 {crab 3432 Vcvv 3474 ⦋csb 3892 ∖ cdif 3944 ∪ cun 3945 ∩ cin 3946 ⊆ wss 3947 ∅c0 4321 ifcif 4527 {csn 4627 {cpr 4629 ⟨cop 4633 class class class wbr 5147 ↦ cmpt 5230 I cid 5572 × cxp 5673 ran crn 5676 ↾ cres 5677 “ cima 5678 ∘ ccom 5679 Fn wfn 6535 ⟶wf 6536 –1-1→wf1 6537 –onto→wfo 6538 –1-1-onto→wf1o 6539 ‘cfv 6540 (class class class)co 7405 ∘_f cof 7664 1^st c1st 7969 2^nd c2nd 7970 ↑_m cmap 8816 ℂcc 11104 ℝcr 11105 0cc0 11106 1c1 11107 + caddc 11109 < clt 11244 ≤ cle 11245 − cmin 11440 ℕcn 12208 ℕ₀cn0 12468 ℤcz 12554 ℤ_≥cuz 12818 ...cfz 13480 ..^cfzo 13623

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-of 7666 df-om 7852 df-1st 7971 df-2nd 7972 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-oadd 8466 df-er 8699 df-map 8818 df-pm 8819 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-dju 9892 df-card 9930 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-div 11868 df-nn 12209 df-2 12271 df-3 12272 df-n0 12469 df-xnn0 12541 df-z 12555 df-uz 12819 df-fz 13481 df-fzo 13624 df-seq 13963 df-fac 14230 df-bc 14259 df-hash 14287

This theorem is referenced by: poimirlem27 36503

W3C validator