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 37628

Description: Lemma for poimir 37639, 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 480	. . . 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 480	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_m (1...𝑁)))
6		poimirlem22.2	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ 𝑆)
7	6	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → 𝑇 ∈ 𝑆)
8		simpr 484	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
9	2, 3, 5, 7, 8	poimirlem15 37621	. . 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 6906	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
11	10	breq2d 5159	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
12	11	ifbid 4553	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
13	12	csbeq1d 3911	. . . . . . . . . . . . . . . . . . . . 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 6911	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
15		2fveq3 6911	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
16	15	imaeq1d 6078	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
17	16	xpeq1d 5717	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
18	15	imaeq1d 6078	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
19	18	xpeq1d 5717	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
20	17, 19	uneq12d 4178	. . . . . . . . . . . . . . . . . . . . . . 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 7448	. . . . . . . . . . . . . . . . . . . . . 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 3914	. . . . . . . . . . . . . . . . . . . . 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 2774	. . . . . . . . . . . . . . . . . . . 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 2745	. . . . . . . . . . . . . . . . . 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 3697	. . . . . . . . . . . . . . . . 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 496	. . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . 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 3689	. . . . . . . . . . . . . . . . . . . . 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 2856	. . . . . . . . . . . . . . . . . . . 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 8044	. . . . . . . . . . . . . . . . . . 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 8044	. . . . . . . . . . . . . . . . . 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 8887	. . . . . . . . . . . . . . . . 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 13695	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ)
40	39	ssriv 3998	. . . . . . . . . . . . . . . 16 ⊢ (0..^𝐾) ⊆ ℤ
41		fss 6752	. . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶ℤ)
44		xp2nd 8045	. . . . . . . . . . . . . . . . 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 6919	. . . . . . . . . . . . . . . . 17 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
47		f1oeq1 6836	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
48	46, 47	elab 3680	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
49	45, 48	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
50	49	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
51	2, 29, 43, 50, 8	poimirlem1 37607	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛))
52	51	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛))
53	1	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → 𝑁 ∈ ℕ)
54		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → (2^nd ‘𝑡) = (2^nd ‘𝑧))
55	54	breq2d 5159	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑧)))
56	55	ifbid 4553	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)))
57	56	csbeq1d 3911	. . . . . . . . . . . . . . . . . . . . 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 6911	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑧)))
59		2fveq3 6911	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑧 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑧)))
60	59	imaeq1d 6078	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑧 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)))
61	60	xpeq1d 5717	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}))
62	59	imaeq1d 6078	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑧 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)))
63	62	xpeq1d 5717	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))
64	61, 63	uneq12d 4178	. . . . . . . . . . . . . . . . . . . . . . 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 7448	. . . . . . . . . . . . . . . . . . . . . 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 3914	. . . . . . . . . . . . . . . . . . . . 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 2774	. . . . . . . . . . . . . . . . . . . 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 2745	. . . . . . . . . . . . . . . . . 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 3697	. . . . . . . . . . . . . . . . 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 496	. . . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . 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 3689	. . . . . . . . . . . . . . . . . . . . 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 2856	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
75		xp1st 8044	. . . . . . . . . . . . . . . . . . . 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 8044	. . . . . . . . . . . . . . . . . . 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 8887	. . . . . . . . . . . . . . . . . 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 6752	. . . . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶ℤ)
84		xp2nd 8045	. . . . . . . . . . . . . . . . . 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 6919	. . . . . . . . . . . . . . . . . 18 ⊢ (2^nd ‘(1^st ‘𝑧)) ∈ V
87		f1oeq1 6836	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)))
88	86, 87	elab 3680	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘(1^st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
89	85, 88	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 → (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
90	89	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
91		simpllr 776	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
92		xp2nd 8045	. . . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (2^nd ‘𝑧) ∈ (0...𝑁))
95		eldifsn 4790	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘𝑧) ∈ ((0...𝑁) ∖ {(2^nd ‘𝑇)}) ↔ ((2^nd ‘𝑧) ∈ (0...𝑁) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)))
96	95	biimpri 228	. . . . . . . . . . . . . . . 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 37608	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛))
99	98	ex 412	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ((2^nd ‘𝑧) ≠ (2^nd ‘𝑇) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛)))
100	99	necon1bd 2955	. . . . . . . . . . . 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 2826	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘𝑧) = (2^nd ‘𝑇) → ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))))
103	102	biimparc 479	. . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → (𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))))
106	71	adantl 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})))))
107		breq1 5150	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 0 → (𝑦 < (2^nd ‘𝑧) ↔ 0 < (2^nd ‘𝑧)))
108		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 0 → 𝑦 = 0)
109	107, 108	ifbieq1d 4554	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 0 → if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) = if(0 < (2^nd ‘𝑧), 0, (𝑦 + 1)))
110		elfznn 13589	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑧) ∈ ℕ)
111	110	nngt0d 12312	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → 0 < (2^nd ‘𝑧))
112	111	iftrued 4538	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → if(0 < (2^nd ‘𝑧), 0, (𝑦 + 1)) = 0)
113	112	ad2antlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → if(0 < (2^nd ‘𝑧), 0, (𝑦 + 1)) = 0)
114	109, 113	sylan9eqr 2796	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) = 0)
115	114	csbeq1d 3911	. . . . . . . . . . . . . . 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 11252	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ V
117		oveq2 7438	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = 0 → (1...𝑗) = (1...0))
118		fz10 13581	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1...0) = ∅
119	117, 118	eqtrdi 2790	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 0 → (1...𝑗) = ∅)
120	119	imaeq2d 6079	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 0 → ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑧)) “ ∅))
121	120	xpeq1d 5717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}))
122		oveq1 7437	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = 0 → (𝑗 + 1) = (0 + 1))
123		0p1e1 12385	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 + 1) = 1
124	122, 123	eqtrdi 2790	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = 0 → (𝑗 + 1) = 1)
125	124	oveq1d 7445	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 0 → ((𝑗 + 1)...𝑁) = (1...𝑁))
126	125	imaeq2d 6079	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 0 → ((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)))
127	126	xpeq1d 5717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
128	121, 127	uneq12d 4178	. . . . . . . . . . . . . . . . . . . 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 6096	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2^nd ‘(1^st ‘𝑧)) “ ∅) = ∅
130	129	xpeq1i 5714	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) = (∅ × {1})
131		0xp 5786	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∅ × {1}) = ∅
132	130, 131	eqtri 2762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) = ∅
133	132	uneq1i 4173	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = (∅ ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
134		uncom 4167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∅ ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}) ∪ ∅)
135		un0 4399	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}) ∪ ∅) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})
136	133, 134, 135	3eqtri 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})
137	128, 136	eqtrdi 2790	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 0 → ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
138	137	oveq2d 7446	. . . . . . . . . . . . . . . . . 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 3943	. . . . . . . . . . . . . . . . 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 6855	. . . . . . . . . . . . . . . . . . . . . 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 6825	. . . . . . . . . . . . . . . . . . . . 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 5717	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}) = ((1...𝑁) × {0}))
145	144	oveq2d 7446	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑆 → ((1^st ‘(1^st ‘𝑧)) ∘_f + (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = ((1^st ‘(1^st ‘𝑧)) ∘_f + ((1...𝑁) × {0})))
146		ovexd 7465	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (1...𝑁) ∈ V)
147	80	ffnd 6737	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘(1^st ‘𝑧)) Fn (1...𝑁))
148		fnconstg 6796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
149	116, 148	mp1i 13	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → ((1...𝑁) × {0}) Fn (1...𝑁))
150		eqidd 2735	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) = ((1^st ‘(1^st ‘𝑧))‘𝑛))
151	116	fvconst2 7223	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
152	151	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
153	80	ffvelcdmda 7103	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ (0..^𝐾))
154		elfzonn0 13743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ ℕ₀)
155	153, 154	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ ℕ₀)
156	155	nn0cnd 12586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ ℂ)
157	156	addridd 11458	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑧))‘𝑛) + 0) = ((1^st ‘(1^st ‘𝑧))‘𝑛))
158	146, 147, 149, 147, 150, 152, 157	offveq 7722	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑆 → ((1^st ‘(1^st ‘𝑧)) ∘_f + ((1...𝑁) × {0})) = (1^st ‘(1^st ‘𝑧)))
159	145, 158	eqtrd 2774	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 → ((1^st ‘(1^st ‘𝑧)) ∘_f + (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = (1^st ‘(1^st ‘𝑧)))
160	139, 159	eqtrid 2786	. . . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . 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 2774	. . . . . . . . . . . . . 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 12564	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
164	1, 163	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
165		0elfz 13660	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 − 1) ∈ ℕ₀ → 0 ∈ (0...(𝑁 − 1)))
166	164, 165	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ (0...(𝑁 − 1)))
167	166	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → 0 ∈ (0...(𝑁 − 1)))
168		fvexd 6921	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (1^st ‘(1^st ‘𝑧)) ∈ V)
169	106, 162, 167, 168	fvmptd 7022	. . . . . . . . . . . . 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 652	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧)))
172	101, 171	mpdan 687	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧)))
173		fveq2 6906	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑇 → (2^nd ‘𝑧) = (2^nd ‘𝑇))
174	173	eleq1d 2823	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑇 → ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))))
175	174	anbi2d 630	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑇 → ((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ↔ (𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))))
176		2fveq3 6911	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑇 → (1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)))
177	176	eqeq2d 2745	. . . . . . . . . . . . . 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 413	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑆 → ((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧))))
180	178, 179	vtoclga 3576	. . . . . . . . . . . 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 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^st ‘(1^st ‘𝑇)))
183	172, 182	eqtr3d 2776	. . . . . . . . 9 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)))
184	183	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)))
185	1	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑁 ∈ ℕ)
186	6	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑇 ∈ 𝑆)
187		simpllr 776	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
188		simplr 769	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑧 ∈ 𝑆)
189	34	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
190		xpopth 8053	. . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
193		xpopth 8053	. . . . . . . . . . . . . . . 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 229	. . . . . . . . . . . . . . 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 694	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ((1^st ‘𝑧) = (1^st ‘𝑇) → 𝑧 = 𝑇))
197	191, 196	sylbid 240	. . . . . . . . . . . 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 695	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ((2^nd ‘(1^st ‘𝑧)) = (2^nd ‘(1^st ‘𝑇)) → 𝑧 = 𝑇))
199	198	necon3d 2958	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (2^nd ‘(1^st ‘𝑧)) ≠ (2^nd ‘(1^st ‘𝑇))))
200	199	imp 406	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^nd ‘(1^st ‘𝑧)) ≠ (2^nd ‘(1^st ‘𝑇)))
201	185, 3, 186, 187, 188, 200	poimirlem9 37615	. . . . . . . 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 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^nd ‘𝑧) = (2^nd ‘𝑇))
203	184, 201, 202	jca31 514	. . . . . . 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 412	. . . . . 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 769	. . . . . . . 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 13589	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ∈ ℕ)
207	206	nnred 12278	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ∈ ℝ)
208	207	ltp1d 12195	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
209	207, 208	ltned 11394	. . . . . . . . . . . 12 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
210	209	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
211		fveq1 6905	. . . . . . . . . . . . 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 12104	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2^nd ‘𝑇) ∈ ℝ → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
214	212, 213	ltned 11394	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2^nd ‘𝑇) ∈ ℝ → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
215		fvex 6919	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2^nd ‘𝑇) ∈ V
216		ovex 7463	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2^nd ‘𝑇) + 1) ∈ V
217	215, 216, 216, 215	fpr 7173	. . . . . . . . . . . . . . . . . . . . 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 6886	. . . . . . . . . . . . . . . . . . . . 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 6848	. . . . . . . . . . . . . . . . . . . . 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 4477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅
223		fun 6770	. . . . . . . . . . . . . . . . . . . . 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 691	. . . . . . . . . . . . . . . . . . . 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 4766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2^nd ‘𝑇) ∈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}
227		elun1 4191	. . . . . . . . . . . . . . . . . . . 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 7007	. . . . . . . . . . . . . . . . . . 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 6737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2^nd ‘𝑇) ∈ ℝ → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
232		fnresi 6697	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) Fn ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
233	222, 226	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅ ∧ (2^nd ‘𝑇) ∈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
234		fvun1 6999	. . . . . . . . . . . . . . . . . . . . . 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 1452	. . . . . . . . . . . . . . . . . . . . 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 7211	. . . . . . . . . . . . . . . . . . . . 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 2774	. . . . . . . . . . . . . . . . . . 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 6910	. . . . . . . . . . . . . . . . . 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 2774	. . . . . . . . . . . . . . . . 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 2745	. . . . . . . . . . . . . . 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 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))))
245		f1of1 6847	. . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁))
248	1	nncnd 12279	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℂ)
249		npcan1 11685	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
250	248, 249	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
251	164	nn0zd 12636	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
252		uzid 12890	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
253	251, 252	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
254		peano2uz 12940	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
255	253, 254	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
256	250, 255	eqeltrrd 2839	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
257		fzss2 13600	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
258	256, 257	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
259	258	sselda 3994	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘𝑇) ∈ (1...𝑁))
260		fzp1elp1 13613	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → ((2^nd ‘𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
261	260	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((2^nd ‘𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
262	250	oveq2d 7446	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
263	262	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (1...((𝑁 − 1) + 1)) = (1...𝑁))
264	261, 263	eleqtrd 2840	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((2^nd ‘𝑇) + 1) ∈ (1...𝑁))
265		f1veqaeq 7276	. . . . . . . . . . . . . . 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 837	. . . . . . . . . . . . . 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 240	. . . . . . . . . . . . 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 2958	. . . . . . . . . . 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 6911	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑇 → (2^nd ‘(1^st ‘𝑧)) = (2^nd ‘(1^st ‘𝑇)))
272	271	neeq1d 2997	. . . . . . . . . 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 247	. . . . . . . . 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 2960	. . . . . . . 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 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 ‘𝑇)) → 𝑧 ≠ 𝑇))
277	204, 276	impbid 212	. . . . 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 8054	. . . . . . . 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 8054	. . . . . . . . . 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 631	. . . . . . . 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 279	. . . . . . 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 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 ‘𝑇))))
285	277, 284	bitr4d 282	. . . 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 3143	. . 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 3736	. . 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 8045	. . . . . . 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 532	. . . . 5 ⊢ (𝜑 → (¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) ↔ ((2^nd ‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))))
292	1	nnnn0d 12584	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
293		nn0uz 12917	. . . . . . . . . . . 12 ⊢ ℕ₀ = (ℤ_≥‘0)
294	292, 293	eleqtrdi 2848	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
295		fzpred 13608	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘0) → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
296	294, 295	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
297	123	oveq1i 7440	. . . . . . . . . . 11 ⊢ ((0 + 1)...𝑁) = (1...𝑁)
298	297	uneq2i 4174	. . . . . . . . . 10 ⊢ ({0} ∪ ((0 + 1)...𝑁)) = ({0} ∪ (1...𝑁))
299	296, 298	eqtrdi 2790	. . . . . . . . 9 ⊢ (𝜑 → (0...𝑁) = ({0} ∪ (1...𝑁)))
300	299	difeq1d 4134	. . . . . . . 8 ⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))))
301		difundir 4296	. . . . . . . . . 10 ⊢ (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = (({0} ∖ (1...(𝑁 − 1))) ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
302		0lt1 11782	. . . . . . . . . . . . . 14 ⊢ 0 < 1
303		0re 11260	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
304		1re 11258	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
305	303, 304	ltnlei 11379	. . . . . . . . . . . . . 14 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
306	302, 305	mpbi 230	. . . . . . . . . . . . 13 ⊢ ¬ 1 ≤ 0
307		elfzle1 13563	. . . . . . . . . . . . 13 ⊢ (0 ∈ (1...(𝑁 − 1)) → 1 ≤ 0)
308	306, 307	mto 197	. . . . . . . . . . . 12 ⊢ ¬ 0 ∈ (1...(𝑁 − 1))
309		incom 4216	. . . . . . . . . . . . . 14 ⊢ ((1...(𝑁 − 1)) ∩ {0}) = ({0} ∩ (1...(𝑁 − 1)))
310	309	eqeq1i 2739	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {0}) = ∅ ↔ ({0} ∩ (1...(𝑁 − 1))) = ∅)
311		disjsn 4715	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (1...(𝑁 − 1)))
312		disj3 4459	. . . . . . . . . . . . 13 ⊢ (({0} ∩ (1...(𝑁 − 1))) = ∅ ↔ {0} = ({0} ∖ (1...(𝑁 − 1))))
313	310, 311, 312	3bitr3i 301	. . . . . . . . . . . 12 ⊢ (¬ 0 ∈ (1...(𝑁 − 1)) ↔ {0} = ({0} ∖ (1...(𝑁 − 1))))
314	308, 313	mpbi 230	. . . . . . . . . . 11 ⊢ {0} = ({0} ∖ (1...(𝑁 − 1)))
315	314	uneq1i 4173	. . . . . . . . . 10 ⊢ ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1)))) = (({0} ∖ (1...(𝑁 − 1))) ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
316	301, 315	eqtr4i 2765	. . . . . . . . 9 ⊢ (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
317		difundir 4296	. . . . . . . . . . . 12 ⊢ (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))) = (((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) ∪ ({𝑁} ∖ (1...(𝑁 − 1))))
318		difid 4381	. . . . . . . . . . . . 13 ⊢ ((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) = ∅
319	318	uneq1i 4173	. . . . . . . . . . . 12 ⊢ (((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1))))
320		uncom 4167	. . . . . . . . . . . . 13 ⊢ (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = (({𝑁} ∖ (1...(𝑁 − 1))) ∪ ∅)
321		un0 4399	. . . . . . . . . . . . 13 ⊢ (({𝑁} ∖ (1...(𝑁 − 1))) ∪ ∅) = ({𝑁} ∖ (1...(𝑁 − 1)))
322	320, 321	eqtri 2762	. . . . . . . . . . . 12 ⊢ (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = ({𝑁} ∖ (1...(𝑁 − 1)))
323	317, 319, 322	3eqtri 2766	. . . . . . . . . . 11 ⊢ (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))) = ({𝑁} ∖ (1...(𝑁 − 1)))
324		nnuz 12918	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
325	1, 324	eleqtrdi 2848	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
326	250, 325	eqeltrd 2838	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘1))
327		fzsplit2 13585	. . . . . . . . . . . . . 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 7445	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
330	1	nnzd 12637	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℤ)
331		fzsn 13602	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
332	330, 331	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁...𝑁) = {𝑁})
333	329, 332	eqtrd 2774	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
334	333	uneq2d 4177	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁}))
335	328, 334	eqtrd 2774	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁}))
336	335	difeq1d 4134	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))))
337	1	nnred 12278	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℝ)
338	337	ltm1d 12197	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
339	164	nn0red 12585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
340	339, 337	ltnled 11405	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
341	338, 340	mpbid 232	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
342		elfzle2 13564	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
343	341, 342	nsyl 140	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
344		incom 4216	. . . . . . . . . . . . . 14 ⊢ ((1...(𝑁 − 1)) ∩ {𝑁}) = ({𝑁} ∩ (1...(𝑁 − 1)))
345	344	eqeq1i 2739	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ({𝑁} ∩ (1...(𝑁 − 1))) = ∅)
346		disjsn 4715	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1)))
347		disj3 4459	. . . . . . . . . . . . 13 ⊢ (({𝑁} ∩ (1...(𝑁 − 1))) = ∅ ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1))))
348	345, 346, 347	3bitr3i 301	. . . . . . . . . . . 12 ⊢ (¬ 𝑁 ∈ (1...(𝑁 − 1)) ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1))))
349	343, 348	sylib 218	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1))))
350	323, 336, 349	3eqtr4a 2800	. . . . . . . . . 10 ⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = {𝑁})
351	350	uneq2d 4177	. . . . . . . . 9 ⊢ (𝜑 → ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1)))) = ({0} ∪ {𝑁}))
352	316, 351	eqtrid 2786	. . . . . . . 8 ⊢ (𝜑 → (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = ({0} ∪ {𝑁}))
353	300, 352	eqtrd 2774	. . . . . . 7 ⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = ({0} ∪ {𝑁}))
354	353	eleq2d 2824	. . . . . 6 ⊢ (𝜑 → ((2^nd ‘𝑇) ∈ ((0...𝑁) ∖ (1...(𝑁 − 1))) ↔ (2^nd ‘𝑇) ∈ ({0} ∪ {𝑁})))
355		eldif 3972	. . . . . 6 ⊢ ((2^nd ‘𝑇) ∈ ((0...𝑁) ∖ (1...(𝑁 − 1))) ↔ ((2^nd ‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))))
356		elun 4162	. . . . . . 7 ⊢ ((2^nd ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2^nd ‘𝑇) ∈ {0} ∨ (2^nd ‘𝑇) ∈ {𝑁}))
357	215	elsn 4645	. . . . . . . 8 ⊢ ((2^nd ‘𝑇) ∈ {0} ↔ (2^nd ‘𝑇) = 0)
358	215	elsn 4645	. . . . . . . 8 ⊢ ((2^nd ‘𝑇) ∈ {𝑁} ↔ (2^nd ‘𝑇) = 𝑁)
359	357, 358	orbi12i 914	. . . . . . 7 ⊢ (((2^nd ‘𝑇) ∈ {0} ∨ (2^nd ‘𝑇) ∈ {𝑁}) ↔ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁))
360	356, 359	bitri 275	. . . . . 6 ⊢ ((2^nd ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁))
361	354, 355, 360	3bitr3g 313	. . . . 5 ⊢ (𝜑 → (((2^nd ‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ↔ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁)))
362	291, 361	bitrd 279	. . . 4 ⊢ (𝜑 → (¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) ↔ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁)))
363	362	biimpa 476	. . 3 ⊢ ((𝜑 ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁))
364	1	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → 𝑁 ∈ ℕ)
365	4	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_m (1...𝑁)))
366	6	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → 𝑇 ∈ 𝑆)
367		poimirlem22.4	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)
368	367	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) = 0) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)
369		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → (2^nd ‘𝑇) = 0)
370	364, 3, 365, 366, 368, 369	poimirlem18 37624	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
371	1	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → 𝑁 ∈ ℕ)
372	4	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_m (1...𝑁)))
373	6	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → 𝑇 ∈ 𝑆)
374		poimirlem22.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)
375	374	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)
376		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → (2^nd ‘𝑇) = 𝑁)
377	371, 3, 372, 373, 375, 376	poimirlem21 37627	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
378	370, 377	jaodan 959	. . 3 ⊢ ((𝜑 ∧ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁)) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
379	363, 378	syldan 591	. 2 ⊢ ((𝜑 ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
380	288, 379	pm2.61dan 813	1 ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1536 ∈ wcel 2105 {cab 2711 ≠ wne 2937 ∀wral 3058 ∃wrex 3067 ∃!wreu 3375 ∃*wrmo 3376 {crab 3432 Vcvv 3477 ⦋csb 3907 ∖ cdif 3959 ∪ cun 3960 ∩ cin 3961 ⊆ wss 3962 ∅c0 4338 ifcif 4530 {csn 4630 {cpr 4632 ⟨cop 4636 class class class wbr 5147 ↦ cmpt 5230 I cid 5581 × cxp 5686 ran crn 5689 ↾ cres 5690 “ cima 5691 ∘ ccom 5692 Fn wfn 6557 ⟶wf 6558 –1-1→wf1 6559 –onto→wfo 6560 –1-1-onto→wf1o 6561 ‘cfv 6562 (class class class)co 7430 ∘_f cof 7694 1^st c1st 8010 2^nd c2nd 8011 ↑_m cmap 8864 ℂcc 11150 ℝcr 11151 0cc0 11152 1c1 11153 + caddc 11155 < clt 11292 ≤ cle 11293 − cmin 11489 ℕcn 12263 ℕ₀cn0 12523 ℤcz 12610 ℤ_≥cuz 12875 ...cfz 13543 ..^cfzo 13690

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-rep 5284 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 ax-cnex 11208 ax-resscn 11209 ax-1cn 11210 ax-icn 11211 ax-addcl 11212 ax-addrcl 11213 ax-mulcl 11214 ax-mulrcl 11215 ax-mulcom 11216 ax-addass 11217 ax-mulass 11218 ax-distr 11219 ax-i2m1 11220 ax-1ne0 11221 ax-1rid 11222 ax-rnegex 11223 ax-rrecex 11224 ax-cnre 11225 ax-pre-lttri 11226 ax-pre-lttrn 11227 ax-pre-ltadd 11228 ax-pre-mulgt0 11229

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rmo 3377 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-pss 3982 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-tp 4635 df-op 4637 df-uni 4912 df-int 4951 df-iun 4997 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5582 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5640 df-we 5642 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-pred 6322 df-ord 6388 df-on 6389 df-lim 6390 df-suc 6391 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-riota 7387 df-ov 7433 df-oprab 7434 df-mpo 7435 df-of 7696 df-om 7887 df-1st 8012 df-2nd 8013 df-frecs 8304 df-wrecs 8335 df-recs 8409 df-rdg 8448 df-1o 8504 df-2o 8505 df-oadd 8508 df-er 8743 df-map 8866 df-pm 8867 df-en 8984 df-dom 8985 df-sdom 8986 df-fin 8987 df-dju 9938 df-card 9976 df-pnf 11294 df-mnf 11295 df-xr 11296 df-ltxr 11297 df-le 11298 df-sub 11491 df-neg 11492 df-div 11918 df-nn 12264 df-2 12326 df-3 12327 df-n0 12524 df-xnn0 12597 df-z 12611 df-uz 12876 df-fz 13544 df-fzo 13691 df-seq 14039 df-fac 14309 df-bc 14338 df-hash 14366

This theorem is referenced by: poimirlem27 37633

W3C validator