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 37642

Description: Lemma for poimir 37653, 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 37635	. . 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 6822	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
11	10	breq2d 5104	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
12	11	ifbid 4500	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
13	12	csbeq1d 3855	. . . . . . . . . . . . . . . . . . . . 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 6827	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
15		2fveq3 6827	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
16	15	imaeq1d 6010	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
17	16	xpeq1d 5648	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
18	15	imaeq1d 6010	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
19	18	xpeq1d 5648	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
20	17, 19	uneq12d 4120	. . . . . . . . . . . . . . . . . . . . . . 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 7367	. . . . . . . . . . . . . . . . . . . . . 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 3858	. . . . . . . . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . . . . . . . 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 5186	. . . . . . . . . . . . . . . . . . 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 2740	. . . . . . . . . . . . . . . . . 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 3651	. . . . . . . . . . . . . . . . 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 3643	. . . . . . . . . . . . . . . . . . . . 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 2846	. . . . . . . . . . . . . . . . . . . 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 7956	. . . . . . . . . . . . . . . . . . 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 7956	. . . . . . . . . . . . . . . . . 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 8776	. . . . . . . . . . . . . . . . 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 13562	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ)
40	39	ssriv 3939	. . . . . . . . . . . . . . . 16 ⊢ (0..^𝐾) ⊆ ℤ
41		fss 6668	. . . . . . . . . . . . . . . 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 7957	. . . . . . . . . . . . . . . . 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 6835	. . . . . . . . . . . . . . . . 17 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
47		f1oeq1 6752	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
48	46, 47	elab 3635	. . . . . . . . . . . . . . . 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 37621	. . . . . . . . . . . . 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 6822	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → (2^nd ‘𝑡) = (2^nd ‘𝑧))
55	54	breq2d 5104	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑧)))
56	55	ifbid 4500	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)))
57	56	csbeq1d 3855	. . . . . . . . . . . . . . . . . . . . 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 6827	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑧 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑧)))
59		2fveq3 6827	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑧 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑧)))
60	59	imaeq1d 6010	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑧 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)))
61	60	xpeq1d 5648	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}))
62	59	imaeq1d 6010	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑧 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)))
63	62	xpeq1d 5648	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑧 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))
64	61, 63	uneq12d 4120	. . . . . . . . . . . . . . . . . . . . . . 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 7367	. . . . . . . . . . . . . . . . . . . . . 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 3858	. . . . . . . . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . . . . . . . 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 5186	. . . . . . . . . . . . . . . . . . 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 2740	. . . . . . . . . . . . . . . . . 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 3651	. . . . . . . . . . . . . . . . 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 3643	. . . . . . . . . . . . . . . . . . . . 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 2846	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑_m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
75		xp1st 7956	. . . . . . . . . . . . . . . . . . . 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 7956	. . . . . . . . . . . . . . . . . . 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 8776	. . . . . . . . . . . . . . . . . 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 6668	. . . . . . . . . . . . . . . . 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 7957	. . . . . . . . . . . . . . . . . 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 6835	. . . . . . . . . . . . . . . . . 18 ⊢ (2^nd ‘(1^st ‘𝑧)) ∈ V
87		f1oeq1 6752	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)))
88	86, 87	elab 3635	. . . . . . . . . . . . . . . . 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 775	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ (2^nd ‘𝑧) ≠ (2^nd ‘𝑇)) → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
92		xp2nd 7957	. . . . . . . . . . . . . . . . . 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 4737	. . . . . . . . . . . . . . . . 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 37622	. . . . . . . . . . . . . 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 2943	. . . . . . . . . . . 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 2816	. . . . . . . . . . . . . . . 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 5095	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 0 → (𝑦 < (2^nd ‘𝑧) ↔ 0 < (2^nd ‘𝑧)))
108		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 0 → 𝑦 = 0)
109	107, 108	ifbieq1d 4501	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 0 → if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) = if(0 < (2^nd ‘𝑧), 0, (𝑦 + 1)))
110		elfznn 13456	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑧) ∈ ℕ)
111	110	nngt0d 12177	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) → 0 < (2^nd ‘𝑧))
112	111	iftrued 4484	. . . . . . . . . . . . . . . . . 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 2786	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → if(𝑦 < (2^nd ‘𝑧), 𝑦, (𝑦 + 1)) = 0)
115	114	csbeq1d 3855	. . . . . . . . . . . . . . 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 11109	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ V
117		oveq2 7357	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = 0 → (1...𝑗) = (1...0))
118		fz10 13448	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1...0) = ∅
119	117, 118	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 0 → (1...𝑗) = ∅)
120	119	imaeq2d 6011	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 0 → ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑧)) “ ∅))
121	120	xpeq1d 5648	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}))
122		oveq1 7356	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = 0 → (𝑗 + 1) = (0 + 1))
123		0p1e1 12245	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 + 1) = 1
124	122, 123	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = 0 → (𝑗 + 1) = 1)
125	124	oveq1d 7364	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 0 → ((𝑗 + 1)...𝑁) = (1...𝑁))
126	125	imaeq2d 6011	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 0 → ((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)))
127	126	xpeq1d 5648	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
128	121, 127	uneq12d 4120	. . . . . . . . . . . . . . . . . . . 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 6028	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2^nd ‘(1^st ‘𝑧)) “ ∅) = ∅
130	129	xpeq1i 5645	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) = (∅ × {1})
131		0xp 5718	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∅ × {1}) = ∅
132	130, 131	eqtri 2752	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) = ∅
133	132	uneq1i 4115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = (∅ ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
134		uncom 4109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∅ ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}) ∪ ∅)
135		un0 4345	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}) ∪ ∅) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})
136	133, 134, 135	3eqtri 2756	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((2^nd ‘(1^st ‘𝑧)) “ ∅) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})
137	128, 136	eqtrdi 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 0 → ((((2^nd ‘(1^st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}))
138	137	oveq2d 7365	. . . . . . . . . . . . . . . . . 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 3886	. . . . . . . . . . . . . . . . 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 6771	. . . . . . . . . . . . . . . . . . . . . 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 6741	. . . . . . . . . . . . . . . . . . . . 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 5648	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0}) = ((1...𝑁) × {0}))
145	144	oveq2d 7365	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑆 → ((1^st ‘(1^st ‘𝑧)) ∘_f + (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = ((1^st ‘(1^st ‘𝑧)) ∘_f + ((1...𝑁) × {0})))
146		ovexd 7384	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (1...𝑁) ∈ V)
147	80	ffnd 6653	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘(1^st ‘𝑧)) Fn (1...𝑁))
148		fnconstg 6712	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
149	116, 148	mp1i 13	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑆 → ((1...𝑁) × {0}) Fn (1...𝑁))
150		eqidd 2730	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) = ((1^st ‘(1^st ‘𝑧))‘𝑛))
151	116	fvconst2 7140	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
152	151	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
153	80	ffvelcdmda 7018	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ (0..^𝐾))
154		elfzonn0 13610	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ ℕ₀)
155	153, 154	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ ℕ₀)
156	155	nn0cnd 12447	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑧))‘𝑛) ∈ ℂ)
157	156	addridd 11316	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑧))‘𝑛) + 0) = ((1^st ‘(1^st ‘𝑧))‘𝑛))
158	146, 147, 149, 147, 150, 152, 157	offveq 7639	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝑆 → ((1^st ‘(1^st ‘𝑧)) ∘_f + ((1...𝑁) × {0})) = (1^st ‘(1^st ‘𝑧)))
159	145, 158	eqtrd 2764	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 → ((1^st ‘(1^st ‘𝑧)) ∘_f + (((2^nd ‘(1^st ‘𝑧)) “ (1...𝑁)) × {0})) = (1^st ‘(1^st ‘𝑧)))
160	139, 159	eqtrid 2776	. . . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . 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 12425	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
164	1, 163	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
165		0elfz 13527	. . . . . . . . . . . . . . . 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 6837	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) → (1^st ‘(1^st ‘𝑧)) ∈ V)
169	106, 162, 167, 168	fvmptd 6937	. . . . . . . . . . . . 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 6822	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑇 → (2^nd ‘𝑧) = (2^nd ‘𝑇))
174	173	eleq1d 2813	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑇 → ((2^nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))))
175	174	anbi2d 630	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑇 → ((𝜑 ∧ (2^nd ‘𝑧) ∈ (1...(𝑁 − 1))) ↔ (𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))))
176		2fveq3 6827	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑇 → (1^st ‘(1^st ‘𝑧)) = (1^st ‘(1^st ‘𝑇)))
177	176	eqeq2d 2740	. . . . . . . . . . . . . 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 3532	. . . . . . . . . . . 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 2766	. . . . . . . . 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 775	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
188		simplr 768	. . . . . . . . 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 7965	. . . . . . . . . . . . . 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 7965	. . . . . . . . . . . . . . . 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 2946	. . . . . . . . . 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 37629	. . . . . . . 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 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 13456	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ∈ ℕ)
207	206	nnred 12143	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ∈ ℝ)
208	207	ltp1d 12055	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
209	207, 208	ltned 11252	. . . . . . . . . . . 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 6821	. . . . . . . . . . . . 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 11964	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2^nd ‘𝑇) ∈ ℝ → (2^nd ‘𝑇) < ((2^nd ‘𝑇) + 1))
214	212, 213	ltned 11252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2^nd ‘𝑇) ∈ ℝ → (2^nd ‘𝑇) ≠ ((2^nd ‘𝑇) + 1))
215		fvex 6835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2^nd ‘𝑇) ∈ V
216		ovex 7382	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2^nd ‘𝑇) + 1) ∈ V
217	215, 216, 216, 215	fpr 7088	. . . . . . . . . . . . . . . . . . . . 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 6802	. . . . . . . . . . . . . . . . . . . . 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 6764	. . . . . . . . . . . . . . . . . . . . 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 4423	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})) = ∅
223		fun 6686	. . . . . . . . . . . . . . . . . . . . 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 4714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2^nd ‘𝑇) ∈ {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)}
227		elun1 4133	. . . . . . . . . . . . . . . . . . . 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 6922	. . . . . . . . . . . . . . . . . . 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 6653	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2^nd ‘𝑇) ∈ ℝ → {⟨(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)⟩, ⟨((2^nd ‘𝑇) + 1), (2^nd ‘𝑇)⟩} Fn {(2^nd ‘𝑇), ((2^nd ‘𝑇) + 1)})
232		fnresi 6611	. . . . . . . . . . . . . . . . . . . . . 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 6914	. . . . . . . . . . . . . . . . . . . . . 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 1455	. . . . . . . . . . . . . . . . . . . . 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 7128	. . . . . . . . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . . . . . . 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 6826	. . . . . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . . . . 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 2740	. . . . . . . . . . . . . . 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 6763	. . . . . . . . . . . . . . . . 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 12144	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℂ)
249		npcan1 11545	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
250	248, 249	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
251	164	nn0zd 12497	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
252		uzid 12750	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
253	251, 252	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
254		peano2uz 12802	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
255	253, 254	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
256	250, 255	eqeltrrd 2829	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
257		fzss2 13467	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
258	256, 257	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
259	258	sselda 3935	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (2^nd ‘𝑇) ∈ (1...𝑁))
260		fzp1elp1 13480	. . . . . . . . . . . . . . . . 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 7365	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
263	262	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (1...((𝑁 − 1) + 1)) = (1...𝑁))
264	261, 263	eleqtrd 2830	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))) → ((2^nd ‘𝑇) + 1) ∈ (1...𝑁))
265		f1veqaeq 7193	. . . . . . . . . . . . . . 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 836	. . . . . . . . . . . . . 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 2946	. . . . . . . . . . 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 6827	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑇 → (2^nd ‘(1^st ‘𝑧)) = (2^nd ‘(1^st ‘𝑇)))
272	271	neeq1d 2984	. . . . . . . . . 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 2948	. . . . . . . 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 7966	. . . . . . . 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 7966	. . . . . . . . . 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 3121	. . 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 3688	. . 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 7957	. . . . . . 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 12445	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
293		nn0uz 12777	. . . . . . . . . . . 12 ⊢ ℕ₀ = (ℤ_≥‘0)
294	292, 293	eleqtrdi 2838	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
295		fzpred 13475	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘0) → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
296	294, 295	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁)))
297	123	oveq1i 7359	. . . . . . . . . . 11 ⊢ ((0 + 1)...𝑁) = (1...𝑁)
298	297	uneq2i 4116	. . . . . . . . . 10 ⊢ ({0} ∪ ((0 + 1)...𝑁)) = ({0} ∪ (1...𝑁))
299	296, 298	eqtrdi 2780	. . . . . . . . 9 ⊢ (𝜑 → (0...𝑁) = ({0} ∪ (1...𝑁)))
300	299	difeq1d 4076	. . . . . . . 8 ⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))))
301		difundir 4242	. . . . . . . . . 10 ⊢ (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = (({0} ∖ (1...(𝑁 − 1))) ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
302		0lt1 11642	. . . . . . . . . . . . . 14 ⊢ 0 < 1
303		0re 11117	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
304		1re 11115	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
305	303, 304	ltnlei 11237	. . . . . . . . . . . . . 14 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
306	302, 305	mpbi 230	. . . . . . . . . . . . 13 ⊢ ¬ 1 ≤ 0
307		elfzle1 13430	. . . . . . . . . . . . 13 ⊢ (0 ∈ (1...(𝑁 − 1)) → 1 ≤ 0)
308	306, 307	mto 197	. . . . . . . . . . . 12 ⊢ ¬ 0 ∈ (1...(𝑁 − 1))
309		incom 4160	. . . . . . . . . . . . . 14 ⊢ ((1...(𝑁 − 1)) ∩ {0}) = ({0} ∩ (1...(𝑁 − 1)))
310	309	eqeq1i 2734	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {0}) = ∅ ↔ ({0} ∩ (1...(𝑁 − 1))) = ∅)
311		disjsn 4663	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (1...(𝑁 − 1)))
312		disj3 4405	. . . . . . . . . . . . 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 4115	. . . . . . . . . 10 ⊢ ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1)))) = (({0} ∖ (1...(𝑁 − 1))) ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
316	301, 315	eqtr4i 2755	. . . . . . . . 9 ⊢ (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1))))
317		difundir 4242	. . . . . . . . . . . 12 ⊢ (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))) = (((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) ∪ ({𝑁} ∖ (1...(𝑁 − 1))))
318		difid 4327	. . . . . . . . . . . . 13 ⊢ ((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) = ∅
319	318	uneq1i 4115	. . . . . . . . . . . 12 ⊢ (((1...(𝑁 − 1)) ∖ (1...(𝑁 − 1))) ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1))))
320		uncom 4109	. . . . . . . . . . . . 13 ⊢ (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = (({𝑁} ∖ (1...(𝑁 − 1))) ∪ ∅)
321		un0 4345	. . . . . . . . . . . . 13 ⊢ (({𝑁} ∖ (1...(𝑁 − 1))) ∪ ∅) = ({𝑁} ∖ (1...(𝑁 − 1)))
322	320, 321	eqtri 2752	. . . . . . . . . . . 12 ⊢ (∅ ∪ ({𝑁} ∖ (1...(𝑁 − 1)))) = ({𝑁} ∖ (1...(𝑁 − 1)))
323	317, 319, 322	3eqtri 2756	. . . . . . . . . . 11 ⊢ (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))) = ({𝑁} ∖ (1...(𝑁 − 1)))
324		nnuz 12778	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
325	1, 324	eleqtrdi 2838	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
326	250, 325	eqeltrd 2828	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘1))
327		fzsplit2 13452	. . . . . . . . . . . . . 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 7364	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
330	1	nnzd 12498	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℤ)
331		fzsn 13469	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
332	330, 331	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁...𝑁) = {𝑁})
333	329, 332	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
334	333	uneq2d 4119	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁}))
335	328, 334	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁}))
336	335	difeq1d 4076	. . . . . . . . . . 11 ⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1))))
337	1	nnred 12143	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℝ)
338	337	ltm1d 12057	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
339	164	nn0red 12446	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
340	339, 337	ltnled 11263	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
341	338, 340	mpbid 232	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
342		elfzle2 13431	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
343	341, 342	nsyl 140	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
344		incom 4160	. . . . . . . . . . . . . 14 ⊢ ((1...(𝑁 − 1)) ∩ {𝑁}) = ({𝑁} ∩ (1...(𝑁 − 1)))
345	344	eqeq1i 2734	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ({𝑁} ∩ (1...(𝑁 − 1))) = ∅)
346		disjsn 4663	. . . . . . . . . . . . 13 ⊢ (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1)))
347		disj3 4405	. . . . . . . . . . . . 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 2790	. . . . . . . . . 10 ⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = {𝑁})
351	350	uneq2d 4119	. . . . . . . . 9 ⊢ (𝜑 → ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1)))) = ({0} ∪ {𝑁}))
352	316, 351	eqtrid 2776	. . . . . . . 8 ⊢ (𝜑 → (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = ({0} ∪ {𝑁}))
353	300, 352	eqtrd 2764	. . . . . . 7 ⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = ({0} ∪ {𝑁}))
354	353	eleq2d 2814	. . . . . 6 ⊢ (𝜑 → ((2^nd ‘𝑇) ∈ ((0...𝑁) ∖ (1...(𝑁 − 1))) ↔ (2^nd ‘𝑇) ∈ ({0} ∪ {𝑁})))
355		eldif 3913	. . . . . 6 ⊢ ((2^nd ‘𝑇) ∈ ((0...𝑁) ∖ (1...(𝑁 − 1))) ↔ ((2^nd ‘𝑇) ∈ (0...𝑁) ∧ ¬ (2^nd ‘𝑇) ∈ (1...(𝑁 − 1))))
356		elun 4104	. . . . . . 7 ⊢ ((2^nd ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2^nd ‘𝑇) ∈ {0} ∨ (2^nd ‘𝑇) ∈ {𝑁}))
357	215	elsn 4592	. . . . . . . 8 ⊢ ((2^nd ‘𝑇) ∈ {0} ↔ (2^nd ‘𝑇) = 0)
358	215	elsn 4592	. . . . . . . 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 37638	. . . 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 37641	. . . 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 812	1 ⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2109 {cab 2707 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 ∃!wreu 3341 ∃*wrmo 3342 {crab 3394 Vcvv 3436 ⦋csb 3851 ∖ cdif 3900 ∪ cun 3901 ∩ cin 3902 ⊆ wss 3903 ∅c0 4284 ifcif 4476 {csn 4577 {cpr 4579 ⟨cop 4583 class class class wbr 5092 ↦ cmpt 5173 I cid 5513 × cxp 5617 ran crn 5620 ↾ cres 5621 “ cima 5622 ∘ ccom 5623 Fn wfn 6477 ⟶wf 6478 –1-1→wf1 6479 –onto→wfo 6480 –1-1-onto→wf1o 6481 ‘cfv 6482 (class class class)co 7349 ∘_f cof 7611 1^st c1st 7922 2^nd c2nd 7923 ↑_m cmap 8753 ℂcc 11007 ℝcr 11008 0cc0 11009 1c1 11010 + caddc 11012 < clt 11149 ≤ cle 11150 − cmin 11347 ℕcn 12128 ℕ₀cn0 12384 ℤcz 12471 ℤ_≥cuz 12735 ...cfz 13410 ..^cfzo 13557

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-of 7613 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-oadd 8392 df-er 8625 df-map 8755 df-pm 8756 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-dju 9797 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-n0 12385 df-xnn0 12458 df-z 12472 df-uz 12736 df-fz 13411 df-fzo 13558 df-seq 13909 df-fac 14181 df-bc 14210 df-hash 14238

This theorem is referenced by: poimirlem27 37647

W3C validator