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 35079

Description: Lemma for poimir 35090, 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 484	. . . 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 484	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_m (1...𝑁)))
6		poimirlem22.2	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ 𝑆)
7	6	adantr 484	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → 𝑇 ∈ 𝑆)
8		simpr 488	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
9	2, 3, 5, 7, 8	poimirlem15 35072	. . 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 6645	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
11	10	breq2d 5042	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
12	11	ifbid 4447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
13	12	csbeq1d 3832	. . . . . . . . . . . . . . . . . . . . 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 6650	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
15		2fveq3 6650	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
16	15	imaeq1d 5895	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
17	16	xpeq1d 5548	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
18	15	imaeq1d 5895	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
19	18	xpeq1d 5548	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
20	17, 19	uneq12d 4091	. . . . . . . . . . . . . . . . . . . . . . 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 7153	. . . . . . . . . . . . . . . . . . . . . 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 3835	. . . . . . . . . . . . . . . . . . . . 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 2833	. . . . . . . . . . . . . . . . . . . 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 5126	. . . . . . . . . . . . . . . . . . 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 2809	. . . . . . . . . . . . . . . . . 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 3631	. . . . . . . . . . . . . . . . 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 500	. . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . 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 3623	. . . . . . . . . . . . . . . . . . . . 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 2908	. . . . . . . . . . . . . . . . . . . 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 7703	. . . . . . . . . . . . . . . . . . 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 7703	. . . . . . . . . . . . . . . . . 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 8411	. . . . . . . . . . . . . . . . 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 13033	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ)
40	39	ssriv 3919	. . . . . . . . . . . . . . . 16 ⊢ (0..^𝐾) ⊆ ℤ
41		fss 6501	. . . . . . . . . . . . . . . 16 ⊢ (((1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶ℤ)
42	38, 40, 41	sylancl 589	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶ℤ)
43	42	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶ℤ)
44		xp2nd 7704	. . . . . . . . . . . . . . . . 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 6658	. . . . . . . . . . . . . . . . 17 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
47		f1oeq1 6579	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
48	46, 47	elab 3615	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
49	45, 48	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
50	49	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
51	2, 29, 43, 50, 8	poimirlem1 35058	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛))
52	51	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛))
53	1	ad3antrrr 729	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → 𝑁 ∈ ℕ)
54		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → (2^nd ‘𝑡) = (2^nd ‘𝑧))
55	54	breq2d 5042	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑧)))
56	55	ifbid 4447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)))
57	56	csbeq1d 3832	. . . . . . . . . . . . . . . . . . . . 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 6650	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑧)))
59		2fveq3 6650	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑧 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑧)))
60	59	imaeq1d 5895	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑧 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)))
61	60	xpeq1d 5548	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}))
62	59	imaeq1d 5895	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑧 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)))
63	62	xpeq1d 5548	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))
64	61, 63	uneq12d 4091	. . . . . . . . . . . . . . . . . . . . . . 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 7153	. . . . . . . . . . . . . . . . . . . . . 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 3835	. . . . . . . . . . . . . . . . . . . . 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 2833	. . . . . . . . . . . . . . . . . . . 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 5126	. . . . . . . . . . . . . . . . . . 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 2809	. . . . . . . . . . . . . . . . . 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 3631	. . . . . . . . . . . . . . . . 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 500	. . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . 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 3623	. . . . . . . . . . . . . . . . . . . . 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 2908	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
75		xp1st 7703	. . . . . . . . . . . . . . . . . . . 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 7703	. . . . . . . . . . . . . . . . . . 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 8411	. . . . . . . . . . . . . . . . . 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 6501	. . . . . . . . . . . . . . . . 17 ⊢ (((1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶ℤ)
82	80, 40, 81	sylancl 589	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶ℤ)
83	82	ad2antlr 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (1^st ‘(1^st ‘𝑧)):(1...𝑁)⟶ℤ)
84		xp2nd 7704	. . . . . . . . . . . . . . . . . 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 6658	. . . . . . . . . . . . . . . . . 18 ⊢ (2^nd ‘(1^st ‘𝑧)) ∈ V
87		f1oeq1 6579	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)))
88	86, 87	elab 3615	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘(1^st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
89	85, 88	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 → (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
90	89	ad2antlr 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))
91		simpllr 775	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
92		xp2nd 7704	. . . . . . . . . . . . . . . . . 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 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (2^nd ‘𝑧) ∈ (0...𝑁))
95		eldifsn 4680	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘𝑧) ∈ ((0...𝑁) ∖ {(2^nd ‘𝑇)}) ↔ ((2^nd ‘𝑧) ∈ (0...𝑁) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)))
96	95	biimpri 231	. . . . . . . . . . . . . . . 16 ⊢ (((2^nd ‘𝑧) ∈ (0...𝑁) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (2^nd ‘𝑧) ∈ ((0...𝑁) ∖ {(2^nd ‘𝑇)}))
97	94, 96	sylan 583	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (2^nd ‘𝑧) ∈ ((0...𝑁) ∖ {(2^nd ‘𝑇)}))
98	53, 72, 83, 90, 91, 97	poimirlem2 35059	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛))
99	98	ex 416	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ((2^nd ‘𝑧) ≠ (2^nd ‘𝑇) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2^nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2^nd ‘𝑇))‘𝑛)))
100	99	necon1bd 3005	. . . . . . . . . . . 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 2877	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘𝑧) = (2^nd ‘𝑇) → ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))))
103	102	biimparc 483	. . . . . . . . . . . . . . 15 ⊢ (((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → (2^nd ‘𝑧) ∈ (1...(𝑁 − 1)))
104	103	anim2i 619	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇))) → (𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))))
105	104	anassrs 471	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → (𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))))
106	71	adantl 485	. . . . . . . . . . . . . 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 5033	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 0 → (𝑦 < (2^nd ‘𝑧) ↔ 0 < (2^nd ‘𝑧)))
108		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 0 → 𝑦 = 0)
109	107, 108	ifbieq1d 4448	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 0 → if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) = if(0 < (2^nd ‘𝑧), 0, (𝑦 + 1)))
110		elfznn 12931	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑧) ∈ ℕ)
111	110	nngt0d 11674	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → 0 < (2^nd ‘𝑧))
112	111	iftrued 4433	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → if(0 < (2^nd ‘𝑧), 0, (𝑦 + 1)) = 0)
113	112	ad2antlr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → if(0 < (2^nd ‘𝑧), 0, (𝑦 + 1)) = 0)
114	109, 113	sylan9eqr 2855	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) = 0)
115	114	csbeq1d 3832	. . . . . . . . . . . . . . 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 10624	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ V
117		oveq2 7143	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = 0 → (1...𝑗) = (1...0))
118		fz10 12923	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1...0) = ∅
119	117, 118	eqtrdi 2849	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 0 → (1...𝑗) = ∅)
120	119	imaeq2d 5896	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 0 → ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑧)) “ ∅))
121	120	xpeq1d 5548	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}))
122		oveq1 7142	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = 0 → (𝑗 + 1) = (0 + 1))
123		0p1e1 11747	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 + 1) = 1
124	122, 123	eqtrdi 2849	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = 0 → (𝑗 + 1) = 1)
125	124	oveq1d 7150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 0 → ((𝑗 + 1)...𝑁) = (1...𝑁))
126	125	imaeq2d 5896	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 0 → ((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)))
127	126	xpeq1d 5548	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
128	121, 127	uneq12d 4091	. . . . . . . . . . . . . . . . . . . 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 5912	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2^nd ‘(1^st ‘𝑧)) “ ∅) = ∅
130	129	xpeq1i 5545	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) = (∅ × {1})
131		0xp 5613	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∅ × {1}) = ∅
132	130, 131	eqtri 2821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) = ∅
133	132	uneq1i 4086	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = (∅ ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
134		uncom 4080	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∅ ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}) ∪ ∅)
135		un0 4298	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}) ∪ ∅) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})
136	133, 134, 135	3eqtri 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})
137	128, 136	eqtrdi 2849	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 0 → ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
138	137	oveq2d 7151	. . . . . . . . . . . . . . . . . 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 3863	. . . . . . . . . . . . . . . . 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 6597	. . . . . . . . . . . . . . . . . . . . . 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 6570	. . . . . . . . . . . . . . . . . . . . 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 5548	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}) = ((1...𝑁) × {0}))
145	144	oveq2d 7151	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑆 → ((1^st ‘(1^st ‘𝑧)) ∘_f + (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = ((1^st ‘(1^st ‘𝑧)) ∘_f + ((1...𝑁) × {0})))
146		ovexd 7170	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (1...𝑁) ∈ V)
147	80	ffnd 6488	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘(1^st ‘𝑧)) Fn (1...𝑁))
148		fnconstg 6541	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
149	116, 148	mp1i 13	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → ((1...𝑁) × {0}) Fn (1...𝑁))
150		eqidd 2799	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) = ((1^st ‘(1^st ‘𝑧))‘𝑛))
151	116	fvconst2 6943	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
152	151	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
153	80	ffvelrnda 6828	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ (0..^𝐾))
154		elfzonn0 13077	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ ℕ₀)
155	153, 154	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ ℕ₀)
156	155	nn0cnd 11945	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ ℂ)
157	156	addid1d 10829	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑧))‘𝑛) + 0) = ((1^st ‘(1^st ‘𝑧))‘𝑛))
158	146, 147, 149, 147, 150, 152, 157	offveq 7410	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑆 → ((1^st ‘(1^st ‘𝑧)) ∘_f + ((1...𝑁) × {0})) = (1^st ‘(1^st ‘𝑧)))
159	145, 158	eqtrd 2833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 → ((1^st ‘(1^st ‘𝑧)) ∘_f + (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = (1^st ‘(1^st ‘𝑧)))
160	139, 159	syl5eq 2845	. . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . 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 2833	. . . . . . . . . . . . . 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 11926	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
164	1, 163	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
165		0elfz 12999	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 − 1) ∈ ℕ₀ → 0 ∈ (0...(𝑁 − 1)))
166	164, 165	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ (0...(𝑁 − 1)))
167	166	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → 0 ∈ (0...(𝑁 − 1)))
168		fvexd 6660	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (1^st ‘(1^st ‘𝑧)) ∈ V)
169	106, 162, 167, 168	fvmptd 6752	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧)))
170	105, 169	sylan 583	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) ∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧)))
171	170	an32s 651	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧)))
172	101, 171	mpdan 686	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧)))
173		fveq2 6645	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑇 → (2^nd ‘𝑧) = (2^nd ‘𝑇))
174	173	eleq1d 2874	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑇 → ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))))
175	174	anbi2d 631	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑇 → ((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ↔ (𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))))
176		2fveq3 6650	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑇 → (1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)))
177	176	eqeq2d 2809	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑇 → ((𝐹‘0) = (1^st ‘(1^st ‘𝑧)) ↔ (𝐹‘0) = (1^st ‘(1^st ‘𝑇))))
178	175, 177	imbi12d 348	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑇 → (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧))) ↔ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^st ‘(1^st ‘𝑇)))))
179	169	expcom 417	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑆 → ((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1^st ‘(1^st ‘𝑧))))
180	178, 179	vtoclga 3522	. . . . . . . . . . . 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 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1^st ‘(1^st ‘𝑇)))
183	172, 182	eqtr3d 2835	. . . . . . . . 9 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)))
184	183	adantr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)))
185	1	ad3antrrr 729	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑁 ∈ ℕ)
186	6	ad3antrrr 729	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑇 ∈ 𝑆)
187		simpllr 775	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
188		simplr 768	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑧 ∈ 𝑆)
189	34	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
190		xpopth 7712	. . . . . . . . . . . . . 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 599	. . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → 𝑇 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
193		xpopth 7712	. . . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . . . 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 599	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (((1^st ‘𝑧) = (1^st ‘𝑇) ∧ (2^nd ‘𝑧) = (2^nd ‘𝑇)) → 𝑧 = 𝑇))
196	101, 195	mpan2d 693	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ((1^st ‘𝑧) = (1^st ‘𝑇) → 𝑧 = 𝑇))
197	191, 196	sylbid 243	. . . . . . . . . . . 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 694	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → ((2^nd ‘(1^st ‘𝑧)) = (2^nd ‘(1^st ‘𝑇)) → 𝑧 = 𝑇))
199	198	necon3d 3008	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (2^nd ‘(1^st ‘𝑧)) ≠ (2^nd ‘(1^st ‘𝑇))))
200	199	imp 410	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^nd ‘(1^st ‘𝑧)) ≠ (2^nd ‘(1^st ‘𝑇)))
201	185, 3, 186, 187, 188, 200	poimirlem9 35066	. . . . . . . 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 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^nd ‘𝑧) = (2^nd ‘𝑇))
203	184, 201, 202	jca31 518	. . . . . . 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 416	. . . . . 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 768	. . . . . . . 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 12931	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ∈ ℕ)
207	206	nnred 11640	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ∈ ℝ)
208	207	ltp1d 11559	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
209	207, 208	ltned 10765	. . . . . . . . . . . 12 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
210	209	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
211		fveq1 6644	. . . . . . . . . . . . 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 11469	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2^nd ‘𝑇) ∈ ℝ → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
214	212, 213	ltned 10765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2^nd ‘𝑇) ∈ ℝ → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
215		fvex 6658	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2^nd ‘𝑇) ∈ V
216		ovex 7168	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2^nd ‘𝑇) + 1) ∈ V
217	215, 216, 216, 215	fpr 6893	. . . . . . . . . . . . . . . . . . . . 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 6627	. . . . . . . . . . . . . . . . . . . . 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 6590	. . . . . . . . . . . . . . . . . . . . 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 4379	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅
223		fun 6514	. . . . . . . . . . . . . . . . . . . . 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 690	. . . . . . . . . . . . . . . . . . . 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 589	. . . . . . . . . . . . . . . . . . 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 4658	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2^nd ‘𝑇) ∈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}
227		elun1 4103	. . . . . . . . . . . . . . . . . . . 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 6737	. . . . . . . . . . . . . . . . . . 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 589	. . . . . . . . . . . . . . . . . 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 6488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2^nd ‘𝑇) ∈ ℝ → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
232		fnresi 6448	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( I ↾ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) Fn ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
233	222, 226	pm3.2i 474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅ ∧ (2^nd ‘𝑇) ∈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
234		fvun1 6729	. . . . . . . . . . . . . . . . . . . . . 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 1450	. . . . . . . . . . . . . . . . . . . . 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 6929	. . . . . . . . . . . . . . . . . . . . 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 2833	. . . . . . . . . . . . . . . . . . 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 6649	. . . . . . . . . . . . . . . . . 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 2833	. . . . . . . . . . . . . . . . 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 2809	. . . . . . . . . . . . . . 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 485	. . . . . . . . . . . . . 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 6589	. . . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁))
248	1	nncnd 11641	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℂ)
249		npcan1 11054	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
250	248, 249	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
251	164	nn0zd 12073	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
252		uzid 12246	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
253	251, 252	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
254		peano2uz 12289	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
255	253, 254	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
256	250, 255	eqeltrrd 2891	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
257		fzss2 12942	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
258	256, 257	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
259	258	sselda 3915	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘𝑇) ∈ (1...𝑁))
260		fzp1elp1 12955	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → ((2^nd ‘𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
261	260	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((2^nd ‘𝑇) + 1) ∈ (1...((𝑁 − 1) + 1)))
262	250	oveq2d 7151	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
263	262	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (1...((𝑁 − 1) + 1)) = (1...𝑁))
264	261, 263	eleqtrd 2892	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((2^nd ‘𝑇) + 1) ∈ (1...𝑁))
265		f1veqaeq 6993	. . . . . . . . . . . . . . 15 ⊢ (((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ ((2^nd ‘𝑇) ∈ (1...𝑁) ∧ ((2^nd ‘𝑇) + 1) ∈ (1...𝑁))) → (((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) = ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) → (2^nd ‘𝑇) = ((2^nd ‘𝑇) + 1)))
266	247, 259, 264, 265	syl12anc 835	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (((2^nd ‘(1^st ‘𝑇))‘(2^nd ‘𝑇)) = ((2^nd ‘(1^st ‘𝑇))‘((2^nd ‘𝑇) + 1)) → (2^nd ‘𝑇) = ((2^nd ‘𝑇) + 1)))
267	244, 266	sylbid 243	. . . . . . . . . . . . 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 3008	. . . . . . . . . . 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 6650	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑇 → (2^nd ‘(1^st ‘𝑧)) = (2^nd ‘(1^st ‘𝑇)))
272	271	neeq1d 3046	. . . . . . . . . 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 250	. . . . . . . . 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 3010	. . . . . . . 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 484	. . . . . 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 215	. . . . 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 7713	. . . . . . . 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 7713	. . . . . . . . . 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 632	. . . . . . . 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 282	. . . . . . 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 485	. . . . 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 285	. . . 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 3149	. . 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 3667	. . 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 587	. 2 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
289		xp2nd 7704	. . . . . . 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 536	. . . . 5 ⊢ (𝜑 → (¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) ↔ ((2^nd ‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))))
292	1	nnnn0d 11943	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
293		nn0uz 12268	. . . . . . . . . . . 12 ⊢ ℕ₀ = (ℤ_≥‘0)
294	292, 293	eleqtrdi 2900	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
295		fzpred 12950	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘0) → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
296	294, 295	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
297	123	oveq1i 7145	. . . . . . . . . . 11 ⊢ ((0 + 1)...𝑁) = (1...𝑁)
298	297	uneq2i 4087	. . . . . . . . . 10 ⊢ ({0} ∪ ((0 + 1)...𝑁)) = ({0} ∪ (1...𝑁))
299	296, 298	eqtrdi 2849	. . . . . . . . 9 ⊢ (𝜑 → (0...𝑁) = ({0} ∪ (1...𝑁)))
300	299	difeq1d 4049	. . . . . . . 8 ⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))))
301		difundir 4207	. . . . . . . . . 10 ⊢ (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = (({0} ∖ (1...(𝑁 − 1))) ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
302		0lt1 11151	. . . . . . . . . . . . . 14 ⊢ 0 < 1
303		0re 10632	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
304		1re 10630	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
305	303, 304	ltnlei 10750	. . . . . . . . . . . . . 14 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
306	302, 305	mpbi 233	. . . . . . . . . . . . 13 ⊢ ¬ 1 ≤ 0
307		elfzle1 12905	. . . . . . . . . . . . 13 ⊢ (0 ∈ (1...(𝑁 − 1)) → 1 ≤ 0)
308	306, 307	mto 200	. . . . . . . . . . . 12 ⊢ ¬ 0 ∈ (1...(𝑁 − 1))
309		incom 4128	. . . . . . . . . . . . . 14 ⊢ ((1...(𝑁 − 1)) ∩ {0}) = ({0} ∩ (1...(𝑁 − 1)))
310	309	eqeq1i 2803	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {0}) = ∅ ↔ ({0} ∩ (1...(𝑁 − 1))) = ∅)
311		disjsn 4607	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (1...(𝑁 − 1)))
312		disj3 4361	. . . . . . . . . . . . 13 ⊢ (({0} ∩ (1...(𝑁 − 1))) = ∅ ↔ {0} = ({0} ∖ (1...(𝑁 − 1))))
313	310, 311, 312	3bitr3i 304	. . . . . . . . . . . 12 ⊢ (¬ 0 ∈ (1...(𝑁 − 1)) ↔ {0} = ({0} ∖ (1...(𝑁 − 1))))
314	308, 313	mpbi 233	. . . . . . . . . . 11 ⊢ {0} = ({0} ∖ (1...(𝑁 − 1)))
315	314	uneq1i 4086	. . . . . . . . . 10 ⊢ ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1)))) = (({0} ∖ (1...(𝑁 − 1))) ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
316	301, 315	eqtr4i 2824	. . . . . . . . 9 ⊢ (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
317		difundir 4207	. . . . . . . . . . . 12 ⊢ (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))) = (((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) ∪ ({𝑁} ∖ (1...(𝑁 − 1))))
318		difid 4284	. . . . . . . . . . . . 13 ⊢ ((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) = ∅
319	318	uneq1i 4086	. . . . . . . . . . . 12 ⊢ (((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1))))
320		uncom 4080	. . . . . . . . . . . . 13 ⊢ (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = (({𝑁} ∖ (1...(𝑁 − 1))) ∪ ∅)
321		un0 4298	. . . . . . . . . . . . 13 ⊢ (({𝑁} ∖ (1...(𝑁 − 1))) ∪ ∅) = ({𝑁} ∖ (1...(𝑁 − 1)))
322	320, 321	eqtri 2821	. . . . . . . . . . . 12 ⊢ (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = ({𝑁} ∖ (1...(𝑁 − 1)))
323	317, 319, 322	3eqtri 2825	. . . . . . . . . . 11 ⊢ (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))) = ({𝑁} ∖ (1...(𝑁 − 1)))
324		nnuz 12269	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
325	1, 324	eleqtrdi 2900	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
326	250, 325	eqeltrd 2890	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘1))
327		fzsplit2 12927	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 − 1) + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
328	326, 256, 327	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
329	250	oveq1d 7150	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
330	1	nnzd 12074	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℤ)
331		fzsn 12944	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
332	330, 331	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁...𝑁) = {𝑁})
333	329, 332	eqtrd 2833	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
334	333	uneq2d 4090	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁}))
335	328, 334	eqtrd 2833	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁}))
336	335	difeq1d 4049	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))))
337	1	nnred 11640	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℝ)
338	337	ltm1d 11561	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
339	164	nn0red 11944	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
340	339, 337	ltnled 10776	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
341	338, 340	mpbid 235	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
342		elfzle2 12906	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
343	341, 342	nsyl 142	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
344		incom 4128	. . . . . . . . . . . . . 14 ⊢ ((1...(𝑁 − 1)) ∩ {𝑁}) = ({𝑁} ∩ (1...(𝑁 − 1)))
345	344	eqeq1i 2803	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ({𝑁} ∩ (1...(𝑁 − 1))) = ∅)
346		disjsn 4607	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1)))
347		disj3 4361	. . . . . . . . . . . . 13 ⊢ (({𝑁} ∩ (1...(𝑁 − 1))) = ∅ ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1))))
348	345, 346, 347	3bitr3i 304	. . . . . . . . . . . 12 ⊢ (¬ 𝑁 ∈ (1...(𝑁 − 1)) ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1))))
349	343, 348	sylib 221	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1))))
350	323, 336, 349	3eqtr4a 2859	. . . . . . . . . 10 ⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = {𝑁})
351	350	uneq2d 4090	. . . . . . . . 9 ⊢ (𝜑 → ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1)))) = ({0} ∪ {𝑁}))
352	316, 351	syl5eq 2845	. . . . . . . 8 ⊢ (𝜑 → (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = ({0} ∪ {𝑁}))
353	300, 352	eqtrd 2833	. . . . . . 7 ⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = ({0} ∪ {𝑁}))
354	353	eleq2d 2875	. . . . . 6 ⊢ (𝜑 → ((2^nd ‘𝑇) ∈ ((0...𝑁) ∖ (1...(𝑁 − 1))) ↔ (2^nd ‘𝑇) ∈ ({0} ∪ {𝑁})))
355		eldif 3891	. . . . . 6 ⊢ ((2^nd ‘𝑇) ∈ ((0...𝑁) ∖ (1...(𝑁 − 1))) ↔ ((2^nd ‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))))
356		elun 4076	. . . . . . 7 ⊢ ((2^nd ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2^nd ‘𝑇) ∈ {0} ∨ (2^nd ‘𝑇) ∈ {𝑁}))
357	215	elsn 4540	. . . . . . . 8 ⊢ ((2^nd ‘𝑇) ∈ {0} ↔ (2^nd ‘𝑇) = 0)
358	215	elsn 4540	. . . . . . . 8 ⊢ ((2^nd ‘𝑇) ∈ {𝑁} ↔ (2^nd ‘𝑇) = 𝑁)
359	357, 358	orbi12i 912	. . . . . . 7 ⊢ (((2^nd ‘𝑇) ∈ {0} ∨ (2^nd ‘𝑇) ∈ {𝑁}) ↔ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁))
360	356, 359	bitri 278	. . . . . 6 ⊢ ((2^nd ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁))
361	354, 355, 360	3bitr3g 316	. . . . 5 ⊢ (𝜑 → (((2^nd ‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ↔ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁)))
362	291, 361	bitrd 282	. . . 4 ⊢ (𝜑 → (¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) ↔ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁)))
363	362	biimpa 480	. . 3 ⊢ ((𝜑 ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁))
364	1	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → 𝑁 ∈ ℕ)
365	4	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_m (1...𝑁)))
366	6	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → 𝑇 ∈ 𝑆)
367		poimirlem22.4	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)
368	367	adantlr 714	. . . . 5 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) = 0) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾)
369		simpr 488	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → (2^nd ‘𝑇) = 0)
370	364, 3, 365, 366, 368, 369	poimirlem18 35075	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 0) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
371	1	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → 𝑁 ∈ ℕ)
372	4	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_m (1...𝑁)))
373	6	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → 𝑇 ∈ 𝑆)
374		poimirlem22.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)
375	374	adantlr 714	. . . . 5 ⊢ (((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)
376		simpr 488	. . . . 5 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → (2^nd ‘𝑇) = 𝑁)
377	371, 3, 372, 373, 375, 376	poimirlem21 35078	. . . 4 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) = 𝑁) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
378	370, 377	jaodan 955	. . 3 ⊢ ((𝜑 ∧ ((2^nd ‘𝑇) = 0 ∨ (2^nd ‘𝑇) = 𝑁)) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
379	363, 378	syldan 594	. 2 ⊢ ((𝜑 ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
380	288, 379	pm2.61dan 812	1 ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 = wceq 1538 ∈ wcel 2111 {cab 2776 ≠ wne 2987 ∀wral 3106 ∃wrex 3107 ∃!wreu 3108 ∃*wrmo 3109 {crab 3110 Vcvv 3441 ⦋csb 3828 ∖ cdif 3878 ∪ cun 3879 ∩ cin 3880 ⊆ wss 3881 ∅c0 4243 ifcif 4425 {csn 4525 {cpr 4527 ⟨cop 4531 class class class wbr 5030 ↦ cmpt 5110 I cid 5424 × cxp 5517 ran crn 5520 ↾ cres 5521 “ cima 5522 ∘ ccom 5523 Fn wfn 6319 ⟶wf 6320 –1-1→wf1 6321 –onto→wfo 6322 –1-1-onto→wf1o 6323 ‘cfv 6324 (class class class)co 7135 ∘_f cof 7387 1^st c1st 7669 2^nd c2nd 7670 ↑_m cmap 8389 ℂcc 10524 ℝcr 10525 0cc0 10526 1c1 10527 + caddc 10529 < clt 10664 ≤ cle 10665 − cmin 10859 ℕcn 11625 ℕ₀cn0 11885 ℤcz 11969 ℤ_≥cuz 12231 ...cfz 12885 ..^cfzo 13028

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-of 7389 df-om 7561 df-1st 7671 df-2nd 7672 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-2o 8086 df-oadd 8089 df-er 8272 df-map 8391 df-pm 8392 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-dju 9314 df-card 9352 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-div 11287 df-nn 11626 df-2 11688 df-3 11689 df-n0 11886 df-xnn0 11956 df-z 11970 df-uz 12232 df-fz 12886 df-fzo 13029 df-seq 13365 df-fac 13630 df-bc 13659 df-hash 13687

This theorem is referenced by: poimirlem27 35084

W3C validator