poimirlem20 - Mathbox for Brendan Leahy

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

Theorem poimirlem20 32599

Description: Lemma for poimir 32612 establishing existence for poimirlem21 32600. (Contributed by Brendan Leahy, 21-Aug-2020.)

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

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

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

**Proof of Theorem poimirlem20**
Step	Hyp	Ref	Expression
1		oveq2 6557	. . . . . . . . 9 ⊢ (1 = if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0) → (((1^st ‘(1^st ‘𝑇))‘𝑛) − 1) = (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0)))
2	1	eleq1d 2672	. . . . . . . 8 ⊢ (1 = if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0) → ((((1^st ‘(1^st ‘𝑇))‘𝑛) − 1) ∈ (0..^𝐾) ↔ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0)) ∈ (0..^𝐾)))
3		oveq2 6557	. . . . . . . . 9 ⊢ (0 = if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0) → (((1^st ‘(1^st ‘𝑇))‘𝑛) − 0) = (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0)))
4	3	eleq1d 2672	. . . . . . . 8 ⊢ (0 = if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0) → ((((1^st ‘(1^st ‘𝑇))‘𝑛) − 0) ∈ (0..^𝐾) ↔ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0)) ∈ (0..^𝐾)))
5		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁) → ((1^st ‘(1^st ‘𝑇))‘𝑛) = ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)))
6	5	oveq1d 6564	. . . . . . . . . . 11 ⊢ (𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁) → (((1^st ‘(1^st ‘𝑇))‘𝑛) − 1) = (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) − 1))
7	6	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁)) → (((1^st ‘(1^st ‘𝑇))‘𝑛) − 1) = (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) − 1))
8		poimirlem22.2	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑇 ∈ 𝑆)
9		elrabi 3328	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
10		poimirlem22.s	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
11	9, 10	eleq2s 2706	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
12	8, 11	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
13		xp1st 7089	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
14	12, 13	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
15		xp1st 7089	. . . . . . . . . . . . . . . . . 18 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)))
16	14, 15	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)))
17		elmapi 7765	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
18	16, 17	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
19		xp2nd 7090	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
20	14, 19	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
21		fvex 6113	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
22		f1oeq1 6040	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
23	21, 22	elab 3319	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
24	20, 23	sylib 207	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
25		f1of 6050	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)⟶(1...𝑁))
26	24, 25	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)⟶(1...𝑁))
27		poimir.0	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℕ)
28		elfz1end 12242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
29	27, 28	sylib 207	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
30	26, 29	ffvelrnd 6268	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇))‘𝑁) ∈ (1...𝑁))
31	18, 30	ffvelrnd 6268	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ∈ (0..^𝐾))
32		elfzonn0 12380	. . . . . . . . . . . . . . 15 ⊢ (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ∈ ℕ₀)
33	31, 32	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ∈ ℕ₀)
34		fvex 6113	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘(1^st ‘𝑇))‘𝑁) ∈ V
35		eleq1 2676	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁) → (𝑛 ∈ (1...𝑁) ↔ ((2^nd ‘(1^st ‘𝑇))‘𝑁) ∈ (1...𝑁)))
36	35	anbi2d 736	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁) → ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ↔ (𝜑 ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑁) ∈ (1...𝑁))))
37		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁) → (𝑝‘𝑛) = (𝑝‘((2^nd ‘(1^st ‘𝑇))‘𝑁)))
38	37	neeq1d 2841	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁) → ((𝑝‘𝑛) ≠ 0 ↔ (𝑝‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ≠ 0))
39	38	rexbidv 3034	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁) → (∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0 ↔ ∃𝑝 ∈ ran 𝐹(𝑝‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ≠ 0))
40	36, 39	imbi12d 333	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁) → (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0) ↔ ((𝜑 ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑁) ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ≠ 0)))
41		poimirlem22.3	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0)
42	34, 40, 41	vtocl 3232	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑁) ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ≠ 0)
43	30, 42	mpdan 699	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∃𝑝 ∈ ran 𝐹(𝑝‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ≠ 0)
44		fveq1 6102	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))) → (𝑝‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) = (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)))
45		ffn 5958	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾) → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
46	18, 45	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
47	46	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
48		1ex 9914	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 1 ∈ V
49		fnconstg 6006	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (1 ∈ V → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)))
50	48, 49	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦))
51		c0ex 9913	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 0 ∈ V
52		fnconstg 6006	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (0 ∈ V → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))
53	51, 52	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁))
54	50, 53	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) ∧ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))
55		dff1o3 6056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡(2^nd ‘(1^st ‘𝑇))))
56	55	simprbi 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡(2^nd ‘(1^st ‘𝑇)))
57	24, 56	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → Fun ^◡(2^nd ‘(1^st ‘𝑇)))
58		imain 5888	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (Fun ^◡(2^nd ‘(1^st ‘𝑇)) → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁))))
59	57, 58	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁))))
60		elfznn0 12302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ₀)
61	60	nn0red 11229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
62	61	ltp1d 10833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 < (𝑦 + 1))
63		fzdisj 12239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 < (𝑦 + 1) → ((1...𝑦) ∩ ((𝑦 + 1)...𝑁)) = ∅)
64	62, 63	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((1...𝑦) ∩ ((𝑦 + 1)...𝑁)) = ∅)
65	64	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑇)) “ ∅))
66		ima0 5400	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ∅) = ∅
67	65, 66	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = ∅)
68	59, 67	sylan9req 2665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) = ∅)
69		fnun 5911	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) ∧ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) ∧ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) = ∅) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁))))
70	54, 68, 69	sylancr 694	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁))))
71		imaundi 5464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))
72		nn0p1nn 11209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 ∈ ℕ₀ → (𝑦 + 1) ∈ ℕ)
73		nnuz 11599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ℕ = (ℤ_≥‘1)
74	72, 73	syl6eleq 2698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 ∈ ℕ₀ → (𝑦 + 1) ∈ (ℤ_≥‘1))
75	60, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (ℤ_≥‘1))
76	75	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ (ℤ_≥‘1))
77	27	nncnd 10913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 𝑁 ∈ ℂ)
78		npcan1 10334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
79	77, 78	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
80	79	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
81		elfzuz3 12210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑦))
82		peano2uz 11617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑦))
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑦))
84	83	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘𝑦))
85	80, 84	eqeltrrd 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ_≥‘𝑦))
86		fzsplit2 12237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑦 + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘𝑦)) → (1...𝑁) = ((1...𝑦) ∪ ((𝑦 + 1)...𝑁)))
87	76, 85, 86	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) = ((1...𝑦) ∪ ((𝑦 + 1)...𝑁)))
88	87	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))))
89		f1ofo 6057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁))
90		foima 6033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (1...𝑁))
91	24, 89, 90	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (1...𝑁))
92	91	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (1...𝑁))
93	88, 92	eqtr3d 2646	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))) = (1...𝑁))
94	71, 93	syl5eqr 2658	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) = (1...𝑁))
95	94	fneq2d 5896	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) ↔ ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (1...𝑁)))
96	70, 95	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (1...𝑁))
97		ovex 6577	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1...𝑁) ∈ V
98	97	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) ∈ V)
99		inidm 3784	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
100		eqidd 2611	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑁) ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) = ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)))
101		f1ofn 6051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁))
102	24, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁))
103	102	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁))
104		fzss1 12251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑦 + 1) ∈ (ℤ_≥‘1) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
105	75, 104	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
106	105	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
107		eluzp1p1 11589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑦 + 1)))
108		uzss 11584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑦 + 1)) → (ℤ_≥‘((𝑁 − 1) + 1)) ⊆ (ℤ_≥‘(𝑦 + 1)))
109	81, 107, 108	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (ℤ_≥‘((𝑁 − 1) + 1)) ⊆ (ℤ_≥‘(𝑦 + 1)))
110	109	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (ℤ_≥‘((𝑁 − 1) + 1)) ⊆ (ℤ_≥‘(𝑦 + 1)))
111	27	nnzd 11357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 𝑁 ∈ ℤ)
112		uzid 11578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ_≥‘𝑁))
113	111, 112	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑁))
114	79	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (ℤ_≥‘((𝑁 − 1) + 1)) = (ℤ_≥‘𝑁))
115	113, 114	eleqtrrd 2691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘((𝑁 − 1) + 1)))
116	115	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ_≥‘((𝑁 − 1) + 1)))
117	110, 116	sseldd 3569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ_≥‘(𝑦 + 1)))
118		eluzfz2 12220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑦 + 1)) → 𝑁 ∈ ((𝑦 + 1)...𝑁))
119	117, 118	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑦 + 1)...𝑁))
120		fnfvima 6400	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁) ∧ ((𝑦 + 1)...𝑁) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑦 + 1)...𝑁)) → ((2^nd ‘(1^st ‘𝑇))‘𝑁) ∈ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))
121	103, 106, 119, 120	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2^nd ‘(1^st ‘𝑇))‘𝑁) ∈ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))
122		fvun2 6180	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) ∧ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) ∧ ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) = ∅ ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑁) ∈ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) = ((((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})‘((2^nd ‘(1^st ‘𝑇))‘𝑁)))
123	50, 53, 122	mp3an12 1406	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) = ∅ ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑁) ∈ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) = ((((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})‘((2^nd ‘(1^st ‘𝑇))‘𝑁)))
124	68, 121, 123	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) = ((((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})‘((2^nd ‘(1^st ‘𝑇))‘𝑁)))
125	51	fvconst2 6374	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((2^nd ‘(1^st ‘𝑇))‘𝑁) ∈ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) → ((((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) = 0)
126	121, 125	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) = 0)
127	124, 126	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) = 0)
128	127	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑁) ∈ (1...𝑁)) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) = 0)
129	47, 96, 98, 98, 99, 100, 128	ofval 6804	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑁) ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) = (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) + 0))
130	30, 129	mpidan 701	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) = (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) + 0))
131	33	nn0cnd 11230	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ∈ ℂ)
132	131	addid1d 10115	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) + 0) = ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)))
133	132	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) + 0) = ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)))
134	130, 133	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) = ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)))
135	44, 134	sylan9eqr 2666	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑝 = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) → (𝑝‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) = ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)))
136	135	adantllr 751	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑝 ∈ ran 𝐹) ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑝 = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) → (𝑝‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) = ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)))
137		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
138	137	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
139	138	ifbid 4058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
140	139	csbeq1d 3506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
141		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑡 = 𝑇 → (1^st ‘𝑡) = (1^st ‘𝑇))
142	141	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
143	141	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
144	143	imaeq1d 5384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
145	144	xpeq1d 5062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
146	143	imaeq1d 5384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
147	146	xpeq1d 5062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
148	145, 147	uneq12d 3730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 = 𝑇 → ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
149	142, 148	oveq12d 6567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑡 = 𝑇 → ((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
150	149	csbeq2dv 3944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
151	140, 150	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
152	151	mpteq2dv 4673	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
153	152	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
154	153, 10	elrab2 3333	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
155	154	simprbi 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
156	8, 155	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
157	61	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ)
158		peano2zm 11297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
159	111, 158	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
160	159	zred 11358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
161	160	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
162	27	nnred 10912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → 𝑁 ∈ ℝ)
163	162	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℝ)
164		elfzle2 12216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑁 − 1))
165	164	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ≤ (𝑁 − 1))
166	162	ltm1d 10835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
167	166	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
168	157, 161, 163, 165, 167	lelttrd 10074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁)
169		poimirlem21.4	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (2^nd ‘𝑇) = 𝑁)
170	169	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2^nd ‘𝑇) = 𝑁)
171	168, 170	breqtrrd 4611	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < (2^nd ‘𝑇))
172	171	iftrued 4044	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑦)
173	172	csbeq1d 3506	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
174		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑦 ∈ V
175		oveq2 6557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 = 𝑦 → (1...𝑗) = (1...𝑦))
176	175	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 = 𝑦 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)))
177	176	xpeq1d 5062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 = 𝑦 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}))
178		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 = 𝑦 → (𝑗 + 1) = (𝑦 + 1))
179	178	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 = 𝑦 → ((𝑗 + 1)...𝑁) = ((𝑦 + 1)...𝑁))
180	179	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 = 𝑦 → ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)))
181	180	xpeq1d 5062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 = 𝑦 → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))
182	177, 181	uneq12d 3730	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 = 𝑦 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))
183	182	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 = 𝑦 → ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
184	174, 183	csbie 3525	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ⦋𝑦 / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))
185	173, 184	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
186	185	mpteq2dva 4672	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))))
187	156, 186	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))))
188	187	rneqd 5274	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ran 𝐹 = ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))))
189	188	eleq2d 2673	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑝 ∈ ran 𝐹 ↔ 𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))))
190		eqid 2610	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
191		ovex 6577	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))) ∈ V
192	190, 191	elrnmpti 5297	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
193	189, 192	syl6bb 275	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑝 ∈ ran 𝐹 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))))
194	193	biimpa 500	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
195	136, 194	r19.29a 3060	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → (𝑝‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) = ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)))
196	195	neeq1d 2841	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → ((𝑝‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ≠ 0 ↔ ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ≠ 0))
197	196	biimpd 218	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → ((𝑝‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ≠ 0 → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ≠ 0))
198	197	rexlimdva 3013	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∃𝑝 ∈ ran 𝐹(𝑝‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ≠ 0 → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ≠ 0))
199	43, 198	mpd 15	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ≠ 0)
200		elnnne0 11183	. . . . . . . . . . . . . 14 ⊢ (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ∈ ℕ ↔ (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ∈ ℕ₀ ∧ ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ≠ 0))
201	33, 199, 200	sylanbrc 695	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ∈ ℕ)
202		nnm1nn0 11211	. . . . . . . . . . . . 13 ⊢ (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ∈ ℕ → (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) − 1) ∈ ℕ₀)
203	201, 202	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) − 1) ∈ ℕ₀)
204		elfzo0 12376	. . . . . . . . . . . . . 14 ⊢ (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ∈ (0..^𝐾) ↔ (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ∈ ℕ₀ ∧ 𝐾 ∈ ℕ ∧ ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) < 𝐾))
205	31, 204	sylib 207	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ∈ ℕ₀ ∧ 𝐾 ∈ ℕ ∧ ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) < 𝐾))
206	205	simp2d 1067	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ ℕ)
207	203	nn0red 11229	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) − 1) ∈ ℝ)
208	33	nn0red 11229	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ∈ ℝ)
209	206	nnred 10912	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ ℝ)
210	208	ltm1d 10835	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) − 1) < ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)))
211		elfzolt2 12348	. . . . . . . . . . . . . 14 ⊢ (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) < 𝐾)
212	31, 211	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) < 𝐾)
213	207, 208, 209, 210, 212	lttrd 10077	. . . . . . . . . . . 12 ⊢ (𝜑 → (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) − 1) < 𝐾)
214		elfzo0 12376	. . . . . . . . . . . 12 ⊢ ((((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) − 1) ∈ (0..^𝐾) ↔ ((((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) − 1) ∈ ℕ₀ ∧ 𝐾 ∈ ℕ ∧ (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) − 1) < 𝐾))
215	203, 206, 213, 214	syl3anbrc 1239	. . . . . . . . . . 11 ⊢ (𝜑 → (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) − 1) ∈ (0..^𝐾))
216	215	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁)) → (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑁)) − 1) ∈ (0..^𝐾))
217	7, 216	eqeltrd 2688	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁)) → (((1^st ‘(1^st ‘𝑇))‘𝑛) − 1) ∈ (0..^𝐾))
218	217	adantlr 747	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁)) → (((1^st ‘(1^st ‘𝑇))‘𝑛) − 1) ∈ (0..^𝐾))
219	18	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑛) ∈ (0..^𝐾))
220		elfzonn0 12380	. . . . . . . . . . . . 13 ⊢ (((1^st ‘(1^st ‘𝑇))‘𝑛) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑇))‘𝑛) ∈ ℕ₀)
221	219, 220	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑛) ∈ ℕ₀)
222	221	nn0cnd 11230	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑛) ∈ ℂ)
223	222	subid1d 10260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑇))‘𝑛) − 0) = ((1^st ‘(1^st ‘𝑇))‘𝑛))
224	223, 219	eqeltrd 2688	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑇))‘𝑛) − 0) ∈ (0..^𝐾))
225	224	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁)) → (((1^st ‘(1^st ‘𝑇))‘𝑛) − 0) ∈ (0..^𝐾))
226	2, 4, 218, 225	ifbothda 4073	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0)) ∈ (0..^𝐾))
227		eqid 2610	. . . . . . 7 ⊢ (𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) = (𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0)))
228	226, 227	fmptd 6292	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))):(1...𝑁)⟶(0..^𝐾))
229		ovex 6577	. . . . . . 7 ⊢ (0..^𝐾) ∈ V
230	229, 97	elmap 7772	. . . . . 6 ⊢ ((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))):(1...𝑁)⟶(0..^𝐾))
231	228, 230	sylibr 223	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)))
232		simpr 476	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ((1 + 1)...𝑁)) → 𝑛 ∈ ((1 + 1)...𝑁))
233		1z 11284	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℤ
234		peano2z 11295	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℤ → (1 + 1) ∈ ℤ)
235	233, 234	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (1 + 1) ∈ ℤ
236	111, 235	jctil 558	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ))
237		elfzelz 12213	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ((1 + 1)...𝑁) → 𝑛 ∈ ℤ)
238	237, 233	jctir 559	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ((1 + 1)...𝑁) → (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
239		fzsubel 12248	. . . . . . . . . . . . . 14 ⊢ ((((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ ((1 + 1)...𝑁) ↔ (𝑛 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
240	236, 238, 239	syl2an 493	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ((1 + 1)...𝑁)) → (𝑛 ∈ ((1 + 1)...𝑁) ↔ (𝑛 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
241	232, 240	mpbid 221	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ((1 + 1)...𝑁)) → (𝑛 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1)))
242		ax-1cn 9873	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
243	242, 242	pncan3oi 10176	. . . . . . . . . . . . 13 ⊢ ((1 + 1) − 1) = 1
244	243	oveq1i 6559	. . . . . . . . . . . 12 ⊢ (((1 + 1) − 1)...(𝑁 − 1)) = (1...(𝑁 − 1))
245	241, 244	syl6eleq 2698	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ((1 + 1)...𝑁)) → (𝑛 − 1) ∈ (1...(𝑁 − 1)))
246	245	ralrimiva 2949	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑛 ∈ ((1 + 1)...𝑁)(𝑛 − 1) ∈ (1...(𝑁 − 1)))
247		simpr 476	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) → 𝑦 ∈ (1...(𝑁 − 1)))
248	159, 233	jctil 558	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ))
249		elfzelz 12213	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (1...(𝑁 − 1)) → 𝑦 ∈ ℤ)
250	249, 233	jctir 559	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (1...(𝑁 − 1)) → (𝑦 ∈ ℤ ∧ 1 ∈ ℤ))
251		fzaddel 12246	. . . . . . . . . . . . . . 15 ⊢ (((1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) ∧ (𝑦 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑦 ∈ (1...(𝑁 − 1)) ↔ (𝑦 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1))))
252	248, 250, 251	syl2an 493	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) → (𝑦 ∈ (1...(𝑁 − 1)) ↔ (𝑦 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1))))
253	247, 252	mpbid 221	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) → (𝑦 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1)))
254	79	oveq2d 6565	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 + 1)...𝑁))
255	254	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 + 1)...𝑁))
256	253, 255	eleqtrd 2690	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) → (𝑦 + 1) ∈ ((1 + 1)...𝑁))
257	237	zcnd 11359	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ((1 + 1)...𝑁) → 𝑛 ∈ ℂ)
258	249	zcnd 11359	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (1...(𝑁 − 1)) → 𝑦 ∈ ℂ)
259		subadd2 10164	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑛 − 1) = 𝑦 ↔ (𝑦 + 1) = 𝑛))
260	242, 259	mp3an2 1404	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑛 − 1) = 𝑦 ↔ (𝑦 + 1) = 𝑛))
261		eqcom 2617	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑛 − 1) ↔ (𝑛 − 1) = 𝑦)
262		eqcom 2617	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑦 + 1) ↔ (𝑦 + 1) = 𝑛)
263	260, 261, 262	3bitr4g 302	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑦 = (𝑛 − 1) ↔ 𝑛 = (𝑦 + 1)))
264	257, 258, 263	syl2anr 494	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (1...(𝑁 − 1)) ∧ 𝑛 ∈ ((1 + 1)...𝑁)) → (𝑦 = (𝑛 − 1) ↔ 𝑛 = (𝑦 + 1)))
265	264	ralrimiva 2949	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (1...(𝑁 − 1)) → ∀𝑛 ∈ ((1 + 1)...𝑁)(𝑦 = (𝑛 − 1) ↔ 𝑛 = (𝑦 + 1)))
266	265	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) → ∀𝑛 ∈ ((1 + 1)...𝑁)(𝑦 = (𝑛 − 1) ↔ 𝑛 = (𝑦 + 1)))
267		reu6i 3364	. . . . . . . . . . . 12 ⊢ (((𝑦 + 1) ∈ ((1 + 1)...𝑁) ∧ ∀𝑛 ∈ ((1 + 1)...𝑁)(𝑦 = (𝑛 − 1) ↔ 𝑛 = (𝑦 + 1))) → ∃!𝑛 ∈ ((1 + 1)...𝑁)𝑦 = (𝑛 − 1))
268	256, 266, 267	syl2anc 691	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...(𝑁 − 1))) → ∃!𝑛 ∈ ((1 + 1)...𝑁)𝑦 = (𝑛 − 1))
269	268	ralrimiva 2949	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑦 ∈ (1...(𝑁 − 1))∃!𝑛 ∈ ((1 + 1)...𝑁)𝑦 = (𝑛 − 1))
270		eqid 2610	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) = (𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1))
271	270	f1ompt 6290	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)):((1 + 1)...𝑁)–1-1-onto→(1...(𝑁 − 1)) ↔ (∀𝑛 ∈ ((1 + 1)...𝑁)(𝑛 − 1) ∈ (1...(𝑁 − 1)) ∧ ∀𝑦 ∈ (1...(𝑁 − 1))∃!𝑛 ∈ ((1 + 1)...𝑁)𝑦 = (𝑛 − 1)))
272	246, 269, 271	sylanbrc 695	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)):((1 + 1)...𝑁)–1-1-onto→(1...(𝑁 − 1)))
273		f1osng 6089	. . . . . . . . . 10 ⊢ ((1 ∈ V ∧ 𝑁 ∈ ℕ) → {⟨1, 𝑁⟩}:{1}–1-1-onto→{𝑁})
274	48, 27, 273	sylancr 694	. . . . . . . . 9 ⊢ (𝜑 → {⟨1, 𝑁⟩}:{1}–1-1-onto→{𝑁})
275	160, 162	ltnled 10063	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
276	166, 275	mpbid 221	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
277		elfzle2 12216	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
278	276, 277	nsyl 134	. . . . . . . . . 10 ⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
279		disjsn 4192	. . . . . . . . . 10 ⊢ (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1)))
280	278, 279	sylibr 223	. . . . . . . . 9 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅)
281		1re 9918	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ
282	281	ltp1i 10806	. . . . . . . . . . . . 13 ⊢ 1 < (1 + 1)
283	235	zrei 11260	. . . . . . . . . . . . . 14 ⊢ (1 + 1) ∈ ℝ
284	281, 283	ltnlei 10037	. . . . . . . . . . . . 13 ⊢ (1 < (1 + 1) ↔ ¬ (1 + 1) ≤ 1)
285	282, 284	mpbi 219	. . . . . . . . . . . 12 ⊢ ¬ (1 + 1) ≤ 1
286		elfzle1 12215	. . . . . . . . . . . 12 ⊢ (1 ∈ ((1 + 1)...𝑁) → (1 + 1) ≤ 1)
287	285, 286	mto 187	. . . . . . . . . . 11 ⊢ ¬ 1 ∈ ((1 + 1)...𝑁)
288		disjsn 4192	. . . . . . . . . . 11 ⊢ ((((1 + 1)...𝑁) ∩ {1}) = ∅ ↔ ¬ 1 ∈ ((1 + 1)...𝑁))
289	287, 288	mpbir 220	. . . . . . . . . 10 ⊢ (((1 + 1)...𝑁) ∩ {1}) = ∅
290		f1oun 6069	. . . . . . . . . 10 ⊢ ((((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)):((1 + 1)...𝑁)–1-1-onto→(1...(𝑁 − 1)) ∧ {⟨1, 𝑁⟩}:{1}–1-1-onto→{𝑁}) ∧ ((((1 + 1)...𝑁) ∩ {1}) = ∅ ∧ ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅)) → ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {⟨1, 𝑁⟩}):(((1 + 1)...𝑁) ∪ {1})–1-1-onto→((1...(𝑁 − 1)) ∪ {𝑁}))
291	289, 290	mpanr1 715	. . . . . . . . 9 ⊢ ((((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)):((1 + 1)...𝑁)–1-1-onto→(1...(𝑁 − 1)) ∧ {⟨1, 𝑁⟩}:{1}–1-1-onto→{𝑁}) ∧ ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅) → ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {⟨1, 𝑁⟩}):(((1 + 1)...𝑁) ∪ {1})–1-1-onto→((1...(𝑁 − 1)) ∪ {𝑁}))
292	272, 274, 280, 291	syl21anc 1317	. . . . . . . 8 ⊢ (𝜑 → ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {⟨1, 𝑁⟩}):(((1 + 1)...𝑁) ∪ {1})–1-1-onto→((1...(𝑁 − 1)) ∪ {𝑁}))
293		eleq1 2676	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → (𝑛 ∈ ((1 + 1)...𝑁) ↔ 1 ∈ ((1 + 1)...𝑁)))
294	287, 293	mtbiri 316	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → ¬ 𝑛 ∈ ((1 + 1)...𝑁))
295	294	necon2ai 2811	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ((1 + 1)...𝑁) → 𝑛 ≠ 1)
296		ifnefalse 4048	. . . . . . . . . . . . 13 ⊢ (𝑛 ≠ 1 → if(𝑛 = 1, 𝑁, (𝑛 − 1)) = (𝑛 − 1))
297	295, 296	syl 17	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ((1 + 1)...𝑁) → if(𝑛 = 1, 𝑁, (𝑛 − 1)) = (𝑛 − 1))
298	297	mpteq2ia 4668	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ((1 + 1)...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) = (𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1))
299	298	uneq1i 3725	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ((1 + 1)...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ∪ {⟨1, 𝑁⟩}) = ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {⟨1, 𝑁⟩})
300	48	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ V)
301		ssv 3588	. . . . . . . . . . . 12 ⊢ ℕ ⊆ V
302	301, 27	sseldi 3566	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ V)
303	27, 73	syl6eleq 2698	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
304		fzpred 12259	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘1) → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁)))
305	303, 304	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁)))
306		uncom 3719	. . . . . . . . . . . 12 ⊢ ({1} ∪ ((1 + 1)...𝑁)) = (((1 + 1)...𝑁) ∪ {1})
307	305, 306	syl6req 2661	. . . . . . . . . . 11 ⊢ (𝜑 → (((1 + 1)...𝑁) ∪ {1}) = (1...𝑁))
308		iftrue 4042	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → if(𝑛 = 1, 𝑁, (𝑛 − 1)) = 𝑁)
309	308	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 = 1) → if(𝑛 = 1, 𝑁, (𝑛 − 1)) = 𝑁)
310	300, 302, 307, 309	fmptapd 6342	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑛 ∈ ((1 + 1)...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ∪ {⟨1, 𝑁⟩}) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))
311	299, 310	syl5eqr 2658	. . . . . . . . 9 ⊢ (𝜑 → ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {⟨1, 𝑁⟩}) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))
312	79, 303	eqeltrd 2688	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘1))
313		uzid 11578	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
314		peano2uz 11617	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
315	159, 313, 314	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
316	79, 315	eqeltrrd 2689	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
317		fzsplit2 12237	. . . . . . . . . . 11 ⊢ ((((𝑁 − 1) + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
318	312, 316, 317	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
319	79	oveq1d 6564	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
320		fzsn 12254	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
321	111, 320	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁...𝑁) = {𝑁})
322	319, 321	eqtrd 2644	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
323	322	uneq2d 3729	. . . . . . . . . 10 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁}))
324	318, 323	eqtr2d 2645	. . . . . . . . 9 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁))
325	311, 307, 324	f1oeq123d 6046	. . . . . . . 8 ⊢ (𝜑 → (((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {⟨1, 𝑁⟩}):(((1 + 1)...𝑁) ∪ {1})–1-1-onto→((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))):(1...𝑁)–1-1-onto→(1...𝑁)))
326	292, 325	mpbid 221	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))):(1...𝑁)–1-1-onto→(1...𝑁))
327		f1oco 6072	. . . . . . 7 ⊢ (((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ∧ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))):(1...𝑁)–1-1-onto→(1...𝑁)) → ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))):(1...𝑁)–1-1-onto→(1...𝑁))
328	24, 326, 327	syl2anc 691	. . . . . 6 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))):(1...𝑁)–1-1-onto→(1...𝑁))
329	97	mptex 6390	. . . . . . . 8 ⊢ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ∈ V
330	21, 329	coex 7011	. . . . . . 7 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) ∈ V
331		f1oeq1 6040	. . . . . . 7 ⊢ (𝑓 = ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))):(1...𝑁)–1-1-onto→(1...𝑁)))
332	330, 331	elab 3319	. . . . . 6 ⊢ (((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))):(1...𝑁)–1-1-onto→(1...𝑁))
333	328, 332	sylibr 223	. . . . 5 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
334		opelxpi 5072	. . . . 5 ⊢ (((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)) ∧ ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩ ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
335	231, 333, 334	syl2anc 691	. . . 4 ⊢ (𝜑 → ⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩ ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
336	27	nnnn0d 11228	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
337		0elfz 12305	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → 0 ∈ (0...𝑁))
338	336, 337	syl 17	. . . 4 ⊢ (𝜑 → 0 ∈ (0...𝑁))
339		opelxpi 5072	. . . 4 ⊢ ((⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩ ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 0 ∈ (0...𝑁)) → ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
340	335, 338, 339	syl2anc 691	. . 3 ⊢ (𝜑 → ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
341		poimirlem22.1	. . . . 5 ⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑_𝑚 (1...𝑁)))
342	27, 10, 341, 8, 41, 169	poimirlem19 32598	. . . 4 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))))
343		elfzle1 12215	. . . . . . . . 9 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 0 ≤ 𝑦)
344		0re 9919	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
345		lenlt 9995	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0 ≤ 𝑦 ↔ ¬ 𝑦 < 0))
346	344, 61, 345	sylancr 694	. . . . . . . . 9 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (0 ≤ 𝑦 ↔ ¬ 𝑦 < 0))
347	343, 346	mpbid 221	. . . . . . . 8 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ¬ 𝑦 < 0)
348	347	iffalsed 4047	. . . . . . 7 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → if(𝑦 < 0, 𝑦, (𝑦 + 1)) = (𝑦 + 1))
349	348	csbeq1d 3506	. . . . . 6 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑦 + 1) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))))
350		ovex 6577	. . . . . . 7 ⊢ (𝑦 + 1) ∈ V
351		oveq2 6557	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑦 + 1) → (1...𝑗) = (1...(𝑦 + 1)))
352	351	imaeq2d 5385	. . . . . . . . . 10 ⊢ (𝑗 = (𝑦 + 1) → (((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) = (((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))))
353	352	xpeq1d 5062	. . . . . . . . 9 ⊢ (𝑗 = (𝑦 + 1) → ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) = ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}))
354		oveq1 6556	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑦 + 1) → (𝑗 + 1) = ((𝑦 + 1) + 1))
355	354	oveq1d 6564	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑦 + 1) → ((𝑗 + 1)...𝑁) = (((𝑦 + 1) + 1)...𝑁))
356	355	imaeq2d 5385	. . . . . . . . . 10 ⊢ (𝑗 = (𝑦 + 1) → (((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) = (((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)))
357	356	xpeq1d 5062	. . . . . . . . 9 ⊢ (𝑗 = (𝑦 + 1) → ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}) = ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
358	353, 357	uneq12d 3730	. . . . . . . 8 ⊢ (𝑗 = (𝑦 + 1) → (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0})) = (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
359	358	oveq2d 6565	. . . . . . 7 ⊢ (𝑗 = (𝑦 + 1) → ((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
360	350, 359	csbie 3525	. . . . . 6 ⊢ ⦋(𝑦 + 1) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
361	349, 360	syl6eq 2660	. . . . 5 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
362	361	mpteq2ia 4668	. . . 4 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
363	342, 362	syl6eqr 2662	. . 3 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0})))))
364		opex 4859	. . . . . . . . . . 11 ⊢ ⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩ ∈ V
365	364, 51	op2ndd 7070	. . . . . . . . . 10 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → (2^nd ‘𝑡) = 0)
366	365	breq2d 4595	. . . . . . . . 9 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < 0))
367	366	ifbid 4058	. . . . . . . 8 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < 0, 𝑦, (𝑦 + 1)))
368	367	csbeq1d 3506	. . . . . . 7 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
369	364, 51	op1std 7069	. . . . . . . . . 10 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → (1^st ‘𝑡) = ⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩)
370	97	mptex 6390	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∈ V
371	370, 330	op1std 7069	. . . . . . . . . 10 ⊢ ((1^st ‘𝑡) = ⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩ → (1^st ‘(1^st ‘𝑡)) = (𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))))
372	369, 371	syl 17	. . . . . . . . 9 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → (1^st ‘(1^st ‘𝑡)) = (𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))))
373	370, 330	op2ndd 7070	. . . . . . . . . . . . 13 ⊢ ((1^st ‘𝑡) = ⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩ → (2^nd ‘(1^st ‘𝑡)) = ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))))
374	369, 373	syl 17	. . . . . . . . . . . 12 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → (2^nd ‘(1^st ‘𝑡)) = ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))))
375	374	imaeq1d 5384	. . . . . . . . . . 11 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = (((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)))
376	375	xpeq1d 5062	. . . . . . . . . 10 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}))
377	374	imaeq1d 5384	. . . . . . . . . . 11 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = (((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)))
378	377	xpeq1d 5062	. . . . . . . . . 10 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))
379	376, 378	uneq12d 3730	. . . . . . . . 9 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0})))
380	372, 379	oveq12d 6567	. . . . . . . 8 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → ((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))))
381	380	csbeq2dv 3944	. . . . . . 7 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))))
382	368, 381	eqtrd 2644	. . . . . 6 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))))
383	382	mpteq2dv 4673	. . . . 5 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0})))))
384	383	eqeq2d 2620	. . . 4 ⊢ (𝑡 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))))))
385	384, 10	elrab2 3333	. . 3 ⊢ (⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ ∈ 𝑆 ↔ (⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 0, 𝑦, (𝑦 + 1)) / 𝑗⦌((𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))) ∘_𝑓 + (((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑗)) × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((𝑗 + 1)...𝑁)) × {0}))))))
386	340, 363, 385	sylanbrc 695	. 2 ⊢ (𝜑 → ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ ∈ 𝑆)
387	364, 51	op2ndd 7070	. . . . . 6 ⊢ (𝑇 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → (2^nd ‘𝑇) = 0)
388	387	eqcoms 2618	. . . . 5 ⊢ (⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ = 𝑇 → (2^nd ‘𝑇) = 0)
389	27	nnne0d 10942	. . . . . . 7 ⊢ (𝜑 → 𝑁 ≠ 0)
390	389	necomd 2837	. . . . . 6 ⊢ (𝜑 → 0 ≠ 𝑁)
391		neeq1 2844	. . . . . 6 ⊢ ((2^nd ‘𝑇) = 0 → ((2^nd ‘𝑇) ≠ 𝑁 ↔ 0 ≠ 𝑁))
392	390, 391	syl5ibrcom 236	. . . . 5 ⊢ (𝜑 → ((2^nd ‘𝑇) = 0 → (2^nd ‘𝑇) ≠ 𝑁))
393	388, 392	syl5 33	. . . 4 ⊢ (𝜑 → (⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ = 𝑇 → (2^nd ‘𝑇) ≠ 𝑁))
394	393	necon2d 2805	. . 3 ⊢ (𝜑 → ((2^nd ‘𝑇) = 𝑁 → ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ ≠ 𝑇))
395	169, 394	mpd 15	. 2 ⊢ (𝜑 → ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ ≠ 𝑇)
396		neeq1 2844	. . 3 ⊢ (𝑧 = ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ → (𝑧 ≠ 𝑇 ↔ ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ ≠ 𝑇))
397	396	rspcev 3282	. 2 ⊢ ((⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ ∈ 𝑆 ∧ ⟨⟨(𝑛 ∈ (1...𝑁) ↦ (((1^st ‘(1^st ‘𝑇))‘𝑛) − if(𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑁), 1, 0))), ((2^nd ‘(1^st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))⟩, 0⟩ ≠ 𝑇) → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)
398	386, 395, 397	syl2anc 691	1 ⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)

Colors of variables: wff setvar class

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

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

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

This theorem is referenced by: poimirlem21 32600

W3C validator