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

Theorem poimirlem16 33396
Description: Lemma for poimir 33413 establishing the vertices of the simplex of poimirlem17 33397. (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 6178 . . . . . . . . . . 11 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
32breq2d 4656 . . . . . . . . . 10 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
43ifbid 4099 . . . . . . . . 9 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
54csbeq1d 3533 . . . . . . . 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 6178 . . . . . . . . . . 11 (𝑡 = 𝑇 → (1st𝑡) = (1st𝑇))
76fveq2d 6182 . . . . . . . . . 10 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
86fveq2d 6182 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
98imaeq1d 5453 . . . . . . . . . . . 12 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
109xpeq1d 5128 . . . . . . . . . . 11 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
118imaeq1d 5453 . . . . . . . . . . . 12 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
1211xpeq1d 5128 . . . . . . . . . . 11 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
1310, 12uneq12d 3760 . . . . . . . . . 10 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
147, 13oveq12d 6653 . . . . . . . . 9 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
1514csbeq2dv 3983 . . . . . . . 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 2654 . . . . . . 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 4736 . . . . . 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 2630 . . . . 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 3360 . . . 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 480 . . 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 3353 . . . . . . . . . . . 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 2717 . . . . . . . . . . 11 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
251, 24syl 17 . . . . . . . . . 10 (𝜑𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
26 xp1st 7183 . . . . . . . . . 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 7183 . . . . . . . . 9 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
2927, 28syl 17 . . . . . . . 8 (𝜑 → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
30 elmapfn 7865 . . . . . . . 8 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑇)) Fn (1...𝑁))
3129, 30syl 17 . . . . . . 7 (𝜑 → (1st ‘(1st𝑇)) Fn (1...𝑁))
3231adantr 481 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1st ‘(1st𝑇)) Fn (1...𝑁))
33 1ex 10020 . . . . . . . . . 10 1 ∈ V
34 fnconstg 6080 . . . . . . . . . 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 10019 . . . . . . . . . 10 0 ∈ V
37 fnconstg 6080 . . . . . . . . . 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 471 . . . . . . . 8 ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∧ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
40 xp2nd 7184 . . . . . . . . . . . . 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 6188 . . . . . . . . . . . . 13 (2nd ‘(1st𝑇)) ∈ V
43 f1oeq1 6114 . . . . . . . . . . . . 13 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
4442, 43elab 3344 . . . . . . . . . . . 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 6130 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑇))))
4746simprbi 480 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑇)))
4845, 47syl 17 . . . . . . . . . 10 (𝜑 → Fun (2nd ‘(1st𝑇)))
49 imain 5962 . . . . . . . . . 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 12417 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ0)
52 nn0p1nn 11317 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ0 → (𝑦 + 1) ∈ ℕ)
5351, 52syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℕ)
5453nnred 11020 . . . . . . . . . . . . 13 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℝ)
5554ltp1d 10939 . . . . . . . . . . . 12 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) < ((𝑦 + 1) + 1))
56 fzdisj 12353 . . . . . . . . . . . 12 ((𝑦 + 1) < ((𝑦 + 1) + 1) → ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
5755, 56syl 17 . . . . . . . . . . 11 (𝑦 ∈ (0...(𝑁 − 1)) → ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
5857imaeq2d 5454 . . . . . . . . . 10 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
59 ima0 5469 . . . . . . . . . 10 ((2nd ‘(1st𝑇)) “ ∅) = ∅
6058, 59syl6eq 2670 . . . . . . . . 9 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ∅)
6150, 60sylan9req 2675 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅)
62 fnun 5985 . . . . . . . 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 694 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
64 imaundi 5533 . . . . . . . . 9 ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
65 nnuz 11708 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
6653, 65syl6eleq 2709 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (ℤ‘1))
67 peano2uz 11726 . . . . . . . . . . . . . 14 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1) + 1) ∈ (ℤ‘1))
6866, 67syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ (ℤ‘1))
6968adantl 482 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1) + 1) ∈ (ℤ‘1))
70 poimir.0 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ)
7170nncnd 11021 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℂ)
72 npcan1 10440 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
7371, 72syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
7473adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
75 elfzuz3 12324 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ𝑦))
76 eluzp1p1 11698 . . . . . . . . . . . . . . 15 ((𝑁 − 1) ∈ (ℤ𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
7775, 76syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
7877adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
7974, 78eqeltrrd 2700 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘(𝑦 + 1)))
80 fzsplit2 12351 . . . . . . . . . . . 12 ((((𝑦 + 1) + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘(𝑦 + 1))) → (1...𝑁) = ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
8169, 79, 80syl2anc 692 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) = ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
8281imaeq2d 5454 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))))
83 f1ofo 6131 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
84 foima 6107 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
8545, 83, 843syl 18 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
8685adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
8782, 86eqtr3d 2656 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (1...𝑁))
8864, 87syl5eqr 2668 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = (1...𝑁))
8988fneq2d 5970 . . . . . . 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 6665 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) ∈ V)
92 inidm 3814 . . . . . 6 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
93 eqidd 2621 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) = ((1st ‘(1st𝑇))‘𝑛))
94 eqidd 2621 . . . . . 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 6889 . . . . 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 6642 . . . . . . . . . 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 2630 . . . . . . . . 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 6642 . . . . . . . . . 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 2630 . . . . . . . . 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 11118 . . . . . . . . . . . . . 14 (1 + 0) = 1
101100eqcomi 2629 . . . . . . . . . . . . 13 1 = (1 + 0)
102 f1ofn 6125 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
10345, 102syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (2nd ‘(1st𝑇)) Fn (1...𝑁))
104103adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
105 fzss2 12366 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘(𝑦 + 1)) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
10679, 105syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
107 eluzfz1 12333 . . . . . . . . . . . . . . . . . 18 ((𝑦 + 1) ∈ (ℤ‘1) → 1 ∈ (1...(𝑦 + 1)))
10866, 107syl 17 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → 1 ∈ (1...(𝑦 + 1)))
109108adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 1 ∈ (1...(𝑦 + 1)))
110 fnfvima 6481 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ (1...(𝑦 + 1)) ⊆ (1...𝑁) ∧ 1 ∈ (1...(𝑦 + 1))) → ((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
111104, 106, 109, 110syl3anc 1324 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
112 fvun1 6256 . . . . . . . . . . . . . . . 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 1412 . . . . . . . . . . . . . . 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 692 . . . . . . . . . . . . . 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 6454 . . . . . . . . . . . . . . 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 2654 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = 1)
118 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → 𝑛 ∈ (1...(𝑁 − 1)))
11970nnzd 11466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℤ)
120 peano2zm 11405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
121119, 120syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑁 − 1) ∈ ℤ)
122 1z 11392 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ ℤ
123121, 122jctil 559 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ))
124 elfzelz 12327 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℤ)
125124, 122jctir 560 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ (1...(𝑁 − 1)) → (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
126 fzaddel 12360 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ (1...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1))))
127123, 125, 126syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 ∈ (1...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1))))
128118, 127mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1)))
12973oveq2d 6651 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 + 1)...𝑁))
130129adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 + 1)...𝑁))
131128, 130eleqtrd 2701 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 + 1) ∈ ((1 + 1)...𝑁))
132131ralrimiva 2963 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑛 + 1) ∈ ((1 + 1)...𝑁))
133 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → 𝑦 ∈ ((1 + 1)...𝑁))
134 peano2z 11403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 ∈ ℤ → (1 + 1) ∈ ℤ)
135122, 134ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (1 + 1) ∈ ℤ
136119, 135jctil 559 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ))
137 elfzelz 12327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ((1 + 1)...𝑁) → 𝑦 ∈ ℤ)
138137, 122jctir 560 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ((1 + 1)...𝑁) → (𝑦 ∈ ℤ ∧ 1 ∈ ℤ))
139 fzsubel 12362 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑦 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑦 ∈ ((1 + 1)...𝑁) ↔ (𝑦 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
140136, 138, 139syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 ∈ ((1 + 1)...𝑁) ↔ (𝑦 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
141133, 140mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1)))
142 ax-1cn 9979 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ ℂ
143142, 142pncan3oi 10282 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 + 1) − 1) = 1
144143oveq1i 6645 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 + 1) − 1)...(𝑁 − 1)) = (1...(𝑁 − 1))
145141, 144syl6eleq 2709 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 − 1) ∈ (1...(𝑁 − 1)))
146137zcnd 11468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ((1 + 1)...𝑁) → 𝑦 ∈ ℂ)
147 elfznn 12355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℕ)
148147nncnd 11021 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℂ)
149 subadd2 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑦 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑦 − 1) = 𝑛 ↔ (𝑛 + 1) = 𝑦))
150142, 149mp3an2 1410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑦 − 1) = 𝑛 ↔ (𝑛 + 1) = 𝑦))
151150bicomd 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑛 + 1) = 𝑦 ↔ (𝑦 − 1) = 𝑛))
152 eqcom 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑛 + 1) = 𝑦𝑦 = (𝑛 + 1))
153 eqcom 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦 − 1) = 𝑛𝑛 = (𝑦 − 1))
154151, 152, 1533bitr3g 302 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1)))
155146, 148, 154syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ((1 + 1)...𝑁) ∧ 𝑛 ∈ (1...(𝑁 − 1))) → (𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1)))
156155ralrimiva 2963 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((1 + 1)...𝑁) → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1)))
157156adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1)))
158 reu6i 3391 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑦 − 1) ∈ (1...(𝑁 − 1)) ∧ ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) → ∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1))
159145, 157, 158syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → ∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1))
160159ralrimiva 2963 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑦 ∈ ((1 + 1)...𝑁)∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1))
161 eqid 2620 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) = (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1))
162161f1ompt 6368 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 + 1)...𝑁) ↔ (∀𝑛 ∈ (1...(𝑁 − 1))(𝑛 + 1) ∈ ((1 + 1)...𝑁) ∧ ∀𝑦 ∈ ((1 + 1)...𝑁)∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1)))
163132, 160, 162sylanbrc 697 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 + 1)...𝑁))
164 f1osng 6164 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ 1 ∈ V) → {⟨𝑁, 1⟩}:{𝑁}–1-1-onto→{1})
16570, 33, 164sylancl 693 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {⟨𝑁, 1⟩}:{𝑁}–1-1-onto→{1})
16670nnred 11020 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑁 ∈ ℝ)
167166ltm1d 10941 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑁 − 1) < 𝑁)
168121zred 11467 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑁 − 1) ∈ ℝ)
169168, 166ltnled 10169 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
170167, 169mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
171 elfzle2 12330 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
172170, 171nsyl 135 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
173 disjsn 4237 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1)))
174172, 173sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅)
175 1re 10024 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 ∈ ℝ
176175ltp1i 10912 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 < (1 + 1)
177175, 175readdcli 10038 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (1 + 1) ∈ ℝ
178175, 177ltnlei 10143 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 < (1 + 1) ↔ ¬ (1 + 1) ≤ 1)
179176, 178mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . . 25 ¬ (1 + 1) ≤ 1
180 elfzle1 12329 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ((1 + 1)...𝑁) → (1 + 1) ≤ 1)
181179, 180mto 188 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ 1 ∈ ((1 + 1)...𝑁)
182 disjsn 4237 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((1 + 1)...𝑁) ∩ {1}) = ∅ ↔ ¬ 1 ∈ ((1 + 1)...𝑁))
183181, 182mpbir 221 . . . . . . . . . . . . . . . . . . . . . . 23 (((1 + 1)...𝑁) ∩ {1}) = ∅
184 f1oun 6143 . . . . . . . . . . . . . . . . . . . . . . 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 719 . . . . . . . . . . . . . . . . . . . . . 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 1323 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}):((1...(𝑁 − 1)) ∪ {𝑁})–1-1-onto→(((1 + 1)...𝑁) ∪ {1}))
187 ssv 3617 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℕ ⊆ V
188187, 70sseldi 3593 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑁 ∈ V)
18933a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ∈ V)
19070, 65syl6eleq 2709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑁 ∈ (ℤ‘1))
19173, 190eqeltrd 2699 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘1))
192 uzid 11687 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
193 peano2uz 11726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
194121, 192, 1933syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
19573, 194eqeltrrd 2700 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
196 fzsplit2 12351 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
197191, 195, 196syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
19873oveq1d 6650 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
199 fzsn 12368 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
200119, 199syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑁...𝑁) = {𝑁})
201198, 200eqtrd 2654 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
202201uneq2d 3759 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁}))
203197, 202eqtr2d 2655 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁))
204 iftrue 4083 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑁 → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = 1)
205204adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑛 = 𝑁) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = 1)
206188, 189, 203, 205fmptapd 6422 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∪ {⟨𝑁, 1⟩}) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))
207 eleq1 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑁 → (𝑛 ∈ (1...(𝑁 − 1)) ↔ 𝑁 ∈ (1...(𝑁 − 1))))
208207notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑁 → (¬ 𝑛 ∈ (1...(𝑁 − 1)) ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1))))
209172, 208syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑛 = 𝑁 → ¬ 𝑛 ∈ (1...(𝑁 − 1))))
210209necon2ad 2806 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛𝑁))
211210imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → 𝑛𝑁)
212 ifnefalse 4089 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛𝑁 → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1))
213211, 212syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1))
214213mpteq2dva 4735 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)))
215214uneq1d 3758 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∪ {⟨𝑁, 1⟩}) = ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}))
216206, 215eqtr3d 2656 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}))
217197, 202eqtrd 2654 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁}))
218 uzid 11687 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℤ → 1 ∈ (ℤ‘1))
219 peano2uz 11726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ (ℤ‘1) → (1 + 1) ∈ (ℤ‘1))
220122, 218, 219mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 + 1) ∈ (ℤ‘1)
221 fzsplit2 12351 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘1)) → (1...𝑁) = ((1...1) ∪ ((1 + 1)...𝑁)))
222220, 190, 221sylancr 694 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑁) = ((1...1) ∪ ((1 + 1)...𝑁)))
223 fzsn 12368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 ∈ ℤ → (1...1) = {1})
224122, 223ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1...1) = {1}
225224uneq1i 3755 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1...1) ∪ ((1 + 1)...𝑁)) = ({1} ∪ ((1 + 1)...𝑁))
226225equncomi 3751 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...1) ∪ ((1 + 1)...𝑁)) = (((1 + 1)...𝑁) ∪ {1})
227222, 226syl6eq 2670 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1...𝑁) = (((1 + 1)...𝑁) ∪ {1}))
228216, 217, 227f1oeq123d 6120 . . . . . . . . . . . . . . . . . . . . 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 6146 . . . . . . . . . . . . . . . . . . . 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 692 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁))
232 dff1o3 6130 . . . . . . . . . . . . . . . . . . . 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 480 . . . . . . . . . . . . . . . . . . 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 5962 . . . . . . . . . . . . . . . . . 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 11337 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
238237ltp1d 10939 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 < (𝑦 + 1))
239 fzdisj 12353 . . . . . . . . . . . . . . . . . . . 20 (𝑦 < (𝑦 + 1) → ((1...𝑦) ∩ ((𝑦 + 1)...𝑁)) = ∅)
240238, 239syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → ((1...𝑦) ∩ ((𝑦 + 1)...𝑁)) = ∅)
241240imaeq2d 5454 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0...(𝑁 − 1)) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ∅))
242 ima0 5469 . . . . . . . . . . . . . . . . . 18 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ∅) = ∅
243241, 242syl6eq 2670 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = ∅)
244236, 243sylan9req 2675 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))) = ∅)
245 imassrn 5465 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)) ⊆ ran (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))
246 f1of 6124 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁) → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)⟶(1...𝑁))
247 frn 6040 . . . . . . . . . . . . . . . . . . . . 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 3606 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)) ⊆ (1...𝑁))
250249adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)) ⊆ (1...𝑁))
251 elfz1end 12356 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
25270, 251sylib 208 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑁 ∈ (1...𝑁))
253 eqid 2620 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))
254204, 253, 33fvmpt 6269 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (1...𝑁) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) = 1)
255252, 254syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) = 1)
256255adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) = 1)
257 f1ofn 6125 . . . . . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁))
260 fzss1 12365 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
26166, 260syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
262261adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
263 eluzfz2 12334 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (ℤ‘(𝑦 + 1)) → 𝑁 ∈ ((𝑦 + 1)...𝑁))
26479, 263syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑦 + 1)...𝑁))
265 fnfvima 6481 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁) ∧ ((𝑦 + 1)...𝑁) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑦 + 1)...𝑁)) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)))
266259, 262, 264, 265syl3anc 1324 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)))
267256, 266eqeltrrd 2700 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 1 ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)))
268 fnfvima 6481 . . . . . . . . . . . . . . . . . 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 1324 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁))))
270 imaco 5628 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)))
271269, 270syl6eleqr 2710 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇))‘1) ∈ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)))
272 fnconstg 6080 . . . . . . . . . . . . . . . . . 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 6080 . . . . . . . . . . . . . . . . . 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 6257 . . . . . . . . . . . . . . . . 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 1412 . . . . . . . . . . . . . . . 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 692 . . . . . . . . . . . . . . 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 6454 . . . . . . . . . . . . . . . 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 2654 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = 0)
282281oveq2d 6651 . . . . . . . . . . . . 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 2680 . . . . . . . . . . . 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 6178 . . . . . . . . . . . . 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 6178 . . . . . . . . . . . . . 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 6651 . . . . . . . . . . . . 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 2635 . . . . . . . . . . . 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 445 . . . . . . . . . 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 750 . . . . . . . . 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 4308 . . . . . . . . . . . . . 14 (𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ↔ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘1)))
292 df-ne 2792 . . . . . . . . . . . . . . 15 (𝑛 ≠ ((2nd ‘(1st𝑇))‘1) ↔ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1))
293292anbi2i 729 . . . . . . . . . . . . . 14 ((𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘1)) ↔ (𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1)))
294291, 293bitri 264 . . . . . . . . . . . . 13 (𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ↔ (𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1)))
295 fnconstg 6080 . . . . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . . . 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 5962 . . . . . . . . . . . . . . . . . 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 12353 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 + 1) < ((𝑦 + 1) + 1) → (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
30155, 300syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
302301imaeq2d 5454 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
303302, 59syl6eq 2670 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ∅)
304299, 303sylan9req 2675 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅)
305 fnun 5985 . . . . . . . . . . . . . . . 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 694 . . . . . . . . . . . . . . 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 5533 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
308 fzpred 12374 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ‘1) → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁)))
309190, 308syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁)))
310 uncom 3749 . . . . . . . . . . . . . . . . . . . . . . . 24 ({1} ∪ ((1 + 1)...𝑁)) = (((1 + 1)...𝑁) ∪ {1})
311309, 310syl6eq 2670 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑁) = (((1 + 1)...𝑁) ∪ {1}))
312311difeq1d 3719 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...𝑁) ∖ {1}) = ((((1 + 1)...𝑁) ∪ {1}) ∖ {1}))
313 difun2 4039 . . . . . . . . . . . . . . . . . . . . . . 23 ((((1 + 1)...𝑁) ∪ {1}) ∖ {1}) = (((1 + 1)...𝑁) ∖ {1})
314 disj3 4012 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((1 + 1)...𝑁) ∩ {1}) = ∅ ↔ ((1 + 1)...𝑁) = (((1 + 1)...𝑁) ∖ {1}))
315183, 314mpbi 220 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 + 1)...𝑁) = (((1 + 1)...𝑁) ∖ {1})
316313, 315eqtr4i 2645 . . . . . . . . . . . . . . . . . . . . . 22 ((((1 + 1)...𝑁) ∪ {1}) ∖ {1}) = ((1 + 1)...𝑁)
317312, 316syl6eq 2670 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((1...𝑁) ∖ {1}) = ((1 + 1)...𝑁))
318317adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1...𝑁) ∖ {1}) = ((1 + 1)...𝑁))
319 eluzp1p1 11698 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1) + 1) ∈ (ℤ‘(1 + 1)))
32066, 319syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ (ℤ‘(1 + 1)))
321320adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1) + 1) ∈ (ℤ‘(1 + 1)))
322 fzsplit2 12351 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 + 1) + 1) ∈ (ℤ‘(1 + 1)) ∧ 𝑁 ∈ (ℤ‘(𝑦 + 1))) → ((1 + 1)...𝑁) = (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
323321, 79, 322syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1 + 1)...𝑁) = (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
324318, 323eqtrd 2654 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1...𝑁) ∖ {1}) = (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
325324imaeq2d 5454 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))))
326 imadif 5961 . . . . . . . . . . . . . . . . . . . . 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 12333 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ‘1) → 1 ∈ (1...𝑁))
329190, 328syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 ∈ (1...𝑁))
330 fnsnfv 6245 . . . . . . . . . . . . . . . . . . . . . . 23 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ 1 ∈ (1...𝑁)) → {((2nd ‘(1st𝑇))‘1)} = ((2nd ‘(1st𝑇)) “ {1}))
331103, 329, 330syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {((2nd ‘(1st𝑇))‘1)} = ((2nd ‘(1st𝑇)) “ {1}))
332331eqcomd 2626 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((2nd ‘(1st𝑇)) “ {1}) = {((2nd ‘(1st𝑇))‘1)})
33385, 332difeq12d 3721 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {1})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
334327, 333eqtrd 2654 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
335334adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
336325, 335eqtr3d 2656 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
337307, 336syl5eqr 2668 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
338337fneq2d 5970 . . . . . . . . . . . . . . 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 3797 . . . . . . . . . . . . . . . 16 (((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∩ {((2nd ‘(1st𝑇))‘1)}) = ({((2nd ‘(1st𝑇))‘1)} ∩ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
341 disjdif 4031 . . . . . . . . . . . . . . . 16 ({((2nd ‘(1st𝑇))‘1)} ∩ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)})) = ∅
342340, 341eqtri 2642 . . . . . . . . . . . . . . 15 (((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∩ {((2nd ‘(1st𝑇))‘1)}) = ∅
343 fnconstg 6080 . . . . . . . . . . . . . . . . . 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 6256 . . . . . . . . . . . . . . . . 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 1410 . . . . . . . . . . . . . . . 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 6080 . . . . . . . . . . . . . . . . . 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 6256 . . . . . . . . . . . . . . . . 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 1410 . . . . . . . . . . . . . . . 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 2657 . . . . . . . . . . . . . . 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 718 . . . . . . . . . . . . . 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 488 . . . . . . . . . . . . 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 493 . . . . . . . . . . . 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 679 . . . . . . . . . . 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 12374 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 + 1) ∈ (ℤ‘1) → (1...(𝑦 + 1)) = ({1} ∪ ((1 + 1)...(𝑦 + 1))))
35766, 356syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (0...(𝑁 − 1)) → (1...(𝑦 + 1)) = ({1} ∪ ((1 + 1)...(𝑦 + 1))))
358357imaeq2d 5454 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) = ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))))
359358adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) = ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))))
360331uneq1d 3758 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1)))) = (((2nd ‘(1st𝑇)) “ {1}) ∪ ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1)))))
361 uncom 3749 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) = ({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
362 imaundi 5533 . . . . . . . . . . . . . . . . . . . 20 ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))) = (((2nd ‘(1st𝑇)) “ {1}) ∪ ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
363360, 361, 3623eqtr4g 2679 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) = ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))))
364363adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) = ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))))
365359, 364eqtr4d 2657 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}))
366365xpeq1d 5128 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) = ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) × {1}))
367 xpundir 5162 . . . . . . . . . . . . . . . 16 ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) × {1}) = ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1}))
368366, 367syl6eq 2670 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) = ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1})))
369368uneq1d 3758 . . . . . . . . . . . . . 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 3764 . . . . . . . . . . . . . 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 2670 . . . . . . . . . . . . 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 6180 . . . . . . . . . . . 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 761 . . . . . . . . . . 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 5628 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦)))
375 df-ima 5117 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦)) = ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ (1...𝑦))
376 peano2uz 11726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 − 1) ∈ (ℤ𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
37775, 376syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
378377adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
37974, 378eqeltrrd 2700 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ𝑦))
380 fzss2 12366 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ𝑦) → (1...𝑦) ⊆ (1...𝑁))
381379, 380syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑦) ⊆ (1...𝑁))
382381resmptd 5440 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ (1...𝑦)) = (𝑛 ∈ (1...𝑦) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))
383172adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
384 fzss2 12366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑁 − 1) ∈ (ℤ𝑦) → (1...𝑦) ⊆ (1...(𝑁 − 1)))
38575, 384syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ (0...(𝑁 − 1)) → (1...𝑦) ⊆ (1...(𝑁 − 1)))
386385adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑦) ⊆ (1...(𝑁 − 1)))
387386sseld 3594 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 ∈ (1...𝑦) → 𝑁 ∈ (1...(𝑁 − 1))))
388383, 387mtod 189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ¬ 𝑁 ∈ (1...𝑦))
389 eleq1 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑁 → (𝑛 ∈ (1...𝑦) ↔ 𝑁 ∈ (1...𝑦)))
390389notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑁 → (¬ 𝑛 ∈ (1...𝑦) ↔ ¬ 𝑁 ∈ (1...𝑦)))
391388, 390syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 = 𝑁 → ¬ 𝑛 ∈ (1...𝑦)))
392391necon2ad 2806 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑦) → 𝑛𝑁))
393392imp 445 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑦)) → 𝑛𝑁)
394393, 212syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑦)) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1))
395394mpteq2dva 4735 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑦) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)))
396382, 395eqtrd 2654 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ (1...𝑦)) = (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)))
397396rneqd 5342 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ (1...𝑦)) = ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)))
398375, 397syl5eq 2666 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦)) = ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)))
399 vex 3198 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 ∈ V
400 eqid 2620 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) = (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1))
401400elrnmpt 5361 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ V → (𝑗 ∈ ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) ↔ ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1)))
402399, 401ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) ↔ ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1))
403 elfzelz 12327 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
404403adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℤ)
405 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ (1...𝑦)) → 𝑛 ∈ (1...𝑦))
406122jctl 563 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℤ → (1 ∈ ℤ ∧ 𝑦 ∈ ℤ))
407 elfzelz 12327 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ (1...𝑦) → 𝑛 ∈ ℤ)
408407, 122jctir 560 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ (1...𝑦) → (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
409 fzaddel 12360 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ (1...𝑦) ↔ (𝑛 + 1) ∈ ((1 + 1)...(𝑦 + 1))))
410406, 408, 409syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ (1...𝑦)) → (𝑛 ∈ (1...𝑦) ↔ (𝑛 + 1) ∈ ((1 + 1)...(𝑦 + 1))))
411405, 410mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ (1...𝑦)) → (𝑛 + 1) ∈ ((1 + 1)...(𝑦 + 1)))
412 eleq1 2687 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = (𝑛 + 1) → (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) ↔ (𝑛 + 1) ∈ ((1 + 1)...(𝑦 + 1))))
413411, 412syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ (1...𝑦)) → (𝑗 = (𝑛 + 1) → 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
414413rexlimdva 3027 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℤ → (∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1) → 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
415 elfzelz 12327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → 𝑗 ∈ ℤ)
416415zcnd 11468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → 𝑗 ∈ ℂ)
417 npcan1 10440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ ℂ → ((𝑗 − 1) + 1) = 𝑗)
418416, 417syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → ((𝑗 − 1) + 1) = 𝑗)
419418eleq1d 2684 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → (((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1)) ↔ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
420419ibir 257 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → ((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1)))
421420adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → ((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1)))
422 peano2zm 11405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
423415, 422syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → (𝑗 − 1) ∈ ℤ)
424423, 122jctir 560 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → ((𝑗 − 1) ∈ ℤ ∧ 1 ∈ ℤ))
425 fzaddel 12360 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ((𝑗 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝑗 − 1) ∈ (1...𝑦) ↔ ((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1))))
426406, 424, 425syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → ((𝑗 − 1) ∈ (1...𝑦) ↔ ((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1))))
427421, 426mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → (𝑗 − 1) ∈ (1...𝑦))
428416adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → 𝑗 ∈ ℂ)
429417eqcomd 2626 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ ℂ → 𝑗 = ((𝑗 − 1) + 1))
430428, 429syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → 𝑗 = ((𝑗 − 1) + 1))
431 oveq1 6642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑗 − 1) → (𝑛 + 1) = ((𝑗 − 1) + 1))
432431eqeq2d 2630 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑗 − 1) → (𝑗 = (𝑛 + 1) ↔ 𝑗 = ((𝑗 − 1) + 1)))
433432rspcev 3304 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑗 − 1) ∈ (1...𝑦) ∧ 𝑗 = ((𝑗 − 1) + 1)) → ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1))
434427, 430, 433syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1))
435434ex 450 . . . . . . . . . . . . . . . . . . . . . . 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 2618 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) = ((1 + 1)...(𝑦 + 1)))
440398, 439eqtrd 2654 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦)) = ((1 + 1)...(𝑦 + 1)))
441440imaeq2d 5454 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦))) = ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
442374, 441syl5eq 2666 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) = ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
443442xpeq1d 5128 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}))
444 imaundi 5533 . . . . . . . . . . . . . . . . . . 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 5628 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ {𝑁}) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁}))
446 imaco 5628 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...(𝑁 − 1))) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))))
447445, 446uneq12i 3757 . . . . . . . . . . . . . . . . . . 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 2642 . . . . . . . . . . . . . . . . . 18 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1)))) = (((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})) ∪ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1)))))
449195adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
450 fzsplit2 12351 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)) ∧ 𝑁 ∈ (ℤ‘(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
45178, 449, 450syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
452201uneq2d 3759 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}))
453452adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}))
454451, 453eqtrd 2654 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}))
455 uncom 3749 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}) = ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1)))
456454, 455syl6eq 2670 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1))))
457456imaeq2d 5454 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) = (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1)))))
458255sneqd 4180 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁)} = {1})
459 fnsnfv 6245 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → {((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁)} = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁}))
460258, 252, 459syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁)} = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁}))
461458, 460eqtr3d 2656 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {1} = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁}))
462461imaeq2d 5454 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((2nd ‘(1st𝑇)) “ {1}) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})))
463331, 462eqtrd 2654 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {((2nd ‘(1st𝑇))‘1)} = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})))
464463adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → {((2nd ‘(1st𝑇))‘1)} = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})))
465 df-ima 5117 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))) = ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ ((𝑦 + 1)...(𝑁 − 1)))
466 fzss1 12365 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1)...(𝑁 − 1)) ⊆ (1...(𝑁 − 1)))
46766, 466syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...(𝑁 − 1)) ⊆ (1...(𝑁 − 1)))
468 fzss2 12366 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
469195, 468syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
470467, 469sylan9ssr 3609 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...(𝑁 − 1)) ⊆ (1...𝑁))
471470resmptd 5440 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ ((𝑦 + 1)...(𝑁 − 1))) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))
472 elfzle2 12330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑁 ∈ ((𝑦 + 1)...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
473170, 472nsyl 135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ¬ 𝑁 ∈ ((𝑦 + 1)...(𝑁 − 1)))
474 eleq1 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑁 → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ 𝑁 ∈ ((𝑦 + 1)...(𝑁 − 1))))
475474notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑁 → (¬ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ ¬ 𝑁 ∈ ((𝑦 + 1)...(𝑁 − 1))))
476473, 475syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝑛 = 𝑁 → ¬ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))))
477476con2d 129 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) → ¬ 𝑛 = 𝑁))
478477imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → ¬ 𝑛 = 𝑁)
479478iffalsed 4088 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1))
480479mpteq2dva 4735 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
481480adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
482471, 481eqtrd 2654 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ ((𝑦 + 1)...(𝑁 − 1))) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
483482rneqd 5342 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ ((𝑦 + 1)...(𝑁 − 1))) = ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
484465, 483syl5eq 2666 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))) = ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
485 elfzelz 12327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → 𝑗 ∈ ℤ)
486485zcnd 11468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → 𝑗 ∈ ℂ)
487486, 417syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → ((𝑗 − 1) + 1) = 𝑗)
488487eleq1d 2684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → ((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)))
49153nnzd 11466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12360 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑦 + 1) ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) ∧ ((𝑗 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝑗 − 1) ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ ((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
496492, 494, 495syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → 𝑗 = ((𝑗 − 1) + 1))
500432rspcev 3304 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑗 − 1) ∈ ((𝑦 + 1)...(𝑁 − 1)) ∧ 𝑗 = ((𝑗 − 1) + 1)) → ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1))
501497, 499, 500syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1))
502501ex 450 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1)))
503 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)))
504 elfzelz 12327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) → 𝑛 ∈ ℤ)
505504, 122jctir 560 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) → (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
506 fzaddel 12360 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑦 + 1) ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
507492, 505, 506syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2687 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3027 . . . . . . . . . . . . . . . . . . . . . . . 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 2620 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1))
514513elrnmpt 5361 . . . . . . . . . . . . . . . . . . . . . . . 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 2618 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) = ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
51873oveq2d 6651 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) = (((𝑦 + 1) + 1)...𝑁))
519518adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) = (((𝑦 + 1) + 1)...𝑁))
520484, 517, 5193eqtr2rd 2661 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1) + 1)...𝑁) = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))))
521520imaeq2d 5454 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1)))))
522464, 521uneq12d 3760 . . . . . . . . . . . . . . . . . 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 2680 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) = ({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
524523xpeq1d 5128 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}) = (({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) × {0}))
525 xpundir 5162 . . . . . . . . . . . . . . . 16 (({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) × {0}) = (({((2nd ‘(1st𝑇))‘1)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
526524, 525syl6eq 2670 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}) = (({((2nd ‘(1st𝑇))‘1)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
527443, 526uneq12d 3760 . . . . . . . . . . . . . 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 3762 . . . . . . . . . . . . . . 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 3764 . . . . . . . . . . . . . . 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 2644 . . . . . . . . . . . . . 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 2670 . . . . . . . . . . . . 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 6180 . . . . . . . . . . . 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 761 . . . . . . . . . . 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 2664 . . . . . . . . . 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 4330 . . . . . . . . . . . . . . 15 (1 ∈ ℂ → {1} ⊆ ℂ)
536142, 535ax-mp 5 . . . . . . . . . . . . . 14 {1} ⊆ ℂ
537 0cn 10017 . . . . . . . . . . . . . . 15 0 ∈ ℂ
538 snssi 4330 . . . . . . . . . . . . . . 15 (0 ∈ ℂ → {0} ⊆ ℂ)
539537, 538ax-mp 5 . . . . . . . . . . . . . 14 {0} ⊆ ℂ
540536, 539unssi 3780 . . . . . . . . . . . . 13 ({1} ∪ {0}) ⊆ ℂ
54133fconst 6078 . . . . . . . . . . . . . . . . 17 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦))⟶{1}
54236fconst 6078 . . . . . . . . . . . . . . . . 17 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))⟶{0}
543541, 542pm3.2i 471 . . . . . . . . . . . . . . . 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 6053 . . . . . . . . . . . . . . . 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 694 . . . . . . . . . . . . . . 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 5533 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))) = ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)))
54766adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ (ℤ‘1))
548 fzsplit2 12351 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑦)) → (1...𝑁) = ((1...𝑦) ∪ ((𝑦 + 1)...𝑁)))
549547, 379, 548syl2anc 692 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) = ((1...𝑦) ∪ ((𝑦 + 1)...𝑁)))
550549imaeq2d 5454 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑁)) = (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))))
551 f1ofo 6131 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–onto→(1...𝑁))
552 foima 6107 . . . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑁)) = (1...𝑁))
555550, 554eqtr3d 2656 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))) = (1...𝑁))
556546, 555syl5eqr 2668 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))) = (1...𝑁))
557556feq2d 6018 . . . . . . . . . . . . . . 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 6345 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) ∈ ({1} ∪ {0}))
560540, 559sseldi 3593 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) ∈ ℂ)
561560addid2d 10222 . . . . . . . . . . 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 481 . . . . . . . . . 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 2657 . . . . . . . . 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 4114 . . . . . . . 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 6651 . . . . . . 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 7864 . . . . . . . . . . . . 13 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
56729, 566syl 17 . . . . . . . . . . . 12 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
568567ffvelrnda 6345 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ (0..^𝐾))
569 elfzonn0 12496 . . . . . . . . . . 11 (((1st ‘(1st𝑇))‘𝑛) ∈ (0..^𝐾) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℕ0)
570568, 569syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℕ0)
571570nn0cnd 11338 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℂ)
572571adantlr 750 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℂ)
573142, 537keepel 4146 . . . . . . . . 9 if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) ∈ ℂ
574573a1i 11 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) ∈ ℂ)
575572, 574, 560addassd 10047 . . . . . . 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 2657 . . . . . 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 4735 . . . . 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 2654 . . . 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 481 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (2nd𝑇) = 0)
581 elfzle1 12329 . . . . . . . . . 10 (𝑦 ∈ (0...(𝑁 − 1)) → 0 ≤ 𝑦)
582581adantl 482 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 0 ≤ 𝑦)
583580, 582eqbrtrd 4666 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (2nd𝑇) ≤ 𝑦)
584 0re 10025 . . . . . . . . . 10 0 ∈ ℝ
585579, 584syl6eqel 2707 . . . . . . . . 9 (𝜑 → (2nd𝑇) ∈ ℝ)
586 lenlt 10101 . . . . . . . . 9 (((2nd𝑇) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((2nd𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd𝑇)))
587585, 237, 586syl2an 494 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd𝑇)))
588583, 587mpbid 222 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ¬ 𝑦 < (2nd𝑇))
589588iffalsed 4088 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = (𝑦 + 1))
590589csbeq1d 3533 . . . . 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 6663 . . . . . 6 (𝑦 + 1) ∈ V
592 oveq2 6643 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → (1...𝑗) = (1...(𝑦 + 1)))
593592imaeq2d 5454 . . . . . . . . 9 (𝑗 = (𝑦 + 1) → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
594593xpeq1d 5128 . . . . . . . 8 (𝑗 = (𝑦 + 1) → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}))
595 oveq1 6642 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (𝑗 + 1) = ((𝑦 + 1) + 1))
596595oveq1d 6650 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → ((𝑗 + 1)...𝑁) = (((𝑦 + 1) + 1)...𝑁))
597596imaeq2d 5454 . . . . . . . . 9 (𝑗 = (𝑦 + 1) → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
598597xpeq1d 5128 . . . . . . . 8 (𝑗 = (𝑦 + 1) → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
599594, 598uneq12d 3760 . . . . . . 7 (𝑗 = (𝑦 + 1) → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
600599oveq2d 6651 . . . . . 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 3552 . . . . 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 2670 . . . 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 6665 . . . . 5 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0)) ∈ V)
604 fvexd 6190 . . . . 5 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) ∈ V)
605 eqidd 2621 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))) = (𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))))
606 ffn 6032 . . . . . . 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 2762 . . . . . . . . . . 11 𝑛(2nd ‘(1st𝑇))
609 nfmpt1 4738 . . . . . . . . . . 11 𝑛(𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))
610608, 609nfco 5276 . . . . . . . . . 10 𝑛((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))
611 nfcv 2762 . . . . . . . . . 10 𝑛(1...𝑦)
612610, 611nfima 5462 . . . . . . . . 9 𝑛(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦))
613 nfcv 2762 . . . . . . . . 9 𝑛{1}
614612, 613nfxp 5132 . . . . . . . 8 𝑛((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1})
615 nfcv 2762 . . . . . . . . . 10 𝑛((𝑦 + 1)...𝑁)
616610, 615nfima 5462 . . . . . . . . 9 𝑛(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))
617 nfcv 2762 . . . . . . . . 9 𝑛{0}
618616, 617nfxp 5132 . . . . . . . 8 𝑛((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})
619614, 618nfun 3761 . . . . . . 7 𝑛(((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))
620619dffn5f 6239 . . . . . 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 6899 . . . 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 2665 . . 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 4735 . 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 2657 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 384   = wceq 1481  wcel 1988  {cab 2606  wne 2791  wral 2909  wrex 2910  ∃!wreu 2911  {crab 2913  Vcvv 3195  csb 3526  cdif 3564  cun 3565  cin 3566  wss 3567  c0 3907  ifcif 4077  {csn 4168  cop 4174   class class class wbr 4644  cmpt 4720   × cxp 5102  ccnv 5103  ran crn 5105  cres 5106  cima 5107  ccom 5108  Fun wfun 5870   Fn wfn 5871  wf 5872  ontowfo 5874  1-1-ontowf1o 5875  cfv 5876  (class class class)co 6635  𝑓 cof 6880  1st c1st 7151  2nd c2nd 7152  𝑚 cmap 7842  cc 9919  cr 9920  0cc0 9921  1c1 9922   + caddc 9924   < clt 10059  cle 10060  cmin 10251  cn 11005  0cn0 11277  cz 11362  cuz 11672  ...cfz 12311  ..^cfzo 12449
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-of 6882  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-er 7727  df-map 7844  df-en 7941  df-dom 7942  df-sdom 7943  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-nn 11006  df-n0 11278  df-z 11363  df-uz 11673  df-fz 12312  df-fzo 12450
This theorem is referenced by:  poimirlem17  33397
  Copyright terms: Public domain W3C validator