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

Theorem poimirlem16 33555
 Description: Lemma for poimir 33572 establishing the vertices of the simplex of poimirlem17 33556. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimirlem22.s 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
poimirlem22.1 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (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))) ∘𝑓 + (((((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 6229 . . . . . . . . . . 11 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
32breq2d 4697 . . . . . . . . . 10 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
43ifbid 4141 . . . . . . . . 9 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
54csbeq1d 3573 . . . . . . . 8 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
6 fveq2 6229 . . . . . . . . . . 11 (𝑡 = 𝑇 → (1st𝑡) = (1st𝑇))
76fveq2d 6233 . . . . . . . . . 10 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
86fveq2d 6233 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
98imaeq1d 5500 . . . . . . . . . . . 12 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
109xpeq1d 5172 . . . . . . . . . . 11 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
118imaeq1d 5500 . . . . . . . . . . . 12 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
1211xpeq1d 5172 . . . . . . . . . . 11 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
1310, 12uneq12d 3801 . . . . . . . . . 10 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
147, 13oveq12d 6708 . . . . . . . . 9 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
1514csbeq2dv 4025 . . . . . . . 8 (𝑡 = 𝑇if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
165, 15eqtrd 2685 . . . . . . 7 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
1716mpteq2dv 4778 . . . . . 6 (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
1817eqeq2d 2661 . . . . 5 (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
19 poimirlem22.s . . . . 5 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
2018, 19elrab2 3399 . . . 4 (𝑇𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
2120simprbi 479 . . 3 (𝑇𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
221, 21syl 17 . 2 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
23 elrabi 3391 . . . . . . . . . . . 12 (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
2423, 19eleq2s 2748 . . . . . . . . . . 11 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
251, 24syl 17 . . . . . . . . . 10 (𝜑𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
26 xp1st 7242 . . . . . . . . . 10 (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
2725, 26syl 17 . . . . . . . . 9 (𝜑 → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
28 xp1st 7242 . . . . . . . . 9 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
2927, 28syl 17 . . . . . . . 8 (𝜑 → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
30 elmapfn 7922 . . . . . . . 8 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑇)) Fn (1...𝑁))
3129, 30syl 17 . . . . . . 7 (𝜑 → (1st ‘(1st𝑇)) Fn (1...𝑁))
3231adantr 480 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1st ‘(1st𝑇)) Fn (1...𝑁))
33 1ex 10073 . . . . . . . . . 10 1 ∈ V
34 fnconstg 6131 . . . . . . . . . 10 (1 ∈ V → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
3533, 34ax-mp 5 . . . . . . . . 9 (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1)))
36 c0ex 10072 . . . . . . . . . 10 0 ∈ V
37 fnconstg 6131 . . . . . . . . . 10 (0 ∈ V → (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
3836, 37ax-mp 5 . . . . . . . . 9 (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))
3935, 38pm3.2i 470 . . . . . . . 8 ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∧ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
40 xp2nd 7243 . . . . . . . . . . . . 13 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
4127, 40syl 17 . . . . . . . . . . . 12 (𝜑 → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
42 fvex 6239 . . . . . . . . . . . . 13 (2nd ‘(1st𝑇)) ∈ V
43 f1oeq1 6165 . . . . . . . . . . . . 13 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
4442, 43elab 3382 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
4541, 44sylib 208 . . . . . . . . . . 11 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
46 dff1o3 6181 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑇))))
4746simprbi 479 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑇)))
4845, 47syl 17 . . . . . . . . . 10 (𝜑 → Fun (2nd ‘(1st𝑇)))
49 imain 6012 . . . . . . . . . 10 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
5048, 49syl 17 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
51 elfznn0 12471 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ0)
52 nn0p1nn 11370 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ0 → (𝑦 + 1) ∈ ℕ)
5351, 52syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℕ)
5453nnred 11073 . . . . . . . . . . . . 13 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℝ)
5554ltp1d 10992 . . . . . . . . . . . 12 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) < ((𝑦 + 1) + 1))
56 fzdisj 12406 . . . . . . . . . . . 12 ((𝑦 + 1) < ((𝑦 + 1) + 1) → ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
5755, 56syl 17 . . . . . . . . . . 11 (𝑦 ∈ (0...(𝑁 − 1)) → ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
5857imaeq2d 5501 . . . . . . . . . 10 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
59 ima0 5516 . . . . . . . . . 10 ((2nd ‘(1st𝑇)) “ ∅) = ∅
6058, 59syl6eq 2701 . . . . . . . . 9 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ∅)
6150, 60sylan9req 2706 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅)
62 fnun 6035 . . . . . . . 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)...𝑁))))
6339, 61, 62sylancr 696 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
64 imaundi 5580 . . . . . . . . 9 ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
65 nnuz 11761 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
6653, 65syl6eleq 2740 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (ℤ‘1))
67 peano2uz 11779 . . . . . . . . . . . . . 14 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1) + 1) ∈ (ℤ‘1))
6866, 67syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ (ℤ‘1))
6968adantl 481 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1) + 1) ∈ (ℤ‘1))
70 poimir.0 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ)
7170nncnd 11074 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℂ)
72 npcan1 10493 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
7371, 72syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
7473adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
75 elfzuz3 12377 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ𝑦))
76 eluzp1p1 11751 . . . . . . . . . . . . . . 15 ((𝑁 − 1) ∈ (ℤ𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
7775, 76syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
7877adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
7974, 78eqeltrrd 2731 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘(𝑦 + 1)))
80 fzsplit2 12404 . . . . . . . . . . . 12 ((((𝑦 + 1) + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘(𝑦 + 1))) → (1...𝑁) = ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
8169, 79, 80syl2anc 694 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) = ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
8281imaeq2d 5501 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))))
83 f1ofo 6182 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
84 foima 6158 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
8545, 83, 843syl 18 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
8685adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
8782, 86eqtr3d 2687 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (1...𝑁))
8864, 87syl5eqr 2699 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = (1...𝑁))
8988fneq2d 6020 . . . . . . 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...𝑁)))
9063, 89mpbid 222 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
91 ovexd 6720 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) ∈ V)
92 inidm 3855 . . . . . 6 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
93 eqidd 2652 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) = ((1st ‘(1st𝑇))‘𝑛))
94 eqidd 2652 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛))
9532, 90, 91, 91, 92, 93, 94offval 6946 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) = (𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛))))
96 oveq1 6697 . . . . . . . . . 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}))‘𝑛)))
9796eqeq2d 2661 . . . . . . . . 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}))‘𝑛))))
98 oveq1 6697 . . . . . . . . . 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}))‘𝑛)))
9998eqeq2d 2661 . . . . . . . . 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}))‘𝑛))))
100 1p0e1 11171 . . . . . . . . . . . . . 14 (1 + 0) = 1
101100eqcomi 2660 . . . . . . . . . . . . 13 1 = (1 + 0)
102 f1ofn 6176 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
10345, 102syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (2nd ‘(1st𝑇)) Fn (1...𝑁))
104103adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
105 fzss2 12419 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘(𝑦 + 1)) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
10679, 105syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
107 eluzfz1 12386 . . . . . . . . . . . . . . . . . 18 ((𝑦 + 1) ∈ (ℤ‘1) → 1 ∈ (1...(𝑦 + 1)))
10866, 107syl 17 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → 1 ∈ (1...(𝑦 + 1)))
109108adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 1 ∈ (1...(𝑦 + 1)))
110 fnfvima 6536 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ (1...(𝑦 + 1)) ⊆ (1...𝑁) ∧ 1 ∈ (1...(𝑦 + 1))) → ((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
111104, 106, 109, 110syl3anc 1366 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
112 fvun1 6308 . . . . . . . . . . . . . . . 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)))
11335, 38, 112mp3an12 1454 . . . . . . . . . . . . . . 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)))
11461, 111, 113syl2anc 694 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd ‘(1st𝑇))‘1)))
11533fvconst2 6510 . . . . . . . . . . . . . . 15 (((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) → ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd ‘(1st𝑇))‘1)) = 1)
116111, 115syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd ‘(1st𝑇))‘1)) = 1)
117114, 116eqtrd 2685 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = 1)
118 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → 𝑛 ∈ (1...(𝑁 − 1)))
11970nnzd 11519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℤ)
120 peano2zm 11458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
121119, 120syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑁 − 1) ∈ ℤ)
122 1z 11445 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ ℤ
123121, 122jctil 559 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ))
124 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℤ)
125124, 122jctir 560 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ (1...(𝑁 − 1)) → (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
126 fzaddel 12413 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ (1...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1))))
127123, 125, 126syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 ∈ (1...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1))))
128118, 127mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1)))
12973oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 + 1)...𝑁))
130129adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 + 1)...𝑁))
131128, 130eleqtrd 2732 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 + 1) ∈ ((1 + 1)...𝑁))
132131ralrimiva 2995 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑛 + 1) ∈ ((1 + 1)...𝑁))
133 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → 𝑦 ∈ ((1 + 1)...𝑁))
134 peano2z 11456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 ∈ ℤ → (1 + 1) ∈ ℤ)
135122, 134ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (1 + 1) ∈ ℤ
136119, 135jctil 559 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ))
137 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ((1 + 1)...𝑁) → 𝑦 ∈ ℤ)
138137, 122jctir 560 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ((1 + 1)...𝑁) → (𝑦 ∈ ℤ ∧ 1 ∈ ℤ))
139 fzsubel 12415 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑦 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑦 ∈ ((1 + 1)...𝑁) ↔ (𝑦 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
140136, 138, 139syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 ∈ ((1 + 1)...𝑁) ↔ (𝑦 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
141133, 140mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1)))
142 ax-1cn 10032 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ ℂ
143142, 142pncan3oi 10335 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 + 1) − 1) = 1
144143oveq1i 6700 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 + 1) − 1)...(𝑁 − 1)) = (1...(𝑁 − 1))
145141, 144syl6eleq 2740 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 − 1) ∈ (1...(𝑁 − 1)))
146137zcnd 11521 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ((1 + 1)...𝑁) → 𝑦 ∈ ℂ)
147 elfznn 12408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℕ)
148147nncnd 11074 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℂ)
149 subadd2 10323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑦 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑦 − 1) = 𝑛 ↔ (𝑛 + 1) = 𝑦))
150142, 149mp3an2 1452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑦 − 1) = 𝑛 ↔ (𝑛 + 1) = 𝑦))
151150bicomd 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑛 + 1) = 𝑦 ↔ (𝑦 − 1) = 𝑛))
152 eqcom 2658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑛 + 1) = 𝑦𝑦 = (𝑛 + 1))
153 eqcom 2658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦 − 1) = 𝑛𝑛 = (𝑦 − 1))
154151, 152, 1533bitr3g 302 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1)))
155146, 148, 154syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ((1 + 1)...𝑁) ∧ 𝑛 ∈ (1...(𝑁 − 1))) → (𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1)))
156155ralrimiva 2995 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((1 + 1)...𝑁) → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1)))
157156adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1)))
158 reu6i 3430 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑦 − 1) ∈ (1...(𝑁 − 1)) ∧ ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) → ∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1))
159145, 157, 158syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → ∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1))
160159ralrimiva 2995 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑦 ∈ ((1 + 1)...𝑁)∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1))
161 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) = (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1))
162161f1ompt 6422 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 + 1)...𝑁) ↔ (∀𝑛 ∈ (1...(𝑁 − 1))(𝑛 + 1) ∈ ((1 + 1)...𝑁) ∧ ∀𝑦 ∈ ((1 + 1)...𝑁)∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1)))
163132, 160, 162sylanbrc 699 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 + 1)...𝑁))
164 f1osng 6215 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ 1 ∈ V) → {⟨𝑁, 1⟩}:{𝑁}–1-1-onto→{1})
16570, 33, 164sylancl 695 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {⟨𝑁, 1⟩}:{𝑁}–1-1-onto→{1})
16670nnred 11073 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑁 ∈ ℝ)
167166ltm1d 10994 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑁 − 1) < 𝑁)
168121zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑁 − 1) ∈ ℝ)
169168, 166ltnled 10222 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
170167, 169mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
171 elfzle2 12383 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
172170, 171nsyl 135 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
173 disjsn 4278 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1)))
174172, 173sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅)
175 1re 10077 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 ∈ ℝ
176175ltp1i 10965 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 < (1 + 1)
177175, 175readdcli 10091 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (1 + 1) ∈ ℝ
178175, 177ltnlei 10196 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 < (1 + 1) ↔ ¬ (1 + 1) ≤ 1)
179176, 178mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . . 25 ¬ (1 + 1) ≤ 1
180 elfzle1 12382 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ((1 + 1)...𝑁) → (1 + 1) ≤ 1)
181179, 180mto 188 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ 1 ∈ ((1 + 1)...𝑁)
182 disjsn 4278 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((1 + 1)...𝑁) ∩ {1}) = ∅ ↔ ¬ 1 ∈ ((1 + 1)...𝑁))
183181, 182mpbir 221 . . . . . . . . . . . . . . . . . . . . . . 23 (((1 + 1)...𝑁) ∩ {1}) = ∅
184 f1oun 6194 . . . . . . . . . . . . . . . . . . . . . . 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}))
185183, 184mpanr2 720 . . . . . . . . . . . . . . . . . . . . . 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}))
186163, 165, 174, 185syl21anc 1365 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}):((1...(𝑁 − 1)) ∪ {𝑁})–1-1-onto→(((1 + 1)...𝑁) ∪ {1}))
187 ssv 3658 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℕ ⊆ V
188187, 70sseldi 3634 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑁 ∈ V)
18933a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ∈ V)
19070, 65syl6eleq 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑁 ∈ (ℤ‘1))
19173, 190eqeltrd 2730 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘1))
192 uzid 11740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
193 peano2uz 11779 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
194121, 192, 1933syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
19573, 194eqeltrrd 2731 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
196 fzsplit2 12404 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
197191, 195, 196syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
19873oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
199 fzsn 12421 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
200119, 199syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑁...𝑁) = {𝑁})
201198, 200eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
202201uneq2d 3800 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁}))
203197, 202eqtr2d 2686 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁))
204 iftrue 4125 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑁 → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = 1)
205204adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑛 = 𝑁) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = 1)
206188, 189, 203, 205fmptapd 6478 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∪ {⟨𝑁, 1⟩}) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))
207 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑁 → (𝑛 ∈ (1...(𝑁 − 1)) ↔ 𝑁 ∈ (1...(𝑁 − 1))))
208207notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑁 → (¬ 𝑛 ∈ (1...(𝑁 − 1)) ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1))))
209172, 208syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑛 = 𝑁 → ¬ 𝑛 ∈ (1...(𝑁 − 1))))
210209necon2ad 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛𝑁))
211210imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → 𝑛𝑁)
212 ifnefalse 4131 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛𝑁 → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1))
213211, 212syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1))
214213mpteq2dva 4777 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)))
215214uneq1d 3799 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∪ {⟨𝑁, 1⟩}) = ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}))
216206, 215eqtr3d 2687 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}))
217197, 202eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁}))
218 uzid 11740 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℤ → 1 ∈ (ℤ‘1))
219 peano2uz 11779 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ (ℤ‘1) → (1 + 1) ∈ (ℤ‘1))
220122, 218, 219mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 + 1) ∈ (ℤ‘1)
221 fzsplit2 12404 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘1)) → (1...𝑁) = ((1...1) ∪ ((1 + 1)...𝑁)))
222220, 190, 221sylancr 696 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑁) = ((1...1) ∪ ((1 + 1)...𝑁)))
223 fzsn 12421 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 ∈ ℤ → (1...1) = {1})
224122, 223ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1...1) = {1}
225224uneq1i 3796 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1...1) ∪ ((1 + 1)...𝑁)) = ({1} ∪ ((1 + 1)...𝑁))
226225equncomi 3792 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...1) ∪ ((1 + 1)...𝑁)) = (((1 + 1)...𝑁) ∪ {1})
227222, 226syl6eq 2701 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1...𝑁) = (((1 + 1)...𝑁) ∪ {1}))
228216, 217, 227f1oeq123d 6171 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}):((1...(𝑁 − 1)) ∪ {𝑁})–1-1-onto→(((1 + 1)...𝑁) ∪ {1})))
229186, 228mpbird 247 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁))
230 f1oco 6197 . . . . . . . . . . . . . . . . . . . 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...𝑁))
23145, 229, 230syl2anc 694 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁))
232 dff1o3 6181 . . . . . . . . . . . . . . . . . . . 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))))))
233232simprbi 479 . . . . . . . . . . . . . . . . . . 19 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))))
234231, 233syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → Fun ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))))
235 imain 6012 . . . . . . . . . . . . . . . . . 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)...𝑁))))
236234, 235syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))))
23751nn0red 11390 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
238237ltp1d 10992 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 < (𝑦 + 1))
239 fzdisj 12406 . . . . . . . . . . . . . . . . . . . 20 (𝑦 < (𝑦 + 1) → ((1...𝑦) ∩ ((𝑦 + 1)...𝑁)) = ∅)
240238, 239syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → ((1...𝑦) ∩ ((𝑦 + 1)...𝑁)) = ∅)
241240imaeq2d 5501 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0...(𝑁 − 1)) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ∅))
242 ima0 5516 . . . . . . . . . . . . . . . . . 18 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ∅) = ∅
243241, 242syl6eq 2701 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = ∅)
244236, 243sylan9req 2706 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))) = ∅)
245 imassrn 5512 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)) ⊆ ran (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))
246 f1of 6175 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁) → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)⟶(1...𝑁))
247 frn 6091 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)⟶(1...𝑁) → ran (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ⊆ (1...𝑁))
248229, 246, 2473syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ran (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ⊆ (1...𝑁))
249245, 248syl5ss 3647 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)) ⊆ (1...𝑁))
250249adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)) ⊆ (1...𝑁))
251 elfz1end 12409 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
25270, 251sylib 208 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑁 ∈ (1...𝑁))
253 eqid 2651 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))
254204, 253, 33fvmpt 6321 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (1...𝑁) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) = 1)
255252, 254syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) = 1)
256255adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) = 1)
257 f1ofn 6176 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁) → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁))
258229, 257syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁))
259258adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁))
260 fzss1 12418 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
26166, 260syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
262261adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
263 eluzfz2 12387 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (ℤ‘(𝑦 + 1)) → 𝑁 ∈ ((𝑦 + 1)...𝑁))
26479, 263syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑦 + 1)...𝑁))
265 fnfvima 6536 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁) ∧ ((𝑦 + 1)...𝑁) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑦 + 1)...𝑁)) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)))
266259, 262, 264, 265syl3anc 1366 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)))
267256, 266eqeltrrd 2731 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 1 ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)))
268 fnfvima 6536 . . . . . . . . . . . . . . . . . 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)...𝑁))))
269104, 250, 267, 268syl3anc 1366 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁))))
270 imaco 5678 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)))
271269, 270syl6eleqr 2741 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇))‘1) ∈ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)))
272 fnconstg 6131 . . . . . . . . . . . . . . . . . 18 (1 ∈ V → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)))
27333, 272ax-mp 5 . . . . . . . . . . . . . . . . 17 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦))
274 fnconstg 6131 . . . . . . . . . . . . . . . . . 18 (0 ∈ V → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)))
27536, 274ax-mp 5 . . . . . . . . . . . . . . . . 17 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))
276 fvun2 6309 . . . . . . . . . . . . . . . . 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)))
277273, 275, 276mp3an12 1454 . . . . . . . . . . . . . . . 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)))
278244, 271, 277syl2anc 694 . . . . . . . . . . . . . . 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)))
27936fvconst2 6510 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇))‘1) ∈ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘1)) = 0)
280271, 279syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘1)) = 0)
281278, 280eqtrd 2685 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = 0)
282281oveq2d 6706 . . . . . . . . . . . . 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))
283101, 117, 2823eqtr4a 2711 . . . . . . . . . . . 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))))
284 fveq2 6229 . . . . . . . . . . . . 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)))
285 fveq2 6229 . . . . . . . . . . . . . 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)))
286285oveq2d 6706 . . . . . . . . . . . . 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))))
287284, 286eqeq12d 2666 . . . . . . . . . . . 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)))))
288283, 287syl5ibrcom 237 . . . . . . . . . . 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}))‘𝑛))))
289288imp 444 . . . . . . . . . 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}))‘𝑛)))
290289adantlr 751 . . . . . . . . 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}))‘𝑛)))
291 eldifsn 4350 . . . . . . . . . . . . . 14 (𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ↔ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘1)))
292 df-ne 2824 . . . . . . . . . . . . . . 15 (𝑛 ≠ ((2nd ‘(1st𝑇))‘1) ↔ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1))
293292anbi2i 730 . . . . . . . . . . . . . 14 ((𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘1)) ↔ (𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1)))
294291, 293bitri 264 . . . . . . . . . . . . 13 (𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ↔ (𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1)))
295 fnconstg 6131 . . . . . . . . . . . . . . . . . 18 (1 ∈ V → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
29633, 295ax-mp 5 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1)))
297296, 38pm3.2i 470 . . . . . . . . . . . . . . . 16 ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∧ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
298 imain 6012 . . . . . . . . . . . . . . . . . 18 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
29948, 298syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
300 fzdisj 12406 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 + 1) < ((𝑦 + 1) + 1) → (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
30155, 300syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
302301imaeq2d 5501 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
303302, 59syl6eq 2701 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ∅)
304299, 303sylan9req 2706 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅)
305 fnun 6035 . . . . . . . . . . . . . . . 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)...𝑁))))
306297, 304, 305sylancr 696 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
307 imaundi 5580 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
308 fzpred 12427 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ‘1) → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁)))
309190, 308syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁)))
310 uncom 3790 . . . . . . . . . . . . . . . . . . . . . . . 24 ({1} ∪ ((1 + 1)...𝑁)) = (((1 + 1)...𝑁) ∪ {1})
311309, 310syl6eq 2701 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑁) = (((1 + 1)...𝑁) ∪ {1}))
312311difeq1d 3760 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...𝑁) ∖ {1}) = ((((1 + 1)...𝑁) ∪ {1}) ∖ {1}))
313 difun2 4081 . . . . . . . . . . . . . . . . . . . . . . 23 ((((1 + 1)...𝑁) ∪ {1}) ∖ {1}) = (((1 + 1)...𝑁) ∖ {1})
314 disj3 4054 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((1 + 1)...𝑁) ∩ {1}) = ∅ ↔ ((1 + 1)...𝑁) = (((1 + 1)...𝑁) ∖ {1}))
315183, 314mpbi 220 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 + 1)...𝑁) = (((1 + 1)...𝑁) ∖ {1})
316313, 315eqtr4i 2676 . . . . . . . . . . . . . . . . . . . . . 22 ((((1 + 1)...𝑁) ∪ {1}) ∖ {1}) = ((1 + 1)...𝑁)
317312, 316syl6eq 2701 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((1...𝑁) ∖ {1}) = ((1 + 1)...𝑁))
318317adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1...𝑁) ∖ {1}) = ((1 + 1)...𝑁))
319 eluzp1p1 11751 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1) + 1) ∈ (ℤ‘(1 + 1)))
32066, 319syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ (ℤ‘(1 + 1)))
321320adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1) + 1) ∈ (ℤ‘(1 + 1)))
322 fzsplit2 12404 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 + 1) + 1) ∈ (ℤ‘(1 + 1)) ∧ 𝑁 ∈ (ℤ‘(𝑦 + 1))) → ((1 + 1)...𝑁) = (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
323321, 79, 322syl2anc 694 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1 + 1)...𝑁) = (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
324318, 323eqtrd 2685 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1...𝑁) ∖ {1}) = (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
325324imaeq2d 5501 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))))
326 imadif 6011 . . . . . . . . . . . . . . . . . . . . 21 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {1})))
32748, 326syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {1})))
328 eluzfz1 12386 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ‘1) → 1 ∈ (1...𝑁))
329190, 328syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 ∈ (1...𝑁))
330 fnsnfv 6297 . . . . . . . . . . . . . . . . . . . . . . 23 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ 1 ∈ (1...𝑁)) → {((2nd ‘(1st𝑇))‘1)} = ((2nd ‘(1st𝑇)) “ {1}))
331103, 329, 330syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {((2nd ‘(1st𝑇))‘1)} = ((2nd ‘(1st𝑇)) “ {1}))
332331eqcomd 2657 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((2nd ‘(1st𝑇)) “ {1}) = {((2nd ‘(1st𝑇))‘1)})
33385, 332difeq12d 3762 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {1})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
334327, 333eqtrd 2685 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
335334adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
336325, 335eqtr3d 2687 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
337307, 336syl5eqr 2699 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
338337fneq2d 6020 . . . . . . . . . . . . . . 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)})))
339306, 338mpbid 222 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
340 incom 3838 . . . . . . . . . . . . . . . 16 (((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∩ {((2nd ‘(1st𝑇))‘1)}) = ({((2nd ‘(1st𝑇))‘1)} ∩ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
341 disjdif 4073 . . . . . . . . . . . . . . . 16 ({((2nd ‘(1st𝑇))‘1)} ∩ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)})) = ∅
342340, 341eqtri 2673 . . . . . . . . . . . . . . 15 (((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∩ {((2nd ‘(1st𝑇))‘1)}) = ∅
343 fnconstg 6131 . . . . . . . . . . . . . . . . . 18 (1 ∈ V → ({((2nd ‘(1st𝑇))‘1)} × {1}) Fn {((2nd ‘(1st𝑇))‘1)})
34433, 343ax-mp 5 . . . . . . . . . . . . . . . . 17 ({((2nd ‘(1st𝑇))‘1)} × {1}) Fn {((2nd ‘(1st𝑇))‘1)}
345 fvun1 6308 . . . . . . . . . . . . . . . . 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}))‘𝑛))
346344, 345mp3an2 1452 . . . . . . . . . . . . . . . 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}))‘𝑛))
347 fnconstg 6131 . . . . . . . . . . . . . . . . . 18 (0 ∈ V → ({((2nd ‘(1st𝑇))‘1)} × {0}) Fn {((2nd ‘(1st𝑇))‘1)})
34836, 347ax-mp 5 . . . . . . . . . . . . . . . . 17 ({((2nd ‘(1st𝑇))‘1)} × {0}) Fn {((2nd ‘(1st𝑇))‘1)}
349 fvun1 6308 . . . . . . . . . . . . . . . . 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}))‘𝑛))
350348, 349mp3an2 1452 . . . . . . . . . . . . . . . 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}))‘𝑛))
351346, 350eqtr4d 2688 . . . . . . . . . . . . . . 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}))‘𝑛))
352342, 351mpanr1 719 . . . . . . . . . . . . . 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}))‘𝑛))
353339, 352sylan 487 . . . . . . . . . . . . 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}))‘𝑛))
354294, 353sylan2br 492 . . . . . . . . . . . 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}))‘𝑛))
355354anassrs 681 . . . . . . . . . . 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}))‘𝑛))
356 fzpred 12427 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 + 1) ∈ (ℤ‘1) → (1...(𝑦 + 1)) = ({1} ∪ ((1 + 1)...(𝑦 + 1))))
35766, 356syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (0...(𝑁 − 1)) → (1...(𝑦 + 1)) = ({1} ∪ ((1 + 1)...(𝑦 + 1))))
358357imaeq2d 5501 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) = ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))))
359358adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) = ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))))
360331uneq1d 3799 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1)))) = (((2nd ‘(1st𝑇)) “ {1}) ∪ ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1)))))
361 uncom 3790 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) = ({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
362 imaundi 5580 . . . . . . . . . . . . . . . . . . . 20 ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))) = (((2nd ‘(1st𝑇)) “ {1}) ∪ ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
363360, 361, 3623eqtr4g 2710 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) = ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))))
364363adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) = ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))))
365359, 364eqtr4d 2688 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}))
366365xpeq1d 5172 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) = ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) × {1}))
367 xpundir 5206 . . . . . . . . . . . . . . . 16 ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) × {1}) = ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1}))
368366, 367syl6eq 2701 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) = ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1})))
369368uneq1d 3799 . . . . . . . . . . . . . 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})))
370 un23 3805 . . . . . . . . . . . . . 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}))
371369, 370syl6eq 2701 . . . . . . . . . . . . 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})))
372371fveq1d 6231 . . . . . . . . . . . 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}))‘𝑛))
373372ad2antrr 762 . . . . . . . . . . 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}))‘𝑛))
374 imaco 5678 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦)))
375 df-ima 5156 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦)) = ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ (1...𝑦))
376 peano2uz 11779 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 − 1) ∈ (ℤ𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
37775, 376syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
378377adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
37974, 378eqeltrrd 2731 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ𝑦))
380 fzss2 12419 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ𝑦) → (1...𝑦) ⊆ (1...𝑁))
381379, 380syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑦) ⊆ (1...𝑁))
382381resmptd 5487 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ (1...𝑦)) = (𝑛 ∈ (1...𝑦) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))
383172adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
384 fzss2 12419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑁 − 1) ∈ (ℤ𝑦) → (1...𝑦) ⊆ (1...(𝑁 − 1)))
38575, 384syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ (0...(𝑁 − 1)) → (1...𝑦) ⊆ (1...(𝑁 − 1)))
386385adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑦) ⊆ (1...(𝑁 − 1)))
387386sseld 3635 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 ∈ (1...𝑦) → 𝑁 ∈ (1...(𝑁 − 1))))
388383, 387mtod 189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ¬ 𝑁 ∈ (1...𝑦))
389 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑁 → (𝑛 ∈ (1...𝑦) ↔ 𝑁 ∈ (1...𝑦)))
390389notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑁 → (¬ 𝑛 ∈ (1...𝑦) ↔ ¬ 𝑁 ∈ (1...𝑦)))
391388, 390syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 = 𝑁 → ¬ 𝑛 ∈ (1...𝑦)))
392391necon2ad 2838 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑦) → 𝑛𝑁))
393392imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑦)) → 𝑛𝑁)
394393, 212syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑦)) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1))
395394mpteq2dva 4777 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑦) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)))
396382, 395eqtrd 2685 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ (1...𝑦)) = (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)))
397396rneqd 5385 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ (1...𝑦)) = ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)))
398375, 397syl5eq 2697 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦)) = ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)))
399 vex 3234 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 ∈ V
400 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) = (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1))
401400elrnmpt 5404 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ V → (𝑗 ∈ ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) ↔ ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1)))
402399, 401ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) ↔ ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1))
403 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
404403adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℤ)
405 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ (1...𝑦)) → 𝑛 ∈ (1...𝑦))
406122jctl 563 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℤ → (1 ∈ ℤ ∧ 𝑦 ∈ ℤ))
407 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ (1...𝑦) → 𝑛 ∈ ℤ)
408407, 122jctir 560 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ (1...𝑦) → (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
409 fzaddel 12413 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ (1...𝑦) ↔ (𝑛 + 1) ∈ ((1 + 1)...(𝑦 + 1))))
410406, 408, 409syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ (1...𝑦)) → (𝑛 ∈ (1...𝑦) ↔ (𝑛 + 1) ∈ ((1 + 1)...(𝑦 + 1))))
411405, 410mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ (1...𝑦)) → (𝑛 + 1) ∈ ((1 + 1)...(𝑦 + 1)))
412 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = (𝑛 + 1) → (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) ↔ (𝑛 + 1) ∈ ((1 + 1)...(𝑦 + 1))))
413411, 412syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ (1...𝑦)) → (𝑗 = (𝑛 + 1) → 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
414413rexlimdva 3060 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℤ → (∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1) → 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
415 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → 𝑗 ∈ ℤ)
416415zcnd 11521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → 𝑗 ∈ ℂ)
417 npcan1 10493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ ℂ → ((𝑗 − 1) + 1) = 𝑗)
418416, 417syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → ((𝑗 − 1) + 1) = 𝑗)
419418eleq1d 2715 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → (((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1)) ↔ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
420419ibir 257 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → ((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1)))
421420adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → ((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1)))
422 peano2zm 11458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
423415, 422syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → (𝑗 − 1) ∈ ℤ)
424423, 122jctir 560 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → ((𝑗 − 1) ∈ ℤ ∧ 1 ∈ ℤ))
425 fzaddel 12413 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ((𝑗 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝑗 − 1) ∈ (1...𝑦) ↔ ((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1))))
426406, 424, 425syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → ((𝑗 − 1) ∈ (1...𝑦) ↔ ((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1))))
427421, 426mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → (𝑗 − 1) ∈ (1...𝑦))
428416adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → 𝑗 ∈ ℂ)
429417eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ ℂ → 𝑗 = ((𝑗 − 1) + 1))
430428, 429syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → 𝑗 = ((𝑗 − 1) + 1))
431 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑗 − 1) → (𝑛 + 1) = ((𝑗 − 1) + 1))
432431eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑗 − 1) → (𝑗 = (𝑛 + 1) ↔ 𝑗 = ((𝑗 − 1) + 1)))
433432rspcev 3340 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑗 − 1) ∈ (1...𝑦) ∧ 𝑗 = ((𝑗 − 1) + 1)) → ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1))
434427, 430, 433syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1))
435434ex 449 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℤ → (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1)))
436414, 435impbid 202 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℤ → (∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1) ↔ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
437404, 436syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1) ↔ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
438402, 437syl5bb 272 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑗 ∈ ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) ↔ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
439438eqrdv 2649 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) = ((1 + 1)...(𝑦 + 1)))
440398, 439eqtrd 2685 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦)) = ((1 + 1)...(𝑦 + 1)))
441440imaeq2d 5501 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦))) = ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
442374, 441syl5eq 2697 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) = ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
443442xpeq1d 5172 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}))
444 imaundi 5580 . . . . . . . . . . . . . . . . . . 19 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1)))) = ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ {𝑁}) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...(𝑁 − 1))))
445 imaco 5678 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ {𝑁}) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁}))
446 imaco 5678 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...(𝑁 − 1))) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))))
447445, 446uneq12i 3798 . . . . . . . . . . . . . . . . . . 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)))))
448444, 447eqtri 2673 . . . . . . . . . . . . . . . . . 18 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1)))) = (((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})) ∪ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1)))))
449195adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
450 fzsplit2 12404 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)) ∧ 𝑁 ∈ (ℤ‘(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
45178, 449, 450syl2anc 694 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
452201uneq2d 3800 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}))
453452adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}))
454451, 453eqtrd 2685 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}))
455 uncom 3790 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}) = ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1)))
456454, 455syl6eq 2701 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1))))
457456imaeq2d 5501 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) = (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1)))))
458255sneqd 4222 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁)} = {1})
459 fnsnfv 6297 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → {((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁)} = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁}))
460258, 252, 459syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁)} = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁}))
461458, 460eqtr3d 2687 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {1} = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁}))
462461imaeq2d 5501 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((2nd ‘(1st𝑇)) “ {1}) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})))
463331, 462eqtrd 2685 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {((2nd ‘(1st𝑇))‘1)} = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})))
464463adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → {((2nd ‘(1st𝑇))‘1)} = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})))
465 df-ima 5156 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))) = ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ ((𝑦 + 1)...(𝑁 − 1)))
466 fzss1 12418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1)...(𝑁 − 1)) ⊆ (1...(𝑁 − 1)))
46766, 466syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...(𝑁 − 1)) ⊆ (1...(𝑁 − 1)))
468 fzss2 12419 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
469195, 468syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
470467, 469sylan9ssr 3650 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...(𝑁 − 1)) ⊆ (1...𝑁))
471470resmptd 5487 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ ((𝑦 + 1)...(𝑁 − 1))) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))
472 elfzle2 12383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑁 ∈ ((𝑦 + 1)...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
473170, 472nsyl 135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ¬ 𝑁 ∈ ((𝑦 + 1)...(𝑁 − 1)))
474 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑁 → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ 𝑁 ∈ ((𝑦 + 1)...(𝑁 − 1))))
475474notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑁 → (¬ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ ¬ 𝑁 ∈ ((𝑦 + 1)...(𝑁 − 1))))
476473, 475syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝑛 = 𝑁 → ¬ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))))
477476con2d 129 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) → ¬ 𝑛 = 𝑁))
478477imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → ¬ 𝑛 = 𝑁)
479478iffalsed 4130 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1))
480479mpteq2dva 4777 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
481480adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
482471, 481eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ ((𝑦 + 1)...(𝑁 − 1))) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
483482rneqd 5385 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ ((𝑦 + 1)...(𝑁 − 1))) = ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
484465, 483syl5eq 2697 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))) = ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
485 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → 𝑗 ∈ ℤ)
486485zcnd 11521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → 𝑗 ∈ ℂ)
487486, 417syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → ((𝑗 − 1) + 1) = 𝑗)
488487eleq1d 2715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → (((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) ↔ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
489488ibir 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → ((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)))
490489adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → ((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)))
49153nnzd 11519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℤ)
492121, 491anim12ci 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1) ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ))
493485, 422syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → (𝑗 − 1) ∈ ℤ)
494493, 122jctir 560 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → ((𝑗 − 1) ∈ ℤ ∧ 1 ∈ ℤ))
495 fzaddel 12413 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑦 + 1) ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) ∧ ((𝑗 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝑗 − 1) ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ ((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
496492, 494, 495syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → ((𝑗 − 1) ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ ((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
497490, 496mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → (𝑗 − 1) ∈ ((𝑦 + 1)...(𝑁 − 1)))
498486, 429syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → 𝑗 = ((𝑗 − 1) + 1))
499498adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → 𝑗 = ((𝑗 − 1) + 1))
500432rspcev 3340 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑗 − 1) ∈ ((𝑦 + 1)...(𝑁 − 1)) ∧ 𝑗 = ((𝑗 − 1) + 1)) → ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1))
501497, 499, 500syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1))
502501ex 449 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1)))
503 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)))
504 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) → 𝑛 ∈ ℤ)
505504, 122jctir 560 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) → (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
506 fzaddel 12413 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑦 + 1) ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
507492, 505, 506syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
508503, 507mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → (𝑛 + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)))
509 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = (𝑛 + 1) → (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) ↔ (𝑛 + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
510508, 509syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → (𝑗 = (𝑛 + 1) → 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
511510rexlimdva 3060 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1) → 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
512502, 511impbid 202 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) ↔ ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1)))
513 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1))
514513elrnmpt 5404 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ V → (𝑗 ∈ ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)) ↔ ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1)))
515399, 514ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)) ↔ ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1))
516512, 515syl6bbr 278 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) ↔ 𝑗 ∈ ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1))))
517516eqrdv 2649 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) = ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
51873oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) = (((𝑦 + 1) + 1)...𝑁))
519518adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) = (((𝑦 + 1) + 1)...𝑁))
520484, 517, 5193eqtr2rd 2692 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1) + 1)...𝑁) = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))))
521520imaeq2d 5501 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1)))))
522464, 521uneq12d 3801 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})) ∪ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))))))
523448, 457, 5223eqtr4a 2711 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) = ({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
524523xpeq1d 5172 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}) = (({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) × {0}))
525 xpundir 5206 . . . . . . . . . . . . . . . 16 (({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) × {0}) = (({((2nd ‘(1st𝑇))‘1)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
526524, 525syl6eq 2701 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}) = (({((2nd ‘(1st𝑇))‘1)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
527443, 526uneq12d 3801 . . . . . . . . . . . . . 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}))))
528 unass 3803 . . . . . . . . . . . . . . 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})))
529 un23 3805 . . . . . . . . . . . . . . 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}))
530528, 529eqtr3i 2675 . . . . . . . . . . . . . 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}))
531527, 530syl6eq 2701 . . . . . . . . . . . . 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})))
532531fveq1d 6231 . . . . . . . . . . . 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}))‘𝑛))
533532ad2antrr 762 . . . . . . . . . . 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}))‘𝑛))
534355, 373, 5333eqtr4d 2695 . . . . . . . . . 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}))‘𝑛))
535 snssi 4371 . . . . . . . . . . . . . . 15 (1 ∈ ℂ → {1} ⊆ ℂ)
536142, 535ax-mp 5 . . . . . . . . . . . . . 14 {1} ⊆ ℂ
537 0cn 10070 . . . . . . . . . . . . . . 15 0 ∈ ℂ
538 snssi 4371 . . . . . . . . . . . . . . 15 (0 ∈ ℂ → {0} ⊆ ℂ)
539537, 538ax-mp 5 . . . . . . . . . . . . . 14 {0} ⊆ ℂ
540536, 539unssi 3821 . . . . . . . . . . . . 13 ({1} ∪ {0}) ⊆ ℂ
54133fconst 6129 . . . . . . . . . . . . . . . . 17 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦))⟶{1}
54236fconst 6129 . . . . . . . . . . . . . . . . 17 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))⟶{0}
543541, 542pm3.2i 470 . . . . . . . . . . . . . . . 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})
544 fun 6104 . . . . . . . . . . . . . . . 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}))
545543, 244, 544sylancr 696 . . . . . . . . . . . . . . 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}))
546 imaundi 5580 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))) = ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)))
54766adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ (ℤ‘1))
548 fzsplit2 12404 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑦)) → (1...𝑁) = ((1...𝑦) ∪ ((𝑦 + 1)...𝑁)))
549547, 379, 548syl2anc 694 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) = ((1...𝑦) ∪ ((𝑦 + 1)...𝑁)))
550549imaeq2d 5501 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑁)) = (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))))
551 f1ofo 6182 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–onto→(1...𝑁))
552 foima 6158 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–onto→(1...𝑁) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑁)) = (1...𝑁))
553231, 551, 5523syl 18 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑁)) = (1...𝑁))
554553adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑁)) = (1...𝑁))
555550, 554eqtr3d 2687 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))) = (1...𝑁))
556546, 555syl5eqr 2699 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))) = (1...𝑁))
557556feq2d 6069 . . . . . . . . . . . . . . 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})))
558545, 557mpbid 222 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
559558ffvelrnda 6399 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) ∈ ({1} ∪ {0}))
560540, 559sseldi 3634 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) ∈ ℂ)
561560addid2d 10275 . . . . . . . . . . 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}))‘𝑛))
562561adantr 480 . . . . . . . . . 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}))‘𝑛))
563534, 562eqtr4d 2688 . . . . . . . . 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}))‘𝑛)))
56497, 99, 290, 563ifbothda 4156 . . . . . . . 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}))‘𝑛)))
565564oveq2d 6706 . . . . . . 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}))‘𝑛))))
566 elmapi 7921 . . . . . . . . . . . . 13 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
56729, 566syl 17 . . . . . . . . . . . 12 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
568567ffvelrnda 6399 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ (0..^𝐾))
569 elfzonn0 12552 . . . . . . . . . . 11 (((1st ‘(1st𝑇))‘𝑛) ∈ (0..^𝐾) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℕ0)
570568, 569syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℕ0)
571570nn0cnd 11391 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℂ)
572571adantlr 751 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℂ)
573142, 537keepel 4188 . . . . . . . . 9 if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) ∈ ℂ
574573a1i 11 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) ∈ ℂ)
575572, 574, 560addassd 10100 . . . . . . 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}))‘𝑛))))
576565, 575eqtr4d 2688 . . . . . 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}))‘𝑛)))
577576mpteq2dva 4777 . . . . 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}))‘𝑛))))
57895, 577eqtrd 2685 . . . 4 ((𝜑𝑦 ∈ (0...(𝑁 − 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}))‘𝑛))))
579 poimirlem18.4 . . . . . . . . . 10 (𝜑 → (2nd𝑇) = 0)
580579adantr 480 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (2nd𝑇) = 0)
581 elfzle1 12382 . . . . . . . . . 10 (𝑦 ∈ (0...(𝑁 − 1)) → 0 ≤ 𝑦)
582581adantl 481 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 0 ≤ 𝑦)
583580, 582eqbrtrd 4707 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (2nd𝑇) ≤ 𝑦)
584 0re 10078 . . . . . . . . . 10 0 ∈ ℝ
585579, 584syl6eqel 2738 . . . . . . . . 9 (𝜑 → (2nd𝑇) ∈ ℝ)
586 lenlt 10154 . . . . . . . . 9 (((2nd𝑇) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((2nd𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd𝑇)))
587585, 237, 586syl2an 493 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd𝑇)))
588583, 587mpbid 222 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ¬ 𝑦 < (2nd𝑇))
589588iffalsed 4130 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = (𝑦 + 1))
590589csbeq1d 3573 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑦 + 1) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
591 ovex 6718 . . . . . 6 (𝑦 + 1) ∈ V
592 oveq2 6698 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → (1...𝑗) = (1...(𝑦 + 1)))
593592imaeq2d 5501 . . . . . . . . 9 (𝑗 = (𝑦 + 1) → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
594593xpeq1d 5172 . . . . . . . 8 (𝑗 = (𝑦 + 1) → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}))
595 oveq1 6697 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (𝑗 + 1) = ((𝑦 + 1) + 1))
596595oveq1d 6705 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → ((𝑗 + 1)...𝑁) = (((𝑦 + 1) + 1)...𝑁))
597596imaeq2d 5501 . . . . . . . . 9 (𝑗 = (𝑦 + 1) → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
598597xpeq1d 5172 . . . . . . . 8 (𝑗 = (𝑦 + 1) → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
599594, 598uneq12d 3801 . . . . . . 7 (𝑗 = (𝑦 + 1) → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
600599oveq2d 6706 . . . . . 6 (𝑗 = (𝑦 + 1) → ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
601591, 600csbie 3592 . . . . 5 (𝑦 + 1) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
602590, 601syl6eq 2701 . . . 4 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
603 ovexd 6720 . . . . 5 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0)) ∈ V)
604 fvexd 6241 . . . . 5 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) ∈ V)
605 eqidd 2652 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))) = (𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))))
606 ffn 6083 . . . . . . 7 ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (1...𝑁))
607558, 606syl 17 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (1...𝑁))
608 nfcv 2793 . . . . . . . . . . 11 𝑛(2nd ‘(1st𝑇))
609 nfmpt1 4780 . . . . . . . . . . 11 𝑛(𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))
610608, 609nfco 5320 . . . . . . . . . 10 𝑛((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))
611 nfcv 2793 . . . . . . . . . 10 𝑛(1...𝑦)
612610, 611nfima 5509 . . . . . . . . 9 𝑛(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦))
613 nfcv 2793 . . . . . . . . 9 𝑛{1}
614612, 613nfxp 5176 . . . . . . . 8 𝑛((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1})
615 nfcv 2793 . . . . . . . . . 10 𝑛((𝑦 + 1)...𝑁)
616610, 615nfima 5509 . . . . . . . . 9 𝑛(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))
617 nfcv 2793 . . . . . . . . 9 𝑛{0}
618616, 617nfxp 5176 . . . . . . . 8 𝑛((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})
619614, 618nfun 3802 . . . . . . 7 𝑛(((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))
620619dffn5f 6291 . . . . . 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}))‘𝑛)))
621607, 620sylib 208 . . . . 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}))‘𝑛)))
62291, 603, 604, 605, 621offval2 6956 . . . 4 ((𝜑𝑦 ∈ (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}))) = (𝑛 ∈ (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}))‘𝑛))))
623578, 602, 6223eqtr4rd 2696 . . 3 ((𝜑𝑦 ∈ (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}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
624623mpteq2dva 4777 . 2 (𝜑 → (𝑦 ∈ (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})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
62522, 624eqtr4d 2688 1 (𝜑𝐹 = (𝑦 ∈ (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})))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   ∈ wcel 2030  {cab 2637   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  ∃!wreu 2943  {crab 2945  Vcvv 3231  ⦋csb 3566   ∖ cdif 3604   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  ifcif 4119  {csn 4210  ⟨cop 4216   class class class wbr 4685   ↦ cmpt 4762   × cxp 5141  ◡ccnv 5142  ran crn 5144   ↾ cres 5145   “ cima 5146   ∘ ccom 5147  Fun wfun 5920   Fn wfn 5921  ⟶wf 5922  –onto→wfo 5924  –1-1-onto→wf1o 5925  ‘cfv 5926  (class class class)co 6690   ∘𝑓 cof 6937  1st c1st 7208  2nd c2nd 7209   ↑𝑚 cmap 7899  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   < clt 10112   ≤ cle 10113   − cmin 10304  ℕcn 11058  ℕ0cn0 11330  ℤcz 11415  ℤ≥cuz 11725  ...cfz 12364  ..^cfzo 12504 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505 This theorem is referenced by:  poimirlem17  33556
 Copyright terms: Public domain W3C validator