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 32601

Description: Lemma for poimir 32612, 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..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
poimirlem22.1	⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_𝑚 (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 480	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ)
3		poimirlem22.s	. . . 4 ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
4		poimirlem22.1	. . . . 5 ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_𝑚 (1...𝑁)))
5	4	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_𝑚 (1...𝑁)))
6		poimirlem22.2	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ 𝑆)
7	6	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → 𝑇 ∈ 𝑆)
8		simpr 476	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
9	2, 3, 5, 7, 8	poimirlem15 32594	. . 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 6103	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
11	10	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
12	11	ifbid 4058	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
13	12	csbeq1d 3506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
14		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → (1^st ‘𝑡) = (1^st ‘𝑇))
15	14	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
16	14	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
17	16	imaeq1d 5384	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
18	17	xpeq1d 5062	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
19	16	imaeq1d 5384	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
20	19	xpeq1d 5062	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
21	18, 20	uneq12d 3730	. . . . . . . . . . . . . . . . . . . . . . 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})))
22	15, 21	oveq12d 6567	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑇 → ((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
23	22	csbeq2dv 3944	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
24	13, 23	eqtrd 2644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
25	24	mpteq2dv 4673	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
26	25	eqeq2d 2620	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
27	26, 3	elrab2 3333	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
28	27	simprbi 479	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
29	6, 28	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
30	29	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
31		elrabi 3328	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
32	31, 3	eleq2s 2706	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
33	6, 32	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
34		xp1st 7089	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
35	33, 34	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
36		xp1st 7089	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)))
37	35, 36	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)))
38		elmapi 7765	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
39	37, 38	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
40		elfzoelz 12339	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ)
41	40	ssriv 3572	. . . . . . . . . . . . . . . 16 ⊢ (0..^𝐾) ⊆ ℤ
42		fss 5969	. . . . . . . . . . . . . . . 16 ⊢ (((1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶ℤ)
43	39, 41, 42	sylancl 693	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶ℤ)
44	43	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶ℤ)
45		xp2nd 7090	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
46	35, 45	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
47		fvex 6113	. . . . . . . . . . . . . . . . 17 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
48		f1oeq1 6040	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
49	47, 48	elab 3319	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
50	46, 49	sylib 207	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
51	50	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
52	2, 30, 44, 51, 8	poimirlem1 32580	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛))
53	52	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛))
54	1	ad3antrrr 762	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → 𝑁 ∈ ℕ)
55		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → (2^nd ‘𝑡) = (2^nd ‘𝑧))
56	55	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑧)))
57	56	ifbid 4058	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)))
58	57	csbeq1d 3506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
59		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → (1^st ‘𝑡) = (1^st ‘𝑧))
60	59	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑧)))
61	59	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑧 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑧)))
62	61	imaeq1d 5384	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑧 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)))
63	62	xpeq1d 5062	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}))
64	61	imaeq1d 5384	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑧 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)))
65	64	xpeq1d 5062	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))
66	63, 65	uneq12d 3730	. . . . . . . . . . . . . . . . . . . . . . 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})))
67	60, 66	oveq12d 6567	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → ((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
68	67	csbeq2dv 3944	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
69	58, 68	eqtrd 2644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
70	69	mpteq2dv 4673	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑧 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
71	70	eqeq2d 2620	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑧 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
72	71, 3	elrab2 3333	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 ↔ (𝑧 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
73	72	simprbi 479	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
74	73	ad2antlr 759	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
75		elrabi 3328	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑧 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
76	75, 3	eleq2s 2706	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
77		xp1st 7089	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑧) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
78	76, 77	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘𝑧) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
79		xp1st 7089	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1^st ‘𝑧) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑧)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)))
80	78, 79	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘(1^st ‘𝑧)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)))
81		elmapi 7765	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘(1^st ‘𝑧)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)) → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶(0..^𝐾))
82	80, 81	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶(0..^𝐾))
83		fss 5969	. . . . . . . . . . . . . . . . 17 ⊢ (((1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶ℤ)
84	82, 41, 83	sylancl 693	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶ℤ)
85	84	ad2antlr 759	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶ℤ)
86		xp2nd 7090	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑧) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
87	78, 86	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 → (2^nd ‘(1^st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
88		fvex 6113	. . . . . . . . . . . . . . . . . 18 ⊢ (2^nd ‘(1^st ‘𝑧)) ∈ V
89		f1oeq1 6040	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)))
90	88, 89	elab 3319	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘(1^st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
91	87, 90	sylib 207	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 → (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
92	91	ad2antlr 759	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
93		simpllr 795	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
94		xp2nd 7090	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2^nd ‘𝑧) ∈ (0...𝑁))
95	76, 94	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 → (2^nd ‘𝑧) ∈ (0...𝑁))
96	95	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (2^nd ‘𝑧) ∈ (0...𝑁))
97		eldifsn 4260	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘𝑧) ∈ ((0...𝑁) ∖ {(2^nd ‘𝑇)}) ↔ ((2^nd ‘𝑧) ∈ (0...𝑁) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)))
98	97	biimpri 217	. . . . . . . . . . . . . . . 16 ⊢ (((2^nd ‘𝑧) ∈ (0...𝑁) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (2^nd ‘𝑧) ∈ ((0...𝑁) ∖ {(2^nd ‘𝑇)}))
99	96, 98	sylan 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (2^nd ‘𝑧) ∈ ((0...𝑁) ∖ {(2^nd ‘𝑇)}))
100	54, 74, 85, 92, 93, 99	poimirlem2 32581	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛))
101	100	ex 449	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ((2^nd ‘𝑧) ≠ (2^nd ‘𝑇) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛)))
102	101	necon1bd 2800	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛) → (2^nd ‘𝑧) = (2^nd ‘𝑇)))
103	53, 102	mpd 15	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (2^nd ‘𝑧) = (2^nd ‘𝑇))
104		eleq1 2676	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘𝑧) = (2^nd ‘𝑇) → ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))))
105	104	biimparc 503	. . . . . . . . . . . . . . 15 ⊢ (((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → (2^nd ‘𝑧) ∈ (1...(𝑁 − 1)))
106	105	anim2i 591	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇))) → (𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))))
107	106	anassrs 678	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → (𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))))
108	73	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))
109		breq1 4586	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 0 → (𝑦 < (2^nd ‘𝑧) ↔ 0 < (2^nd ‘𝑧)))
110		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 0 → 𝑦 = 0)
111	109, 110	ifbieq1d 4059	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 0 → if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) = if(0 < (2^nd ‘𝑧), 0, (𝑦 + 1)))
112		elfznn 12241	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑧) ∈ ℕ)
113	112	nngt0d 10941	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → 0 < (2^nd ‘𝑧))
114	113	iftrued 4044	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → if(0 < (2^nd ‘𝑧), 0, (𝑦 + 1)) = 0)
115	114	ad2antlr 759	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → if(0 < (2^nd ‘𝑧), 0, (𝑦 + 1)) = 0)
116	111, 115	sylan9eqr 2666	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) = 0)
117	116	csbeq1d 3506	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋0 / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))
118		c0ex 9913	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ V
119		oveq2 6557	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = 0 → (1...𝑗) = (1...0))
120		fz10 12233	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1...0) = ∅
121	119, 120	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 0 → (1...𝑗) = ∅)
122	121	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 0 → ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑧)) “ ∅))
123	122	xpeq1d 5062	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}))
124		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = 0 → (𝑗 + 1) = (0 + 1))
125		0p1e1 11009	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 + 1) = 1
126	124, 125	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = 0 → (𝑗 + 1) = 1)
127	126	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 0 → ((𝑗 + 1)...𝑁) = (1...𝑁))
128	127	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 0 → ((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)))
129	128	xpeq1d 5062	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
130	123, 129	uneq12d 3730	. . . . . . . . . . . . . . . . . . . 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})))
131		ima0 5400	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2^nd ‘(1^st ‘𝑧)) “ ∅) = ∅
132	131	xpeq1i 5059	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) = (∅ × {1})
133		0xp 5122	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∅ × {1}) = ∅
134	132, 133	eqtri 2632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) = ∅
135	134	uneq1i 3725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = (∅ ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
136		uncom 3719	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∅ ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}) ∪ ∅)
137		un0 3919	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}) ∪ ∅) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})
138	135, 136, 137	3eqtri 2636	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})
139	130, 138	syl6eq 2660	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 0 → ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
140	139	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 0 → ((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})))
141	118, 140	csbie 3525	. . . . . . . . . . . . . . . . 17 ⊢ ⦋0 / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
142		f1ofo 6057	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–onto→(1...𝑁))
143	91, 142	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ 𝑆 → (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–onto→(1...𝑁))
144		foima 6033	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2^nd ‘(1^st ‘𝑧)):(1...𝑁)–onto→(1...𝑁) → ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) = (1...𝑁))
145	143, 144	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝑆 → ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) = (1...𝑁))
146	145	xpeq1d 5062	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}) = ((1...𝑁) × {0}))
147	146	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑆 → ((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = ((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((1...𝑁) × {0})))
148		ovex 6577	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...𝑁) ∈ V
149	148	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (1...𝑁) ∈ V)
150		ffn 5958	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶(0..^𝐾) → (1^st ‘(1^st ‘𝑧)) Fn (1...𝑁))
151	82, 150	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘(1^st ‘𝑧)) Fn (1...𝑁))
152		fnconstg 6006	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
153	118, 152	mp1i 13	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → ((1...𝑁) × {0}) Fn (1...𝑁))
154		eqidd 2611	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) = ((1^st ‘(1^st ‘𝑧))‘𝑛))
155	118	fvconst2 6374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
156	155	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
157	82	ffvelrnda 6267	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ (0..^𝐾))
158		elfzonn0 12380	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ ℕ₀)
159	157, 158	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ ℕ₀)
160	159	nn0cnd 11230	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ ℂ)
161	160	addid1d 10115	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑧))‘𝑛) + 0) = ((1^st ‘(1^st ‘𝑧))‘𝑛))
162	149, 151, 153, 151, 154, 156, 161	offveq 6816	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑆 → ((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((1...𝑁) × {0})) = (1^st ‘(1^st ‘𝑧)))
163	147, 162	eqtrd 2644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 → ((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = (1^st ‘(1^st ‘𝑧)))
164	141, 163	syl5eq 2656	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 → ⦋0 / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1^st ‘(1^st ‘𝑧)))
165	164	ad2antlr 759	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → ⦋0 / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1^st ‘(1^st ‘𝑧)))
166	117, 165	eqtrd 2644	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → ⦋if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑧)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1^st ‘(1^st ‘𝑧)))
167		nnm1nn0 11211	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
168	1, 167	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
169		0elfz 12305	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 − 1) ∈ ℕ₀ → 0 ∈ (0...(𝑁 − 1)))
170	168, 169	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ (0...(𝑁 − 1)))
171	170	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → 0 ∈ (0...(𝑁 − 1)))
172		fvex 6113	. . . . . . . . . . . . . . 15 ⊢ (1^st ‘(1^st ‘𝑧)) ∈ V
173	172	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (1^st ‘(1^st ‘𝑧)) ∈ V)
174	108, 166, 171, 173	fvmptd 6197	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧)))
175	107, 174	sylan 487	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) ∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧)))
176	175	an32s 842	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧)))
177	103, 176	mpdan 699	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧)))
178		fveq2 6103	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑇 → (2^nd ‘𝑧) = (2^nd ‘𝑇))
179	178	eleq1d 2672	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑇 → ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))))
180	179	anbi2d 736	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑇 → ((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ↔ (𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))))
181		fveq2 6103	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑇 → (1^st ‘𝑧) = (1^st ‘𝑇))
182	181	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑇 → (1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)))
183	182	eqeq2d 2620	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑇 → ((𝐹‘0) = (1^st ‘(1^st ‘𝑧)) ↔ (𝐹‘0) = (1^st ‘(1^st ‘𝑇))))
184	180, 183	imbi12d 333	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑇 → (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧))) ↔ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^st ‘(1^st ‘𝑇)))))
185	174	expcom 450	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑆 → ((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧))))
186	184, 185	vtoclga 3245	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ 𝑆 → ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^st ‘(1^st ‘𝑇))))
187	7, 186	mpcom 37	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^st ‘(1^st ‘𝑇)))
188	187	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^st ‘(1^st ‘𝑇)))
189	177, 188	eqtr3d 2646	. . . . . . . . 9 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)))
190	189	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)))
191	1	ad3antrrr 762	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑁 ∈ ℕ)
192	6	ad3antrrr 762	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑇 ∈ 𝑆)
193		simpllr 795	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
194		simplr 788	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑧 ∈ 𝑆)
195	35	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
196		xpopth 7098	. . . . . . . . . . . . . 14 ⊢ (((1^st ‘𝑧) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (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 ‘𝑇)))
197	78, 195, 196	syl2anr 494	. . . . . . . . . . . . 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 ‘𝑇)))
198	33	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
199		xpopth 7098	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1^st ‘𝑧) = (1^st ‘𝑇) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) ↔ 𝑧 = 𝑇))
200	199	biimpd 218	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1^st ‘𝑧) = (1^st ‘𝑇) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → 𝑧 = 𝑇))
201	76, 198, 200	syl2anr 494	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (((1^st ‘𝑧) = (1^st ‘𝑇) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → 𝑧 = 𝑇))
202	103, 201	mpan2d 706	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ((1^st ‘𝑧) = (1^st ‘𝑇) → 𝑧 = 𝑇))
203	197, 202	sylbid 229	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (((1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)) ∧ (2^nd ‘(1^st ‘𝑧)) = (2^nd ‘(1^st ‘𝑇))) → 𝑧 = 𝑇))
204	189, 203	mpand 707	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ((2^nd ‘(1^st ‘𝑧)) = (2^nd ‘(1^st ‘𝑇)) → 𝑧 = 𝑇))
205	204	necon3d 2803	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (2^nd ‘(1^st ‘𝑧)) ≠ (2^nd ‘(1^st ‘𝑇))))
206	205	imp 444	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^nd ‘(1^st ‘𝑧)) ≠ (2^nd ‘(1^st ‘𝑇)))
207	191, 3, 192, 193, 194, 206	poimirlem9 32588	. . . . . . . 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)})))))
208	103	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^nd ‘𝑧) = (2^nd ‘𝑇))
209	190, 207, 208	jca31 555	. . . . . . 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 ‘𝑇)))
210	209	ex 449	. . . . . 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 ‘𝑇))))
211		simplr 788	. . . . . . . 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)})))))
212		elfznn 12241	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ∈ ℕ)
213	212	nnred 10912	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ∈ ℝ)
214	213	ltp1d 10833	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
215	213, 214	ltned 10052	. . . . . . . . . . . 12 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
216	215	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
217		fveq1 6102	. . . . . . . . . . . . 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 ‘𝑇)))
218		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2^nd ‘𝑇) ∈ ℝ → (2^nd ‘𝑇) ∈ ℝ)
219		ltp1 10740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2^nd ‘𝑇) ∈ ℝ → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
220	218, 219	ltned 10052	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2^nd ‘𝑇) ∈ ℝ → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
221		fvex 6113	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2^nd ‘𝑇) ∈ V
222		ovex 6577	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2^nd ‘𝑇) + 1) ∈ V
223	221, 222, 222, 221	fpr 6326	. . . . . . . . . . . . . . . . . . . . 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 ‘𝑇)})
224	220, 223	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 ‘𝑇)})
225		f1oi 6086	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})):((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})–1-1-onto→((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
226		f1of 6050	. . . . . . . . . . . . . . . . . . . . 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)}))
227	225, 226	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})):((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})⟶((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
228		disjdif 3992	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅
229		fun 5979	. . . . . . . . . . . . . . . . . . . . 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)})))
230	228, 229	mpan2 703	. . . . . . . . . . . . . . . . . . . 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)})))
231	224, 227, 230	sylancl 693	. . . . . . . . . . . . . . . . . . 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)})))
232	221	prid1 4241	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2^nd ‘𝑇) ∈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}
233		elun1 3742	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑇) ∈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} → (2^nd ‘𝑇) ∈ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})))
234	232, 233	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (2^nd ‘𝑇) ∈ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}))
235		fvco3 6185	. . . . . . . . . . . . . . . . . . 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 ‘𝑇))))
236	231, 234, 235	sylancl 693	. . . . . . . . . . . . . . . . . 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 ‘𝑇))))
237		ffn 5958	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}:{(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}⟶{((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)} → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
238	224, 237	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2^nd ‘𝑇) ∈ ℝ → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
239		fnresi 5922	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) Fn ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
240	228, 232	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅ ∧ (2^nd ‘𝑇) ∈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
241		fvun1 6179	. . . . . . . . . . . . . . . . . . . . . 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 ‘𝑇)))
242	239, 240, 241	mp3an23 1408	. . . . . . . . . . . . . . . . . . . . 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 ‘𝑇)))
243	238, 242	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 ‘𝑇)))
244	221, 222	fvpr1 6361	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1) → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}‘(2^nd ‘𝑇)) = ((2^nd ‘𝑇) + 1))
245	220, 244	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑇) ∈ ℝ → ({⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩}‘(2^nd ‘𝑇)) = ((2^nd ‘𝑇) + 1))
246	243, 245	eqtrd 2644	. . . . . . . . . . . . . . . . . . 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))
247	246	fveq2d 6107	. . . . . . . . . . . . . . . . . 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)))
248	236, 247	eqtrd 2644	. . . . . . . . . . . . . . . . 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)))
249	213, 248	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)))
250	249	eqeq2d 2620	. . . . . . . . . . . . . . 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))))
251	250	adantl 481	. . . . . . . . . . . . . 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))))
252		f1of1 6049	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁))
253	50, 252	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁))
254	253	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁))
255	1	nncnd 10913	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℂ)
256		npcan1 10334	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
257	255, 256	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
258	168	nn0zd 11356	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
259		uzid 11578	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
260	258, 259	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
261		peano2uz 11617	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
262	260, 261	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
263	257, 262	eqeltrrd 2689	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
264		fzss2 12252	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
265	263, 264	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
266	265	sselda 3568	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘𝑇) ∈ (1...𝑁))
267		fzp1elp1 12264	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → ((2^nd ‘𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
268	267	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((2^nd ‘𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
269	257	oveq2d 6565	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
270	269	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (1...((𝑁 − 1) + 1)) = (1...𝑁))
271	268, 270	eleqtrd 2690	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((2^nd ‘𝑇) + 1) ∈ (1...𝑁))
272		f1veqaeq 6418	. . . . . . . . . . . . . . 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)))
273	254, 266, 271, 272	syl12anc 1316	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) = ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) → (2^nd ‘𝑇) = ((2^nd ‘𝑇) + 1)))
274	251, 273	sylbid 229	. . . . . . . . . . . . 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)))
275	217, 274	syl5 33	. . . . . . . . . . . 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)))
276	275	necon3d 2803	. . . . . . . . . . 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)}))))))
277	216, 276	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)})))))
278	181	fveq2d 6107	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑇 → (2^nd ‘(1^st ‘𝑧)) = (2^nd ‘(1^st ‘𝑇)))
279	278	neeq1d 2841	. . . . . . . . . 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)}))))))
280	277, 279	syl5ibrcom 236	. . . . . . . . 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)}))))))
281	280	necon2d 2805	. . . . . . . 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)})))) → 𝑧 ≠ 𝑇))
282	211, 281	syl5 33	. . . . . . 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 ‘𝑇)) → 𝑧 ≠ 𝑇))
283	282	adantr 480	. . . . . 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 ‘𝑇)) → 𝑧 ≠ 𝑇))
284	210, 283	impbid 201	. . . . 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 ‘𝑇))))
285		eqop 7099	. . . . . . . 8 ⊢ (𝑧 ∈ ((((0..^𝐾) ↑_𝑚 (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 ‘𝑇))))
286		eqop 7099	. . . . . . . . . 10 ⊢ ((1^st ‘𝑧) ∈ (((0..^𝐾) ↑_𝑚 (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)})))))))
287	77, 286	syl 17	. . . . . . . . 9 ⊢ (𝑧 ∈ ((((0..^𝐾) ↑_𝑚 (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)})))))))
288	287	anbi1d 737	. . . . . . . 8 ⊢ (𝑧 ∈ ((((0..^𝐾) ↑_𝑚 (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 ‘𝑇))))
289	285, 288	bitrd 267	. . . . . . 7 ⊢ (𝑧 ∈ ((((0..^𝐾) ↑_𝑚 (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 ‘𝑇))))
290	76, 289	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 ‘𝑇))))
291	290	adantl 481	. . . . 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 ‘𝑇))))
292	284, 291	bitr4d 270	. . . 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 ‘𝑇)⟩))
293	292	ralrimiva 2949	. . 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 ‘𝑇)⟩))
294		reu6i 3364	. . 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 ‘𝑇)⟩)) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
295	9, 293, 294	syl2anc 691	. 2 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
296		xp2nd 7090	. . . . . . 7 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2^nd ‘𝑇) ∈ (0...𝑁))
297	33, 296	syl 17	. . . . . 6 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (0...𝑁))
298	297	biantrurd 528	. . . . 5 ⊢ (𝜑 → (¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) ↔ ((2^nd ‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))))
299	1	nnnn0d 11228	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
300		nn0uz 11598	. . . . . . . . . . . 12 ⊢ ℕ₀ = (ℤ_≥‘0)
301	299, 300	syl6eleq 2698	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
302		fzpred 12259	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘0) → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
303	301, 302	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
304	125	oveq1i 6559	. . . . . . . . . . 11 ⊢ ((0 + 1)...𝑁) = (1...𝑁)
305	304	uneq2i 3726	. . . . . . . . . 10 ⊢ ({0} ∪ ((0 + 1)...𝑁)) = ({0} ∪ (1...𝑁))
306	303, 305	syl6eq 2660	. . . . . . . . 9 ⊢ (𝜑 → (0...𝑁) = ({0} ∪ (1...𝑁)))
307	306	difeq1d 3689	. . . . . . . 8 ⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))))
308		difundir 3839	. . . . . . . . . 10 ⊢ (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = (({0} ∖ (1...(𝑁 − 1))) ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
309		0lt1 10429	. . . . . . . . . . . . . 14 ⊢ 0 < 1
310		0re 9919	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
311		1re 9918	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
312	310, 311	ltnlei 10037	. . . . . . . . . . . . . 14 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
313	309, 312	mpbi 219	. . . . . . . . . . . . 13 ⊢ ¬ 1 ≤ 0
314		elfzle1 12215	. . . . . . . . . . . . 13 ⊢ (0 ∈ (1...(𝑁 − 1)) → 1 ≤ 0)
315	313, 314	mto 187	. . . . . . . . . . . 12 ⊢ ¬ 0 ∈ (1...(𝑁 − 1))
316		incom 3767	. . . . . . . . . . . . . 14 ⊢ ((1...(𝑁 − 1)) ∩ {0}) = ({0} ∩ (1...(𝑁 − 1)))
317	316	eqeq1i 2615	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {0}) = ∅ ↔ ({0} ∩ (1...(𝑁 − 1))) = ∅)
318		disjsn 4192	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (1...(𝑁 − 1)))
319		disj3 3973	. . . . . . . . . . . . 13 ⊢ (({0} ∩ (1...(𝑁 − 1))) = ∅ ↔ {0} = ({0} ∖ (1...(𝑁 − 1))))
320	317, 318, 319	3bitr3i 289	. . . . . . . . . . . 12 ⊢ (¬ 0 ∈ (1...(𝑁 − 1)) ↔ {0} = ({0} ∖ (1...(𝑁 − 1))))
321	315, 320	mpbi 219	. . . . . . . . . . 11 ⊢ {0} = ({0} ∖ (1...(𝑁 − 1)))
322	321	uneq1i 3725	. . . . . . . . . 10 ⊢ ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1)))) = (({0} ∖ (1...(𝑁 − 1))) ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
323	308, 322	eqtr4i 2635	. . . . . . . . 9 ⊢ (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
324		difundir 3839	. . . . . . . . . . . 12 ⊢ (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))) = (((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) ∪ ({𝑁} ∖ (1...(𝑁 − 1))))
325		difid 3902	. . . . . . . . . . . . 13 ⊢ ((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) = ∅
326	325	uneq1i 3725	. . . . . . . . . . . 12 ⊢ (((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1))))
327		uncom 3719	. . . . . . . . . . . . 13 ⊢ (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = (({𝑁} ∖ (1...(𝑁 − 1))) ∪ ∅)
328		un0 3919	. . . . . . . . . . . . 13 ⊢ (({𝑁} ∖ (1...(𝑁 − 1))) ∪ ∅) = ({𝑁} ∖ (1...(𝑁 − 1)))
329	327, 328	eqtri 2632	. . . . . . . . . . . 12 ⊢ (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = ({𝑁} ∖ (1...(𝑁 − 1)))
330	324, 326, 329	3eqtri 2636	. . . . . . . . . . 11 ⊢ (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))) = ({𝑁} ∖ (1...(𝑁 − 1)))
331		nnuz 11599	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
332	1, 331	syl6eleq 2698	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
333	257, 332	eqeltrd 2688	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘1))
334		fzsplit2 12237	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 − 1) + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
335	333, 263, 334	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
336	257	oveq1d 6564	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
337	1	nnzd 11357	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℤ)
338		fzsn 12254	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
339	337, 338	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁...𝑁) = {𝑁})
340	336, 339	eqtrd 2644	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
341	340	uneq2d 3729	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁}))
342	335, 341	eqtrd 2644	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁}))
343	342	difeq1d 3689	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))))
344	1	nnred 10912	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℝ)
345	344	ltm1d 10835	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
346	168	nn0red 11229	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
347	346, 344	ltnled 10063	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
348	345, 347	mpbid 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
349		elfzle2 12216	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
350	348, 349	nsyl 134	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
351		incom 3767	. . . . . . . . . . . . . 14 ⊢ ((1...(𝑁 − 1)) ∩ {𝑁}) = ({𝑁} ∩ (1...(𝑁 − 1)))
352	351	eqeq1i 2615	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ({𝑁} ∩ (1...(𝑁 − 1))) = ∅)
353		disjsn 4192	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1)))
354		disj3 3973	. . . . . . . . . . . . 13 ⊢ (({𝑁} ∩ (1...(𝑁 − 1))) = ∅ ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1))))
355	352, 353, 354	3bitr3i 289	. . . . . . . . . . . 12 ⊢ (¬ 𝑁 ∈ (1...(𝑁 − 1)) ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1))))
356	350, 355	sylib 207	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1))))
357	330, 343, 356	3eqtr4a 2670	. . . . . . . . . 10 ⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = {𝑁})
358	357	uneq2d 3729	. . . . . . . . 9 ⊢ (𝜑 → ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1)))) = ({0} ∪ {𝑁}))
359	323, 358	syl5eq 2656	. . . . . . . 8 ⊢ (𝜑 → (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = ({0} ∪ {𝑁}))
360	307, 359	eqtrd 2644	. . . . . . 7 ⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = ({0} ∪ {𝑁}))
361	360	eleq2d 2673	. . . . . 6 ⊢ (𝜑 → ((2^nd ‘𝑇) ∈ ((0...𝑁) ∖ (1...(𝑁 − 1))) ↔ (2^nd ‘𝑇) ∈ ({0} ∪ {𝑁})))
362		eldif 3550	. . . . . 6 ⊢ ((2^nd ‘𝑇) ∈ ((0...𝑁) ∖ (1...(𝑁 − 1))) ↔ ((2^nd ‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))))
363		elun 3715	. . . . . . 7 ⊢ ((2^nd ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2^nd ‘𝑇) ∈ {0} ∨ (2^nd ‘𝑇) ∈ {𝑁}))
364	221	elsn 4140	. . . . . . . 8 ⊢ ((2^nd ‘𝑇) ∈ {0} ↔ (2^nd ‘𝑇) = 0)
365	221	elsn 4140	. . . . . . . 8 ⊢ ((2^nd ‘𝑇) ∈ {𝑁} ↔ (2^nd ‘𝑇) = 𝑁)
366	364, 365	orbi12i 542	. . . . . . 7 ⊢ (((2^nd ‘𝑇) ∈ {0} ∨ (2^nd ‘𝑇) ∈ {𝑁}) ↔ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁))
367	363, 366	bitri 263	. . . . . 6 ⊢ ((2^nd ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁))
368	361, 362, 367	3bitr3g 301	. . . . 5 ⊢ (𝜑 → (((2^nd ‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ↔ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁)))
369	298, 368	bitrd 267	. . . 4 ⊢ (𝜑 → (¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) ↔ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁)))
370	369	biimpa 500	. . 3 ⊢ ((𝜑 ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁))
371	1	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → 𝑁 ∈ ℕ)
372	4	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_𝑚 (1...𝑁)))
373	6	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → 𝑇 ∈ 𝑆)
374		poimirlem22.4	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)
375	374	adantlr 747	. . . . 5 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) = 0) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)
376		simpr 476	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → (2^nd ‘𝑇) = 0)
377	371, 3, 372, 373, 375, 376	poimirlem18 32597	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
378	1	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → 𝑁 ∈ ℕ)
379	4	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_𝑚 (1...𝑁)))
380	6	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → 𝑇 ∈ 𝑆)
381		poimirlem22.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)
382	381	adantlr 747	. . . . 5 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)
383		simpr 476	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → (2^nd ‘𝑇) = 𝑁)
384	378, 3, 379, 380, 382, 383	poimirlem21 32600	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
385	377, 384	jaodan 822	. . 3 ⊢ ((𝜑 ∧ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁)) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
386	370, 385	syldan 486	. 2 ⊢ ((𝜑 ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
387	295, 386	pm2.61dan 828	1 ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 = wceq 1475 ∈ wcel 1977 {cab 2596 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 ∃!wreu 2898 ∃*wrmo 2899 {crab 2900 Vcvv 3173 ⦋csb 3499 ∖ cdif 3537 ∪ cun 3538 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 ifcif 4036 {csn 4125 {cpr 4127 ⟨cop 4131 class class class wbr 4583 ↦ cmpt 4643 I cid 4948 × cxp 5036 ran crn 5039 ↾ cres 5040 “ cima 5041 ∘ ccom 5042 Fn wfn 5799 ⟶wf 5800 –1-1→wf1 5801 –onto→wfo 5802 –1-1-onto→wf1o 5803 ‘cfv 5804 (class class class)co 6549 ∘_𝑓 cof 6793 1^st c1st 7057 2^nd c2nd 7058 ↑_𝑚 cmap 7744 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 < clt 9953 ≤ cle 9954 − cmin 10145 ℕcn 10897 ℕ₀cn0 11169 ℤcz 11254 ℤ_≥cuz 11563 ...cfz 12197 ..^cfzo 12334

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-of 6795 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-xnn0 11241 df-z 11255 df-uz 11564 df-fz 12198 df-fzo 12335 df-seq 12664 df-fac 12923 df-bc 12952 df-hash 12980

This theorem is referenced by: poimirlem27 32606

W3C validator