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

Theorem poimirlem16 35066
 Description: Lemma for poimir 35083 establishing the vertices of the simplex of poimirlem17 35067. (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(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
poimirlem22.1 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))
poimirlem22.2 (𝜑𝑇𝑆)
poimirlem18.3 ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 𝐾)
poimirlem18.4 (𝜑 → (2nd𝑇) = 0)
Assertion
Ref Expression
poimirlem16 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))) ∘f + (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))))
Distinct variable groups:   𝑓,𝑗,𝑛,𝑝,𝑡,𝑦   𝜑,𝑗,𝑛,𝑦   𝑗,𝐹,𝑛,𝑦   𝑗,𝑁,𝑛,𝑦   𝑇,𝑗,𝑛,𝑦   𝜑,𝑝,𝑡   𝑓,𝐾,𝑗,𝑛,𝑝,𝑡   𝑓,𝑁,𝑝,𝑡   𝑇,𝑓,𝑝   𝑓,𝐹,𝑝,𝑡   𝑡,𝑇   𝑆,𝑗,𝑛,𝑝,𝑡,𝑦
Allowed substitution hints:   𝜑(𝑓)   𝑆(𝑓)   𝐾(𝑦)

Proof of Theorem poimirlem16
StepHypRef Expression
1 poimirlem22.2 . . 3 (𝜑𝑇𝑆)
2 fveq2 6649 . . . . . . . . . . 11 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
32breq2d 5045 . . . . . . . . . 10 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
43ifbid 4450 . . . . . . . . 9 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
54csbeq1d 3835 . . . . . . . 8 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
6 2fveq3 6654 . . . . . . . . . 10 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
7 2fveq3 6654 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
87imaeq1d 5899 . . . . . . . . . . . 12 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
98xpeq1d 5552 . . . . . . . . . . 11 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
107imaeq1d 5899 . . . . . . . . . . . 12 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
1110xpeq1d 5552 . . . . . . . . . . 11 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
129, 11uneq12d 4094 . . . . . . . . . 10 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
136, 12oveq12d 7157 . . . . . . . . 9 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
1413csbeq2dv 3838 . . . . . . . 8 (𝑡 = 𝑇if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
155, 14eqtrd 2836 . . . . . . 7 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
1615mpteq2dv 5129 . . . . . 6 (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
1716eqeq2d 2812 . . . . 5 (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
18 poimirlem22.s . . . . 5 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
1917, 18elrab2 3634 . . . 4 (𝑇𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
2019simprbi 500 . . 3 (𝑇𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
211, 20syl 17 . 2 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
22 elrabi 3626 . . . . . . . . . . . 12 (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
2322, 18eleq2s 2911 . . . . . . . . . . 11 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
241, 23syl 17 . . . . . . . . . 10 (𝜑𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
25 xp1st 7707 . . . . . . . . . 10 (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
2624, 25syl 17 . . . . . . . . 9 (𝜑 → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
27 xp1st 7707 . . . . . . . . 9 ((1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
2826, 27syl 17 . . . . . . . 8 (𝜑 → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
29 elmapfn 8416 . . . . . . . 8 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑇)) Fn (1...𝑁))
3028, 29syl 17 . . . . . . 7 (𝜑 → (1st ‘(1st𝑇)) Fn (1...𝑁))
3130adantr 484 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1st ‘(1st𝑇)) Fn (1...𝑁))
32 1ex 10630 . . . . . . . . . 10 1 ∈ V
33 fnconstg 6545 . . . . . . . . . 10 (1 ∈ V → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
3432, 33ax-mp 5 . . . . . . . . 9 (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1)))
35 c0ex 10628 . . . . . . . . . 10 0 ∈ V
36 fnconstg 6545 . . . . . . . . . 10 (0 ∈ V → (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
3735, 36ax-mp 5 . . . . . . . . 9 (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))
3834, 37pm3.2i 474 . . . . . . . 8 ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∧ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
39 xp2nd 7708 . . . . . . . . . . . . 13 ((1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
4026, 39syl 17 . . . . . . . . . . . 12 (𝜑 → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
41 fvex 6662 . . . . . . . . . . . . 13 (2nd ‘(1st𝑇)) ∈ V
42 f1oeq1 6583 . . . . . . . . . . . . 13 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
4341, 42elab 3618 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
4440, 43sylib 221 . . . . . . . . . . 11 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
45 dff1o3 6600 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑇))))
4645simprbi 500 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑇)))
4744, 46syl 17 . . . . . . . . . 10 (𝜑 → Fun (2nd ‘(1st𝑇)))
48 imain 6413 . . . . . . . . . 10 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
4947, 48syl 17 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
50 elfznn0 12999 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ0)
51 nn0p1nn 11928 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ0 → (𝑦 + 1) ∈ ℕ)
5250, 51syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℕ)
5352nnred 11644 . . . . . . . . . . . . 13 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℝ)
5453ltp1d 11563 . . . . . . . . . . . 12 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) < ((𝑦 + 1) + 1))
55 fzdisj 12933 . . . . . . . . . . . 12 ((𝑦 + 1) < ((𝑦 + 1) + 1) → ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
5654, 55syl 17 . . . . . . . . . . 11 (𝑦 ∈ (0...(𝑁 − 1)) → ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
5756imaeq2d 5900 . . . . . . . . . 10 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
58 ima0 5916 . . . . . . . . . 10 ((2nd ‘(1st𝑇)) “ ∅) = ∅
5957, 58eqtrdi 2852 . . . . . . . . 9 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ∅)
6049, 59sylan9req 2857 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅)
61 fnun 6438 . . . . . . . 8 ((((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∧ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) ∧ (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅) → ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
6238, 60, 61sylancr 590 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
63 imaundi 5979 . . . . . . . . 9 ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
64 nnuz 12273 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
6552, 64eleqtrdi 2903 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (ℤ‘1))
66 peano2uz 12293 . . . . . . . . . . . . . 14 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1) + 1) ∈ (ℤ‘1))
6765, 66syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ (ℤ‘1))
6867adantl 485 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1) + 1) ∈ (ℤ‘1))
69 poimir.0 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ)
7069nncnd 11645 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℂ)
71 npcan1 11058 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
7270, 71syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
7372adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
74 elfzuz3 12903 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ𝑦))
75 eluzp1p1 12262 . . . . . . . . . . . . . . 15 ((𝑁 − 1) ∈ (ℤ𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
7674, 75syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
7776adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
7873, 77eqeltrrd 2894 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘(𝑦 + 1)))
79 fzsplit2 12931 . . . . . . . . . . . 12 ((((𝑦 + 1) + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘(𝑦 + 1))) → (1...𝑁) = ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
8068, 78, 79syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) = ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
8180imaeq2d 5900 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))))
82 f1ofo 6601 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
83 foima 6574 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
8444, 82, 833syl 18 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
8584adantr 484 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
8681, 85eqtr3d 2838 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (1...𝑁))
8763, 86syl5eqr 2850 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = (1...𝑁))
8887fneq2d 6421 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) ↔ ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)))
8962, 88mpbid 235 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
90 ovexd 7174 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) ∈ V)
91 inidm 4148 . . . . . 6 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
92 eqidd 2802 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) = ((1st ‘(1st𝑇))‘𝑛))
93 eqidd 2802 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛))
9431, 89, 90, 90, 91, 92, 93offval 7400 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) = (𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛))))
95 oveq1 7146 . . . . . . . . . 10 (1 = if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) → (1 + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)) = (if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)))
9695eqeq2d 2812 . . . . . . . . 9 (1 = if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) → ((((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (1 + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)) ↔ (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))))
97 oveq1 7146 . . . . . . . . . 10 (0 = if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) → (0 + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)) = (if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)))
9897eqeq2d 2812 . . . . . . . . 9 (0 = if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) → ((((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (0 + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)) ↔ (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))))
99 1p0e1 11753 . . . . . . . . . . . . . 14 (1 + 0) = 1
10099eqcomi 2810 . . . . . . . . . . . . 13 1 = (1 + 0)
101 f1ofn 6595 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
10244, 101syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (2nd ‘(1st𝑇)) Fn (1...𝑁))
103102adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
104 fzss2 12946 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘(𝑦 + 1)) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
10578, 104syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
106 eluzfz1 12913 . . . . . . . . . . . . . . . . . 18 ((𝑦 + 1) ∈ (ℤ‘1) → 1 ∈ (1...(𝑦 + 1)))
10765, 106syl 17 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → 1 ∈ (1...(𝑦 + 1)))
108107adantl 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 1 ∈ (1...(𝑦 + 1)))
109 fnfvima 6977 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ (1...(𝑦 + 1)) ⊆ (1...𝑁) ∧ 1 ∈ (1...(𝑦 + 1))) → ((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
110103, 105, 108, 109syl3anc 1368 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
111 fvun1 6733 . . . . . . . . . . . . . . . 16 (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∧ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) ∧ ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅ ∧ ((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd ‘(1st𝑇))‘1)))
11234, 37, 111mp3an12 1448 . . . . . . . . . . . . . . 15 (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅ ∧ ((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1)))) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd ‘(1st𝑇))‘1)))
11360, 110, 112syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd ‘(1st𝑇))‘1)))
11432fvconst2 6947 . . . . . . . . . . . . . . 15 (((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) → ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd ‘(1st𝑇))‘1)) = 1)
115110, 114syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd ‘(1st𝑇))‘1)) = 1)
116113, 115eqtrd 2836 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = 1)
117 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → 𝑛 ∈ (1...(𝑁 − 1)))
11869nnzd 12078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℤ)
119 peano2zm 12017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
120118, 119syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑁 − 1) ∈ ℤ)
121 1z 12004 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ ℤ
122120, 121jctil 523 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ))
123 elfzelz 12906 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℤ)
124123, 121jctir 524 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ (1...(𝑁 − 1)) → (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
125 fzaddel 12940 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ (1...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1))))
126122, 124, 125syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 ∈ (1...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1))))
127117, 126mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1)))
12872oveq2d 7155 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 + 1)...𝑁))
129128adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 + 1)...𝑁))
130127, 129eleqtrd 2895 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 + 1) ∈ ((1 + 1)...𝑁))
131130ralrimiva 3152 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑛 + 1) ∈ ((1 + 1)...𝑁))
132 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → 𝑦 ∈ ((1 + 1)...𝑁))
133 peano2z 12015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 ∈ ℤ → (1 + 1) ∈ ℤ)
134121, 133ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (1 + 1) ∈ ℤ
135118, 134jctil 523 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ))
136 elfzelz 12906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ((1 + 1)...𝑁) → 𝑦 ∈ ℤ)
137136, 121jctir 524 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ((1 + 1)...𝑁) → (𝑦 ∈ ℤ ∧ 1 ∈ ℤ))
138 fzsubel 12942 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑦 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑦 ∈ ((1 + 1)...𝑁) ↔ (𝑦 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
139135, 137, 138syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 ∈ ((1 + 1)...𝑁) ↔ (𝑦 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
140132, 139mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1)))
141 ax-1cn 10588 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ ℂ
142141, 141pncan3oi 10895 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 + 1) − 1) = 1
143142oveq1i 7149 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 + 1) − 1)...(𝑁 − 1)) = (1...(𝑁 − 1))
144140, 143eleqtrdi 2903 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 − 1) ∈ (1...(𝑁 − 1)))
145136zcnd 12080 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ((1 + 1)...𝑁) → 𝑦 ∈ ℂ)
146 elfznn 12935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℕ)
147146nncnd 11645 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℂ)
148 subadd2 10883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑦 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑦 − 1) = 𝑛 ↔ (𝑛 + 1) = 𝑦))
149141, 148mp3an2 1446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑦 − 1) = 𝑛 ↔ (𝑛 + 1) = 𝑦))
150149bicomd 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑛 + 1) = 𝑦 ↔ (𝑦 − 1) = 𝑛))
151 eqcom 2808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑛 + 1) = 𝑦𝑦 = (𝑛 + 1))
152 eqcom 2808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦 − 1) = 𝑛𝑛 = (𝑦 − 1))
153150, 151, 1523bitr3g 316 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1)))
154145, 147, 153syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ((1 + 1)...𝑁) ∧ 𝑛 ∈ (1...(𝑁 − 1))) → (𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1)))
155154ralrimiva 3152 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((1 + 1)...𝑁) → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1)))
156155adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1)))
157 reu6i 3670 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑦 − 1) ∈ (1...(𝑁 − 1)) ∧ ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) → ∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1))
158144, 156, 157syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → ∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1))
159158ralrimiva 3152 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑦 ∈ ((1 + 1)...𝑁)∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1))
160 eqid 2801 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) = (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1))
161160f1ompt 6856 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 + 1)...𝑁) ↔ (∀𝑛 ∈ (1...(𝑁 − 1))(𝑛 + 1) ∈ ((1 + 1)...𝑁) ∧ ∀𝑦 ∈ ((1 + 1)...𝑁)∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1)))
162131, 159, 161sylanbrc 586 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 + 1)...𝑁))
163 f1osng 6634 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ 1 ∈ V) → {⟨𝑁, 1⟩}:{𝑁}–1-1-onto→{1})
16469, 32, 163sylancl 589 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {⟨𝑁, 1⟩}:{𝑁}–1-1-onto→{1})
16569nnred 11644 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑁 ∈ ℝ)
166165ltm1d 11565 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑁 − 1) < 𝑁)
167120zred 12079 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑁 − 1) ∈ ℝ)
168167, 165ltnled 10780 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
169166, 168mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
170 elfzle2 12910 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
171169, 170nsyl 142 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
172 disjsn 4610 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1)))
173171, 172sylibr 237 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅)
174 1re 10634 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 ∈ ℝ
175174ltp1i 11537 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 < (1 + 1)
176174, 174readdcli 10649 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (1 + 1) ∈ ℝ
177174, 176ltnlei 10754 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 < (1 + 1) ↔ ¬ (1 + 1) ≤ 1)
178175, 177mpbi 233 . . . . . . . . . . . . . . . . . . . . . . . . 25 ¬ (1 + 1) ≤ 1
179 elfzle1 12909 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ((1 + 1)...𝑁) → (1 + 1) ≤ 1)
180178, 179mto 200 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ 1 ∈ ((1 + 1)...𝑁)
181 disjsn 4610 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((1 + 1)...𝑁) ∩ {1}) = ∅ ↔ ¬ 1 ∈ ((1 + 1)...𝑁))
182180, 181mpbir 234 . . . . . . . . . . . . . . . . . . . . . . 23 (((1 + 1)...𝑁) ∩ {1}) = ∅
183 f1oun 6613 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 + 1)...𝑁) ∧ {⟨𝑁, 1⟩}:{𝑁}–1-1-onto→{1}) ∧ (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ∧ (((1 + 1)...𝑁) ∩ {1}) = ∅)) → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}):((1...(𝑁 − 1)) ∪ {𝑁})–1-1-onto→(((1 + 1)...𝑁) ∪ {1}))
184182, 183mpanr2 703 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 + 1)...𝑁) ∧ {⟨𝑁, 1⟩}:{𝑁}–1-1-onto→{1}) ∧ ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅) → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}):((1...(𝑁 − 1)) ∪ {𝑁})–1-1-onto→(((1 + 1)...𝑁) ∪ {1}))
185162, 164, 173, 184syl21anc 836 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}):((1...(𝑁 − 1)) ∪ {𝑁})–1-1-onto→(((1 + 1)...𝑁) ∪ {1}))
186 ssv 3942 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℕ ⊆ V
187186, 69sseldi 3916 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑁 ∈ V)
18832a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ∈ V)
18969, 64eleqtrdi 2903 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑁 ∈ (ℤ‘1))
19072, 189eqeltrd 2893 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘1))
191 uzid 12250 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
192 peano2uz 12293 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
193120, 191, 1923syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
19472, 193eqeltrrd 2894 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
195 fzsplit2 12931 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
196190, 194, 195syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
19772oveq1d 7154 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
198 fzsn 12948 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
199118, 198syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑁...𝑁) = {𝑁})
200197, 199eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
201200uneq2d 4093 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁}))
202196, 201eqtr2d 2837 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁))
203 iftrue 4434 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑁 → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = 1)
204203adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑛 = 𝑁) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = 1)
205187, 188, 202, 204fmptapd 6914 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∪ {⟨𝑁, 1⟩}) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))
206 eleq1 2880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑁 → (𝑛 ∈ (1...(𝑁 − 1)) ↔ 𝑁 ∈ (1...(𝑁 − 1))))
207206notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑁 → (¬ 𝑛 ∈ (1...(𝑁 − 1)) ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1))))
208171, 207syl5ibrcom 250 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑛 = 𝑁 → ¬ 𝑛 ∈ (1...(𝑁 − 1))))
209208necon2ad 3005 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛𝑁))
210209imp 410 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → 𝑛𝑁)
211 ifnefalse 4440 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛𝑁 → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1))
212210, 211syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1))
213212mpteq2dva 5128 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)))
214213uneq1d 4092 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∪ {⟨𝑁, 1⟩}) = ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}))
215205, 214eqtr3d 2838 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}))
216196, 201eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁}))
217 uzid 12250 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℤ → 1 ∈ (ℤ‘1))
218 peano2uz 12293 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ (ℤ‘1) → (1 + 1) ∈ (ℤ‘1))
219121, 217, 218mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 + 1) ∈ (ℤ‘1)
220 fzsplit2 12931 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘1)) → (1...𝑁) = ((1...1) ∪ ((1 + 1)...𝑁)))
221219, 189, 220sylancr 590 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑁) = ((1...1) ∪ ((1 + 1)...𝑁)))
222 fzsn 12948 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 ∈ ℤ → (1...1) = {1})
223121, 222ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1...1) = {1}
224223uneq1i 4089 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1...1) ∪ ((1 + 1)...𝑁)) = ({1} ∪ ((1 + 1)...𝑁))
225224equncomi 4085 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...1) ∪ ((1 + 1)...𝑁)) = (((1 + 1)...𝑁) ∪ {1})
226221, 225eqtrdi 2852 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1...𝑁) = (((1 + 1)...𝑁) ∪ {1}))
227215, 216, 226f1oeq123d 6589 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}):((1...(𝑁 − 1)) ∪ {𝑁})–1-1-onto→(((1 + 1)...𝑁) ∪ {1})))
228185, 227mpbird 260 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁))
229 f1oco 6616 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ∧ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁)) → ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁))
23044, 228, 229syl2anc 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁))
231 dff1o3 6600 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁) ↔ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–onto→(1...𝑁) ∧ Fun ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))))
232231simprbi 500 . . . . . . . . . . . . . . . . . . 19 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))))
233230, 232syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → Fun ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))))
234 imain 6413 . . . . . . . . . . . . . . . . . 18 (Fun ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))))
235233, 234syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))))
23650nn0red 11948 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
237236ltp1d 11563 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 < (𝑦 + 1))
238 fzdisj 12933 . . . . . . . . . . . . . . . . . . . 20 (𝑦 < (𝑦 + 1) → ((1...𝑦) ∩ ((𝑦 + 1)...𝑁)) = ∅)
239237, 238syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → ((1...𝑦) ∩ ((𝑦 + 1)...𝑁)) = ∅)
240239imaeq2d 5900 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0...(𝑁 − 1)) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ∅))
241 ima0 5916 . . . . . . . . . . . . . . . . . 18 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ∅) = ∅
242240, 241eqtrdi 2852 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = ∅)
243235, 242sylan9req 2857 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))) = ∅)
244 imassrn 5911 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)) ⊆ ran (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))
245 f1of 6594 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁) → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)⟶(1...𝑁))
246 frn 6497 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)⟶(1...𝑁) → ran (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ⊆ (1...𝑁))
247228, 245, 2463syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ran (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ⊆ (1...𝑁))
248244, 247sstrid 3929 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)) ⊆ (1...𝑁))
249248adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)) ⊆ (1...𝑁))
250 elfz1end 12936 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
25169, 250sylib 221 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑁 ∈ (1...𝑁))
252 eqid 2801 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))
253203, 252, 32fvmpt 6749 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (1...𝑁) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) = 1)
254251, 253syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) = 1)
255254adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) = 1)
256 f1ofn 6595 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁) → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁))
257228, 256syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁))
258257adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁))
259 fzss1 12945 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
26065, 259syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
261260adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
262 eluzfz2 12914 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (ℤ‘(𝑦 + 1)) → 𝑁 ∈ ((𝑦 + 1)...𝑁))
26378, 262syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑦 + 1)...𝑁))
264 fnfvima 6977 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁) ∧ ((𝑦 + 1)...𝑁) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑦 + 1)...𝑁)) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)))
265258, 261, 263, 264syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)))
266255, 265eqeltrrd 2894 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 1 ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)))
267 fnfvima 6977 . . . . . . . . . . . . . . . . . 18 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)) ⊆ (1...𝑁) ∧ 1 ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁))) → ((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁))))
268103, 249, 266, 267syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁))))
269 imaco 6075 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)))
270268, 269eleqtrrdi 2904 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇))‘1) ∈ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)))
271 fnconstg 6545 . . . . . . . . . . . . . . . . . 18 (1 ∈ V → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)))
27232, 271ax-mp 5 . . . . . . . . . . . . . . . . 17 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦))
273 fnconstg 6545 . . . . . . . . . . . . . . . . . 18 (0 ∈ V → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)))
27435, 273ax-mp 5 . . . . . . . . . . . . . . . . 17 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))
275 fvun2 6734 . . . . . . . . . . . . . . . . 17 ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∧ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) ∧ (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))) = ∅ ∧ ((2nd ‘(1st𝑇))‘1) ∈ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)))) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘1)))
276272, 274, 275mp3an12 1448 . . . . . . . . . . . . . . . 16 ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))) = ∅ ∧ ((2nd ‘(1st𝑇))‘1) ∈ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘1)))
277243, 270, 276syl2anc 587 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘1)))
27835fvconst2 6947 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇))‘1) ∈ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘1)) = 0)
279270, 278syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘1)) = 0)
280277, 279eqtrd 2836 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = 0)
281280oveq2d 7155 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1 + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1))) = (1 + 0))
282100, 116, 2813eqtr4a 2862 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = (1 + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1))))
283 fveq2 6649 . . . . . . . . . . . . 13 (𝑛 = ((2nd ‘(1st𝑇))‘1) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)))
284 fveq2 6649 . . . . . . . . . . . . . 14 (𝑛 = ((2nd ‘(1st𝑇))‘1) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) = ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)))
285284oveq2d 7155 . . . . . . . . . . . . 13 (𝑛 = ((2nd ‘(1st𝑇))‘1) → (1 + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)) = (1 + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1))))
286283, 285eqeq12d 2817 . . . . . . . . . . . 12 (𝑛 = ((2nd ‘(1st𝑇))‘1) → ((((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (1 + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)) ↔ (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = (1 + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)))))
287282, 286syl5ibrcom 250 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 = ((2nd ‘(1st𝑇))‘1) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (1 + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))))
288287imp 410 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 = ((2nd ‘(1st𝑇))‘1)) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (1 + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)))
289288adantlr 714 . . . . . . . . 9 ((((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 = ((2nd ‘(1st𝑇))‘1)) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (1 + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)))
290 eldifsn 4683 . . . . . . . . . . . . . 14 (𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ↔ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘1)))
291 df-ne 2991 . . . . . . . . . . . . . . 15 (𝑛 ≠ ((2nd ‘(1st𝑇))‘1) ↔ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1))
292291anbi2i 625 . . . . . . . . . . . . . 14 ((𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘1)) ↔ (𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1)))
293290, 292bitri 278 . . . . . . . . . . . . 13 (𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ↔ (𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1)))
294 fnconstg 6545 . . . . . . . . . . . . . . . . . 18 (1 ∈ V → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
29532, 294ax-mp 5 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1)))
296295, 37pm3.2i 474 . . . . . . . . . . . . . . . 16 ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∧ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
297 imain 6413 . . . . . . . . . . . . . . . . . 18 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
29847, 297syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
299 fzdisj 12933 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 + 1) < ((𝑦 + 1) + 1) → (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
30054, 299syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
301300imaeq2d 5900 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
302301, 58eqtrdi 2852 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ∅)
303298, 302sylan9req 2857 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅)
304 fnun 6438 . . . . . . . . . . . . . . . 16 ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∧ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) ∧ (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅) → ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
305296, 303, 304sylancr 590 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
306 imaundi 5979 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
307 fzpred 12954 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ‘1) → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁)))
308189, 307syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁)))
309 uncom 4083 . . . . . . . . . . . . . . . . . . . . . . . 24 ({1} ∪ ((1 + 1)...𝑁)) = (((1 + 1)...𝑁) ∪ {1})
310308, 309eqtrdi 2852 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑁) = (((1 + 1)...𝑁) ∪ {1}))
311310difeq1d 4052 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...𝑁) ∖ {1}) = ((((1 + 1)...𝑁) ∪ {1}) ∖ {1}))
312 difun2 4390 . . . . . . . . . . . . . . . . . . . . . . 23 ((((1 + 1)...𝑁) ∪ {1}) ∖ {1}) = (((1 + 1)...𝑁) ∖ {1})
313 disj3 4364 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((1 + 1)...𝑁) ∩ {1}) = ∅ ↔ ((1 + 1)...𝑁) = (((1 + 1)...𝑁) ∖ {1}))
314182, 313mpbi 233 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 + 1)...𝑁) = (((1 + 1)...𝑁) ∖ {1})
315312, 314eqtr4i 2827 . . . . . . . . . . . . . . . . . . . . . 22 ((((1 + 1)...𝑁) ∪ {1}) ∖ {1}) = ((1 + 1)...𝑁)
316311, 315eqtrdi 2852 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((1...𝑁) ∖ {1}) = ((1 + 1)...𝑁))
317316adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1...𝑁) ∖ {1}) = ((1 + 1)...𝑁))
318 eluzp1p1 12262 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1) + 1) ∈ (ℤ‘(1 + 1)))
31965, 318syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ (ℤ‘(1 + 1)))
320319adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1) + 1) ∈ (ℤ‘(1 + 1)))
321 fzsplit2 12931 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 + 1) + 1) ∈ (ℤ‘(1 + 1)) ∧ 𝑁 ∈ (ℤ‘(𝑦 + 1))) → ((1 + 1)...𝑁) = (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
322320, 78, 321syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1 + 1)...𝑁) = (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
323317, 322eqtrd 2836 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1...𝑁) ∖ {1}) = (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
324323imaeq2d 5900 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))))
325 imadif 6412 . . . . . . . . . . . . . . . . . . . . 21 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {1})))
32647, 325syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {1})))
327 eluzfz1 12913 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ‘1) → 1 ∈ (1...𝑁))
328189, 327syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 ∈ (1...𝑁))
329 fnsnfv 6722 . . . . . . . . . . . . . . . . . . . . . . 23 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ 1 ∈ (1...𝑁)) → {((2nd ‘(1st𝑇))‘1)} = ((2nd ‘(1st𝑇)) “ {1}))
330102, 328, 329syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {((2nd ‘(1st𝑇))‘1)} = ((2nd ‘(1st𝑇)) “ {1}))
331330eqcomd 2807 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((2nd ‘(1st𝑇)) “ {1}) = {((2nd ‘(1st𝑇))‘1)})
33284, 331difeq12d 4054 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {1})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
333326, 332eqtrd 2836 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
334333adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
335324, 334eqtr3d 2838 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
336306, 335syl5eqr 2850 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
337336fneq2d 6421 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) ↔ ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)})))
338305, 337mpbid 235 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
339 incom 4131 . . . . . . . . . . . . . . . 16 (((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∩ {((2nd ‘(1st𝑇))‘1)}) = ({((2nd ‘(1st𝑇))‘1)} ∩ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
340 disjdif 4382 . . . . . . . . . . . . . . . 16 ({((2nd ‘(1st𝑇))‘1)} ∩ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)})) = ∅
341339, 340eqtri 2824 . . . . . . . . . . . . . . 15 (((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∩ {((2nd ‘(1st𝑇))‘1)}) = ∅
342 fnconstg 6545 . . . . . . . . . . . . . . . . . 18 (1 ∈ V → ({((2nd ‘(1st𝑇))‘1)} × {1}) Fn {((2nd ‘(1st𝑇))‘1)})
34332, 342ax-mp 5 . . . . . . . . . . . . . . . . 17 ({((2nd ‘(1st𝑇))‘1)} × {1}) Fn {((2nd ‘(1st𝑇))‘1)}
344 fvun1 6733 . . . . . . . . . . . . . . . . 17 ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∧ ({((2nd ‘(1st𝑇))‘1)} × {1}) Fn {((2nd ‘(1st𝑇))‘1)} ∧ ((((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∩ {((2nd ‘(1st𝑇))‘1)}) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))) → ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛))
345343, 344mp3an2 1446 . . . . . . . . . . . . . . . 16 ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∧ ((((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∩ {((2nd ‘(1st𝑇))‘1)}) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))) → ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛))
346 fnconstg 6545 . . . . . . . . . . . . . . . . . 18 (0 ∈ V → ({((2nd ‘(1st𝑇))‘1)} × {0}) Fn {((2nd ‘(1st𝑇))‘1)})
34735, 346ax-mp 5 . . . . . . . . . . . . . . . . 17 ({((2nd ‘(1st𝑇))‘1)} × {0}) Fn {((2nd ‘(1st𝑇))‘1)}
348 fvun1 6733 . . . . . . . . . . . . . . . . 17 ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∧ ({((2nd ‘(1st𝑇))‘1)} × {0}) Fn {((2nd ‘(1st𝑇))‘1)} ∧ ((((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∩ {((2nd ‘(1st𝑇))‘1)}) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))) → ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {0}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛))
349347, 348mp3an2 1446 . . . . . . . . . . . . . . . 16 ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∧ ((((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∩ {((2nd ‘(1st𝑇))‘1)}) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))) → ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {0}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛))
350345, 349eqtr4d 2839 . . . . . . . . . . . . . . 15 ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∧ ((((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∩ {((2nd ‘(1st𝑇))‘1)}) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))) → ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {0}))‘𝑛))
351341, 350mpanr1 702 . . . . . . . . . . . . . 14 ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)})) → ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {0}))‘𝑛))
352338, 351sylan 583 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)})) → ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {0}))‘𝑛))
353293, 352sylan2br 597 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1))) → ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {0}))‘𝑛))
354353anassrs 471 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1)) → ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {0}))‘𝑛))
355 fzpred 12954 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 + 1) ∈ (ℤ‘1) → (1...(𝑦 + 1)) = ({1} ∪ ((1 + 1)...(𝑦 + 1))))
35665, 355syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (0...(𝑁 − 1)) → (1...(𝑦 + 1)) = ({1} ∪ ((1 + 1)...(𝑦 + 1))))
357356imaeq2d 5900 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) = ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))))
358357adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) = ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))))
359330uneq1d 4092 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1)))) = (((2nd ‘(1st𝑇)) “ {1}) ∪ ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1)))))
360 uncom 4083 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) = ({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
361 imaundi 5979 . . . . . . . . . . . . . . . . . . . 20 ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))) = (((2nd ‘(1st𝑇)) “ {1}) ∪ ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
362359, 360, 3613eqtr4g 2861 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) = ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))))
363362adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) = ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))))
364358, 363eqtr4d 2839 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}))
365364xpeq1d 5552 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) = ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) × {1}))
366 xpundir 5589 . . . . . . . . . . . . . . . 16 ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) × {1}) = ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1}))
367365, 366eqtrdi 2852 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) = ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1})))
368367uneq1d 4092 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) = (((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1})) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
369 un23 4098 . . . . . . . . . . . . . 14 (((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1})) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) = (((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1}))
370368, 369eqtrdi 2852 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) = (((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1})))
371370fveq1d 6651 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1}))‘𝑛))
372371ad2antrr 725 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1)) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1}))‘𝑛))
373 imaco 6075 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦)))
374 df-ima 5536 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦)) = ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ (1...𝑦))
375 peano2uz 12293 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 − 1) ∈ (ℤ𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
37674, 375syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
377376adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
37873, 377eqeltrrd 2894 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ𝑦))
379 fzss2 12946 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ𝑦) → (1...𝑦) ⊆ (1...𝑁))
380378, 379syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑦) ⊆ (1...𝑁))
381380resmptd 5879 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ (1...𝑦)) = (𝑛 ∈ (1...𝑦) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))
382171adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
383 fzss2 12946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑁 − 1) ∈ (ℤ𝑦) → (1...𝑦) ⊆ (1...(𝑁 − 1)))
38474, 383syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ (0...(𝑁 − 1)) → (1...𝑦) ⊆ (1...(𝑁 − 1)))
385384adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑦) ⊆ (1...(𝑁 − 1)))
386385sseld 3917 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 ∈ (1...𝑦) → 𝑁 ∈ (1...(𝑁 − 1))))
387382, 386mtod 201 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ¬ 𝑁 ∈ (1...𝑦))
388 eleq1 2880 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑁 → (𝑛 ∈ (1...𝑦) ↔ 𝑁 ∈ (1...𝑦)))
389388notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑁 → (¬ 𝑛 ∈ (1...𝑦) ↔ ¬ 𝑁 ∈ (1...𝑦)))
390387, 389syl5ibrcom 250 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 = 𝑁 → ¬ 𝑛 ∈ (1...𝑦)))
391390necon2ad 3005 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑦) → 𝑛𝑁))
392391imp 410 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑦)) → 𝑛𝑁)
393392, 211syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑦)) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1))
394393mpteq2dva 5128 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑦) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)))
395381, 394eqtrd 2836 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ (1...𝑦)) = (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)))
396395rneqd 5776 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ (1...𝑦)) = ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)))
397374, 396syl5eq 2848 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦)) = ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)))
398 vex 3447 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 ∈ V
399 eqid 2801 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) = (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1))
400399elrnmpt 5796 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ V → (𝑗 ∈ ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) ↔ ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1)))
401398, 400ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) ↔ ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1))
402 elfzelz 12906 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
403402adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℤ)
404 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ (1...𝑦)) → 𝑛 ∈ (1...𝑦))
405121jctl 527 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℤ → (1 ∈ ℤ ∧ 𝑦 ∈ ℤ))
406 elfzelz 12906 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ (1...𝑦) → 𝑛 ∈ ℤ)
407406, 121jctir 524 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ (1...𝑦) → (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
408 fzaddel 12940 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ (1...𝑦) ↔ (𝑛 + 1) ∈ ((1 + 1)...(𝑦 + 1))))
409405, 407, 408syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ (1...𝑦)) → (𝑛 ∈ (1...𝑦) ↔ (𝑛 + 1) ∈ ((1 + 1)...(𝑦 + 1))))
410404, 409mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ (1...𝑦)) → (𝑛 + 1) ∈ ((1 + 1)...(𝑦 + 1)))
411 eleq1 2880 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = (𝑛 + 1) → (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) ↔ (𝑛 + 1) ∈ ((1 + 1)...(𝑦 + 1))))
412410, 411syl5ibrcom 250 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ (1...𝑦)) → (𝑗 = (𝑛 + 1) → 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
413412rexlimdva 3246 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℤ → (∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1) → 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
414 elfzelz 12906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → 𝑗 ∈ ℤ)
415414zcnd 12080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → 𝑗 ∈ ℂ)
416 npcan1 11058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ ℂ → ((𝑗 − 1) + 1) = 𝑗)
417415, 416syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → ((𝑗 − 1) + 1) = 𝑗)
418417eleq1d 2877 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → (((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1)) ↔ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
419418ibir 271 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → ((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1)))
420419adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → ((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1)))
421 peano2zm 12017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
422414, 421syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → (𝑗 − 1) ∈ ℤ)
423422, 121jctir 524 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → ((𝑗 − 1) ∈ ℤ ∧ 1 ∈ ℤ))
424 fzaddel 12940 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ((𝑗 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝑗 − 1) ∈ (1...𝑦) ↔ ((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1))))
425405, 423, 424syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → ((𝑗 − 1) ∈ (1...𝑦) ↔ ((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1))))
426420, 425mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → (𝑗 − 1) ∈ (1...𝑦))
427415adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → 𝑗 ∈ ℂ)
428416eqcomd 2807 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ ℂ → 𝑗 = ((𝑗 − 1) + 1))
429427, 428syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → 𝑗 = ((𝑗 − 1) + 1))
430 oveq1 7146 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑗 − 1) → (𝑛 + 1) = ((𝑗 − 1) + 1))
431430rspceeqv 3589 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑗 − 1) ∈ (1...𝑦) ∧ 𝑗 = ((𝑗 − 1) + 1)) → ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1))
432426, 429, 431syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1))
433432ex 416 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℤ → (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1)))
434413, 433impbid 215 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℤ → (∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1) ↔ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
435403, 434syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1) ↔ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
436401, 435syl5bb 286 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑗 ∈ ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) ↔ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
437436eqrdv 2799 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) = ((1 + 1)...(𝑦 + 1)))
438397, 437eqtrd 2836 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦)) = ((1 + 1)...(𝑦 + 1)))
439438imaeq2d 5900 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦))) = ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
440373, 439syl5eq 2848 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) = ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
441440xpeq1d 5552 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}))
442 imaundi 5979 . . . . . . . . . . . . . . . . . . 19 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1)))) = ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ {𝑁}) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...(𝑁 − 1))))
443 imaco 6075 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ {𝑁}) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁}))
444 imaco 6075 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...(𝑁 − 1))) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))))
445443, 444uneq12i 4091 . . . . . . . . . . . . . . . . . . 19 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ {𝑁}) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...(𝑁 − 1)))) = (((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})) ∪ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1)))))
446442, 445eqtri 2824 . . . . . . . . . . . . . . . . . 18 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1)))) = (((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})) ∪ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1)))))
447194adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
448 fzsplit2 12931 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)) ∧ 𝑁 ∈ (ℤ‘(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
44977, 447, 448syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
450200uneq2d 4093 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}))
451450adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}))
452449, 451eqtrd 2836 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}))
453 uncom 4083 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}) = ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1)))
454452, 453eqtrdi 2852 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1))))
455454imaeq2d 5900 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) = (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1)))))
456254sneqd 4540 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁)} = {1})
457 fnsnfv 6722 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → {((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁)} = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁}))
458257, 251, 457syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁)} = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁}))
459456, 458eqtr3d 2838 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {1} = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁}))
460459imaeq2d 5900 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((2nd ‘(1st𝑇)) “ {1}) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})))
461330, 460eqtrd 2836 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {((2nd ‘(1st𝑇))‘1)} = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})))
462461adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → {((2nd ‘(1st𝑇))‘1)} = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})))
463 df-ima 5536 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))) = ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ ((𝑦 + 1)...(𝑁 − 1)))
464 fzss1 12945 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1)...(𝑁 − 1)) ⊆ (1...(𝑁 − 1)))
46565, 464syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...(𝑁 − 1)) ⊆ (1...(𝑁 − 1)))
466 fzss2 12946 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
467194, 466syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
468465, 467sylan9ssr 3932 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...(𝑁 − 1)) ⊆ (1...𝑁))
469468resmptd 5879 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ ((𝑦 + 1)...(𝑁 − 1))) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))
470 elfzle2 12910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑁 ∈ ((𝑦 + 1)...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
471169, 470nsyl 142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ¬ 𝑁 ∈ ((𝑦 + 1)...(𝑁 − 1)))
472 eleq1 2880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑁 → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ 𝑁 ∈ ((𝑦 + 1)...(𝑁 − 1))))
473472notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑁 → (¬ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ ¬ 𝑁 ∈ ((𝑦 + 1)...(𝑁 − 1))))
474471, 473syl5ibrcom 250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝑛 = 𝑁 → ¬ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))))
475474con2d 136 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) → ¬ 𝑛 = 𝑁))
476475imp 410 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → ¬ 𝑛 = 𝑁)
477476iffalsed 4439 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1))
478477mpteq2dva 5128 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
479478adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
480469, 479eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ ((𝑦 + 1)...(𝑁 − 1))) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
481480rneqd 5776 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ ((𝑦 + 1)...(𝑁 − 1))) = ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
482463, 481syl5eq 2848 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))) = ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
483 elfzelz 12906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → 𝑗 ∈ ℤ)
484483zcnd 12080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → 𝑗 ∈ ℂ)
485484, 416syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → ((𝑗 − 1) + 1) = 𝑗)
486485eleq1d 2877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → (((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) ↔ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
487486ibir 271 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → ((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)))
488487adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → ((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)))
48952nnzd 12078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℤ)
490120, 489anim12ci 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1) ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ))
491483, 421syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → (𝑗 − 1) ∈ ℤ)
492491, 121jctir 524 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → ((𝑗 − 1) ∈ ℤ ∧ 1 ∈ ℤ))
493 fzaddel 12940 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑦 + 1) ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) ∧ ((𝑗 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝑗 − 1) ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ ((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
494490, 492, 493syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → ((𝑗 − 1) ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ ((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
495488, 494mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → (𝑗 − 1) ∈ ((𝑦 + 1)...(𝑁 − 1)))
496484, 428syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → 𝑗 = ((𝑗 − 1) + 1))
497496adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → 𝑗 = ((𝑗 − 1) + 1))
498430rspceeqv 3589 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑗 − 1) ∈ ((𝑦 + 1)...(𝑁 − 1)) ∧ 𝑗 = ((𝑗 − 1) + 1)) → ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1))
499495, 497, 498syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1))
500499ex 416 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1)))
501 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)))
502 elfzelz 12906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) → 𝑛 ∈ ℤ)
503502, 121jctir 524 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) → (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
504 fzaddel 12940 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑦 + 1) ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
505490, 503, 504syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
506501, 505mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → (𝑛 + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)))
507 eleq1 2880 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = (𝑛 + 1) → (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) ↔ (𝑛 + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
508506, 507syl5ibrcom 250 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → (𝑗 = (𝑛 + 1) → 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
509508rexlimdva 3246 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1) → 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
510500, 509impbid 215 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) ↔ ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1)))
511 eqid 2801 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1))
512511elrnmpt 5796 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ V → (𝑗 ∈ ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)) ↔ ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1)))
513398, 512ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)) ↔ ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1))
514510, 513syl6bbr 292 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) ↔ 𝑗 ∈ ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1))))
515514eqrdv 2799 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) = ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
51672oveq2d 7155 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) = (((𝑦 + 1) + 1)...𝑁))
517516adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) = (((𝑦 + 1) + 1)...𝑁))
518482, 515, 5173eqtr2rd 2843 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1) + 1)...𝑁) = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))))
519518imaeq2d 5900 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1)))))
520462, 519uneq12d 4094 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})) ∪ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))))))
521446, 455, 5203eqtr4a 2862 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) = ({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
522521xpeq1d 5552 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}) = (({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) × {0}))
523 xpundir 5589 . . . . . . . . . . . . . . . 16 (({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) × {0}) = (({((2nd ‘(1st𝑇))‘1)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
524522, 523eqtrdi 2852 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}) = (({((2nd ‘(1st𝑇))‘1)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
525441, 524uneq12d 4094 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (({((2nd ‘(1st𝑇))‘1)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
526 unass 4096 . . . . . . . . . . . . . . 15 (((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘1)} × {0})) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (({((2nd ‘(1st𝑇))‘1)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
527 un23 4098 . . . . . . . . . . . . . . 15 (((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘1)} × {0})) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) = (((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {0}))
528526, 527eqtr3i 2826 . . . . . . . . . . . . . 14 ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (({((2nd ‘(1st𝑇))‘1)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) = (((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {0}))
529525, 528eqtrdi 2852 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})) = (((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {0})))
530529fveq1d 6651 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {0}))‘𝑛))
531530ad2antrr 725 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘1)} × {0}))‘𝑛))
532354, 372, 5313eqtr4d 2846 . . . . . . . . . 10 ((((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1)) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))
533 snssi 4704 . . . . . . . . . . . . . . 15 (1 ∈ ℂ → {1} ⊆ ℂ)
534141, 533ax-mp 5 . . . . . . . . . . . . . 14 {1} ⊆ ℂ
535 0cn 10626 . . . . . . . . . . . . . . 15 0 ∈ ℂ
536 snssi 4704 . . . . . . . . . . . . . . 15 (0 ∈ ℂ → {0} ⊆ ℂ)
537535, 536ax-mp 5 . . . . . . . . . . . . . 14 {0} ⊆ ℂ
538534, 537unssi 4115 . . . . . . . . . . . . 13 ({1} ∪ {0}) ⊆ ℂ
53932fconst 6543 . . . . . . . . . . . . . . . . 17 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦))⟶{1}
54035fconst 6543 . . . . . . . . . . . . . . . . 17 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))⟶{0}
541539, 540pm3.2i 474 . . . . . . . . . . . . . . . 16 (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦))⟶{1} ∧ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))⟶{0})
542 fun 6518 . . . . . . . . . . . . . . . 16 (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦))⟶{1} ∧ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))⟶{0}) ∧ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))) = ∅) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})):((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)))⟶({1} ∪ {0}))
543541, 243, 542sylancr 590 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})):((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)))⟶({1} ∪ {0}))
544 imaundi 5979 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))) = ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)))
54565adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ (ℤ‘1))
546 fzsplit2 12931 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑦)) → (1...𝑁) = ((1...𝑦) ∪ ((𝑦 + 1)...𝑁)))
547545, 378, 546syl2anc 587 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) = ((1...𝑦) ∪ ((𝑦 + 1)...𝑁)))
548547imaeq2d 5900 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑁)) = (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))))
549 f1ofo 6601 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–onto→(1...𝑁))
550 foima 6574 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–onto→(1...𝑁) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑁)) = (1...𝑁))
551230, 549, 5503syl 18 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑁)) = (1...𝑁))
552551adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑁)) = (1...𝑁))
553548, 552eqtr3d 2838 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))) = (1...𝑁))
554544, 553syl5eqr 2850 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))) = (1...𝑁))
555554feq2d 6477 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})):((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})))
556543, 555mpbid 235 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
557556ffvelrnda 6832 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) ∈ ({1} ∪ {0}))
558538, 557sseldi 3916 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) ∈ ℂ)
559558addid2d 10834 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (0 + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)) = ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))
560559adantr 484 . . . . . . . . . 10 ((((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1)) → (0 + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)) = ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))
561532, 560eqtr4d 2839 . . . . . . . . 9 ((((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1)) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (0 + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)))
56296, 98, 289, 561ifbothda 4465 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)))
563562oveq2d 7155 . . . . . . 7 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (((1st ‘(1st𝑇))‘𝑛) + (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛)) = (((1st ‘(1st𝑇))‘𝑛) + (if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))))
564 elmapi 8415 . . . . . . . . . . . . 13 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
56528, 564syl 17 . . . . . . . . . . . 12 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
566565ffvelrnda 6832 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ (0..^𝐾))
567 elfzonn0 13081 . . . . . . . . . . 11 (((1st ‘(1st𝑇))‘𝑛) ∈ (0..^𝐾) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℕ0)
568566, 567syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℕ0)
569568nn0cnd 11949 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℂ)
570569adantlr 714 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℂ)
571141, 535ifcli 4474 . . . . . . . . 9 if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) ∈ ℂ
572571a1i 11 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) ∈ ℂ)
573570, 572, 558addassd 10656 . . . . . . 7 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0)) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)) = (((1st ‘(1st𝑇))‘𝑛) + (if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))))
574563, 573eqtr4d 2839 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (((1st ‘(1st𝑇))‘𝑛) + (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛)) = ((((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0)) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)))
575574mpteq2dva 5128 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛))) = (𝑛 ∈ (1...𝑁) ↦ ((((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0)) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))))
57694, 575eqtrd 2836 . . . 4 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) = (𝑛 ∈ (1...𝑁) ↦ ((((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0)) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))))
577 poimirlem18.4 . . . . . . . . . 10 (𝜑 → (2nd𝑇) = 0)
578577adantr 484 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (2nd𝑇) = 0)
579 elfzle1 12909 . . . . . . . . . 10 (𝑦 ∈ (0...(𝑁 − 1)) → 0 ≤ 𝑦)
580579adantl 485 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 0 ≤ 𝑦)
581578, 580eqbrtrd 5055 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (2nd𝑇) ≤ 𝑦)
582 0re 10636 . . . . . . . . . 10 0 ∈ ℝ
583577, 582eqeltrdi 2901 . . . . . . . . 9 (𝜑 → (2nd𝑇) ∈ ℝ)
584 lenlt 10712 . . . . . . . . 9 (((2nd𝑇) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((2nd𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd𝑇)))
585583, 236, 584syl2an 598 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd𝑇)))
586581, 585mpbid 235 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ¬ 𝑦 < (2nd𝑇))
587586iffalsed 4439 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = (𝑦 + 1))
588587csbeq1d 3835 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑦 + 1) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
589 ovex 7172 . . . . . 6 (𝑦 + 1) ∈ V
590 oveq2 7147 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → (1...𝑗) = (1...(𝑦 + 1)))
591590imaeq2d 5900 . . . . . . . . 9 (𝑗 = (𝑦 + 1) → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
592591xpeq1d 5552 . . . . . . . 8 (𝑗 = (𝑦 + 1) → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}))
593 oveq1 7146 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (𝑗 + 1) = ((𝑦 + 1) + 1))
594593oveq1d 7154 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → ((𝑗 + 1)...𝑁) = (((𝑦 + 1) + 1)...𝑁))
595594imaeq2d 5900 . . . . . . . . 9 (𝑗 = (𝑦 + 1) → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
596595xpeq1d 5552 . . . . . . . 8 (𝑗 = (𝑦 + 1) → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
597592, 596uneq12d 4094 . . . . . . 7 (𝑗 = (𝑦 + 1) → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
598597oveq2d 7155 . . . . . 6 (𝑗 = (𝑦 + 1) → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
599589, 598csbie 3866 . . . . 5 (𝑦 + 1) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
600588, 599eqtrdi 2852 . . . 4 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
601 ovexd 7174 . . . . 5 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0)) ∈ V)
602 fvexd 6664 . . . . 5 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) ∈ V)
603 eqidd 2802 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))) = (𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))))
604556ffnd 6492 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (1...𝑁))
605 nfcv 2958 . . . . . . . . . . 11 𝑛(2nd ‘(1st𝑇))
606 nfmpt1 5131 . . . . . . . . . . 11 𝑛(𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))
607605, 606nfco 5704 . . . . . . . . . 10 𝑛((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))
608 nfcv 2958 . . . . . . . . . 10 𝑛(1...𝑦)
609607, 608nfima 5908 . . . . . . . . 9 𝑛(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦))
610 nfcv 2958 . . . . . . . . 9 𝑛{1}
611609, 610nfxp 5556 . . . . . . . 8 𝑛((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1})
612 nfcv 2958 . . . . . . . . . 10 𝑛((𝑦 + 1)...𝑁)
613607, 612nfima 5908 . . . . . . . . 9 𝑛(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))
614 nfcv 2958 . . . . . . . . 9 𝑛{0}
615613, 614nfxp 5556 . . . . . . . 8 𝑛((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})
616611, 615nfun 4095 . . . . . . 7 𝑛(((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))
617616dffn5f 6715 . . . . . 6 ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (1...𝑁) ↔ (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})) = (𝑛 ∈ (1...𝑁) ↦ ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)))
618604, 617sylib 221 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})) = (𝑛 ∈ (1...𝑁) ↦ ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)))
61990, 601, 602, 603, 618offval2 7410 . . . 4 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))) ∘f + (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))) = (𝑛 ∈ (1...𝑁) ↦ ((((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0)) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))))
620576, 600, 6193eqtr4rd 2847 . . 3 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))) ∘f + (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
621620mpteq2dva 5128 . 2 (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))) ∘f + (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
62221, 621eqtr4d 2839 1 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))) ∘f + (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2112  {cab 2779   ≠ wne 2990  ∀wral 3109  ∃wrex 3110  ∃!wreu 3111  {crab 3113  Vcvv 3444  ⦋csb 3831   ∖ cdif 3881   ∪ cun 3882   ∩ cin 3883   ⊆ wss 3884  ∅c0 4246  ifcif 4428  {csn 4528  ⟨cop 4534   class class class wbr 5033   ↦ cmpt 5113   × cxp 5521  ◡ccnv 5522  ran crn 5524   ↾ cres 5525   “ cima 5526   ∘ ccom 5527  Fun wfun 6322   Fn wfn 6323  ⟶wf 6324  –onto→wfo 6326  –1-1-onto→wf1o 6327  ‘cfv 6328  (class class class)co 7139   ∘f cof 7391  1st c1st 7673  2nd c2nd 7674   ↑m cmap 8393  ℂcc 10528  ℝcr 10529  0cc0 10530  1c1 10531   + caddc 10533   < clt 10668   ≤ cle 10669   − cmin 10863  ℕcn 11629  ℕ0cn0 11889  ℤcz 11973  ℤ≥cuz 12235  ...cfz 12889  ..^cfzo 13032 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-map 8395  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-nn 11630  df-n0 11890  df-z 11974  df-uz 12236  df-fz 12890  df-fzo 13033 This theorem is referenced by:  poimirlem17  35067
 Copyright terms: Public domain W3C validator