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 35802
Description: Lemma for poimir 35819 establishing the vertices of the simplex of poimirlem17 35803. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimirlem22.s 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
poimirlem22.1 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))
poimirlem22.2 (𝜑𝑇𝑆)
poimirlem18.3 ((𝜑𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝𝑛) ≠ 𝐾)
poimirlem18.4 (𝜑 → (2nd𝑇) = 0)
Assertion
Ref Expression
poimirlem16 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))) ∘f + (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))))
Distinct variable groups:   𝑓,𝑗,𝑛,𝑝,𝑡,𝑦   𝜑,𝑗,𝑛,𝑦   𝑗,𝐹,𝑛,𝑦   𝑗,𝑁,𝑛,𝑦   𝑇,𝑗,𝑛,𝑦   𝜑,𝑝,𝑡   𝑓,𝐾,𝑗,𝑛,𝑝,𝑡   𝑓,𝑁,𝑝,𝑡   𝑇,𝑓,𝑝   𝑓,𝐹,𝑝,𝑡   𝑡,𝑇   𝑆,𝑗,𝑛,𝑝,𝑡,𝑦
Allowed substitution hints:   𝜑(𝑓)   𝑆(𝑓)   𝐾(𝑦)

Proof of Theorem poimirlem16
StepHypRef Expression
1 poimirlem22.2 . . 3 (𝜑𝑇𝑆)
2 fveq2 6783 . . . . . . . . . 10 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
32breq2d 5087 . . . . . . . . 9 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
43ifbid 4483 . . . . . . . 8 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
5 2fveq3 6788 . . . . . . . . 9 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
6 2fveq3 6788 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
76imaeq1d 5971 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
87xpeq1d 5619 . . . . . . . . . 10 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
96imaeq1d 5971 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
109xpeq1d 5619 . . . . . . . . . 10 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
118, 10uneq12d 4099 . . . . . . . . 9 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
125, 11oveq12d 7302 . . . . . . . 8 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
134, 12csbeq12dv 3842 . . . . . . 7 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
1413mpteq2dv 5177 . . . . . 6 (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
1514eqeq2d 2750 . . . . 5 (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
16 poimirlem22.s . . . . 5 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
1715, 16elrab2 3628 . . . 4 (𝑇𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
1817simprbi 497 . . 3 (𝑇𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
191, 18syl 17 . 2 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
20 elrabi 3619 . . . . . . . . . . . 12 (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
2120, 16eleq2s 2858 . . . . . . . . . . 11 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
221, 21syl 17 . . . . . . . . . 10 (𝜑𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
23 xp1st 7872 . . . . . . . . . 10 (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
2422, 23syl 17 . . . . . . . . 9 (𝜑 → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
25 xp1st 7872 . . . . . . . . 9 ((1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
2624, 25syl 17 . . . . . . . 8 (𝜑 → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
27 elmapfn 8662 . . . . . . . 8 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑇)) Fn (1...𝑁))
2826, 27syl 17 . . . . . . 7 (𝜑 → (1st ‘(1st𝑇)) Fn (1...𝑁))
2928adantr 481 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1st ‘(1st𝑇)) Fn (1...𝑁))
30 1ex 10980 . . . . . . . . . 10 1 ∈ V
31 fnconstg 6671 . . . . . . . . . 10 (1 ∈ V → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
3230, 31ax-mp 5 . . . . . . . . 9 (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1)))
33 c0ex 10978 . . . . . . . . . 10 0 ∈ V
34 fnconstg 6671 . . . . . . . . . 10 (0 ∈ V → (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
3533, 34ax-mp 5 . . . . . . . . 9 (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))
3632, 35pm3.2i 471 . . . . . . . 8 ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∧ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
37 xp2nd 7873 . . . . . . . . . . . . 13 ((1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
3824, 37syl 17 . . . . . . . . . . . 12 (𝜑 → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
39 fvex 6796 . . . . . . . . . . . . 13 (2nd ‘(1st𝑇)) ∈ V
40 f1oeq1 6713 . . . . . . . . . . . . 13 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
4139, 40elab 3610 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
4238, 41sylib 217 . . . . . . . . . . 11 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
43 dff1o3 6731 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑇))))
4443simprbi 497 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑇)))
4542, 44syl 17 . . . . . . . . . 10 (𝜑 → Fun (2nd ‘(1st𝑇)))
46 imain 6526 . . . . . . . . . 10 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
4745, 46syl 17 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
48 elfznn0 13358 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ0)
49 nn0p1nn 12281 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ0 → (𝑦 + 1) ∈ ℕ)
5048, 49syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℕ)
5150nnred 11997 . . . . . . . . . . . . 13 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℝ)
5251ltp1d 11914 . . . . . . . . . . . 12 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) < ((𝑦 + 1) + 1))
53 fzdisj 13292 . . . . . . . . . . . 12 ((𝑦 + 1) < ((𝑦 + 1) + 1) → ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
5452, 53syl 17 . . . . . . . . . . 11 (𝑦 ∈ (0...(𝑁 − 1)) → ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
5554imaeq2d 5972 . . . . . . . . . 10 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
56 ima0 5988 . . . . . . . . . 10 ((2nd ‘(1st𝑇)) “ ∅) = ∅
5755, 56eqtrdi 2795 . . . . . . . . 9 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ∅)
5847, 57sylan9req 2800 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅)
59 fnun 6554 . . . . . . . 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)...𝑁))))
6036, 58, 59sylancr 587 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
61 imaundi 6058 . . . . . . . . 9 ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
62 nnuz 12630 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
6350, 62eleqtrdi 2850 . . . . . . . . . . . . 13 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (ℤ‘1))
64 peano2uz 12650 . . . . . . . . . . . . 13 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1) + 1) ∈ (ℤ‘1))
6563, 64syl 17 . . . . . . . . . . . 12 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ (ℤ‘1))
66 poimir.0 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ)
6766nncnd 11998 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℂ)
68 npcan1 11409 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
6967, 68syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
7069adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
71 elfzuz3 13262 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ𝑦))
72 eluzp1p1 12619 . . . . . . . . . . . . . . 15 ((𝑁 − 1) ∈ (ℤ𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
7371, 72syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
7473adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
7570, 74eqeltrrd 2841 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘(𝑦 + 1)))
76 fzsplit2 13290 . . . . . . . . . . . 12 ((((𝑦 + 1) + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘(𝑦 + 1))) → (1...𝑁) = ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
7765, 75, 76syl2an2 683 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) = ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
7877imaeq2d 5972 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))))
79 f1ofo 6732 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
80 foima 6702 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
8142, 79, 803syl 18 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
8281adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
8378, 82eqtr3d 2781 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (1...𝑁))
8461, 83eqtr3id 2793 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = (1...𝑁))
8584fneq2d 6536 . . . . . . 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...𝑁)))
8660, 85mpbid 231 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
87 ovexd 7319 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) ∈ V)
88 inidm 4153 . . . . . 6 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
89 eqidd 2740 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) = ((1st ‘(1st𝑇))‘𝑛))
90 eqidd 2740 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛))
9129, 86, 87, 87, 88, 89, 90offval 7551 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) = (𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛))))
92 oveq1 7291 . . . . . . . . . 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}))‘𝑛)))
9392eqeq2d 2750 . . . . . . . . 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}))‘𝑛))))
94 oveq1 7291 . . . . . . . . . 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}))‘𝑛)))
9594eqeq2d 2750 . . . . . . . . 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}))‘𝑛))))
96 1p0e1 12106 . . . . . . . . . . . . . 14 (1 + 0) = 1
9796eqcomi 2748 . . . . . . . . . . . . 13 1 = (1 + 0)
98 f1ofn 6726 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
9942, 98syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (2nd ‘(1st𝑇)) Fn (1...𝑁))
10099adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
101 fzss2 13305 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘(𝑦 + 1)) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
10275, 101syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
103 eluzfz1 13272 . . . . . . . . . . . . . . . . . 18 ((𝑦 + 1) ∈ (ℤ‘1) → 1 ∈ (1...(𝑦 + 1)))
10463, 103syl 17 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → 1 ∈ (1...(𝑦 + 1)))
105104adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 1 ∈ (1...(𝑦 + 1)))
106 fnfvima 7118 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ (1...(𝑦 + 1)) ⊆ (1...𝑁) ∧ 1 ∈ (1...(𝑦 + 1))) → ((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
107100, 102, 105, 106syl3anc 1370 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
108 fvun1 6868 . . . . . . . . . . . . . . . 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)))
10932, 35, 108mp3an12 1450 . . . . . . . . . . . . . . 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)))
11058, 107, 109syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd ‘(1st𝑇))‘1)))
11130fvconst2 7088 . . . . . . . . . . . . . . 15 (((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) → ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd ‘(1st𝑇))‘1)) = 1)
112107, 111syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd ‘(1st𝑇))‘1)) = 1)
113110, 112eqtrd 2779 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = 1)
114 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → 𝑛 ∈ (1...(𝑁 − 1)))
11566nnzd 12434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℤ)
116 peano2zm 12372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
117115, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑁 − 1) ∈ ℤ)
118 1z 12359 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ ℤ
119117, 118jctil 520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ))
120 elfzelz 13265 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℤ)
121120, 118jctir 521 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ (1...(𝑁 − 1)) → (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
122 fzaddel 13299 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ (1...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1))))
123119, 121, 122syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 ∈ (1...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1))))
124114, 123mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1)))
12569oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 + 1)...𝑁))
126125adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 + 1)...𝑁))
127124, 126eleqtrd 2842 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 + 1) ∈ ((1 + 1)...𝑁))
128127ralrimiva 3104 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑛 + 1) ∈ ((1 + 1)...𝑁))
129 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → 𝑦 ∈ ((1 + 1)...𝑁))
130 peano2z 12370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 ∈ ℤ → (1 + 1) ∈ ℤ)
131118, 130ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (1 + 1) ∈ ℤ
132115, 131jctil 520 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ))
133 elfzelz 13265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ((1 + 1)...𝑁) → 𝑦 ∈ ℤ)
134133, 118jctir 521 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ((1 + 1)...𝑁) → (𝑦 ∈ ℤ ∧ 1 ∈ ℤ))
135 fzsubel 13301 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑦 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑦 ∈ ((1 + 1)...𝑁) ↔ (𝑦 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
136132, 134, 135syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 ∈ ((1 + 1)...𝑁) ↔ (𝑦 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
137129, 136mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1)))
138 ax-1cn 10938 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 ∈ ℂ
139138, 138pncan3oi 11246 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 + 1) − 1) = 1
140139oveq1i 7294 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((1 + 1) − 1)...(𝑁 − 1)) = (1...(𝑁 − 1))
141137, 140eleqtrdi 2850 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 − 1) ∈ (1...(𝑁 − 1)))
142133zcnd 12436 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ((1 + 1)...𝑁) → 𝑦 ∈ ℂ)
143 elfznn 13294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℕ)
144143nncnd 11998 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℂ)
145 subadd2 11234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑦 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑦 − 1) = 𝑛 ↔ (𝑛 + 1) = 𝑦))
146138, 145mp3an2 1448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑦 − 1) = 𝑛 ↔ (𝑛 + 1) = 𝑦))
147146bicomd 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑛 + 1) = 𝑦 ↔ (𝑦 − 1) = 𝑛))
148 eqcom 2746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑛 + 1) = 𝑦𝑦 = (𝑛 + 1))
149 eqcom 2746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦 − 1) = 𝑛𝑛 = (𝑦 − 1))
150147, 148, 1493bitr3g 313 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1)))
151142, 144, 150syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ((1 + 1)...𝑁) ∧ 𝑛 ∈ (1...(𝑁 − 1))) → (𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1)))
152151ralrimiva 3104 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((1 + 1)...𝑁) → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1)))
153152adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1)))
154 reu6i 3664 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑦 − 1) ∈ (1...(𝑁 − 1)) ∧ ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) → ∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1))
155141, 153, 154syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ ((1 + 1)...𝑁)) → ∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1))
156155ralrimiva 3104 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑦 ∈ ((1 + 1)...𝑁)∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1))
157 eqid 2739 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) = (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1))
158157f1ompt 6994 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 + 1)...𝑁) ↔ (∀𝑛 ∈ (1...(𝑁 − 1))(𝑛 + 1) ∈ ((1 + 1)...𝑁) ∧ ∀𝑦 ∈ ((1 + 1)...𝑁)∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1)))
159128, 156, 158sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 + 1)...𝑁))
160 f1osng 6766 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ 1 ∈ V) → {⟨𝑁, 1⟩}:{𝑁}–1-1-onto→{1})
16166, 30, 160sylancl 586 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {⟨𝑁, 1⟩}:{𝑁}–1-1-onto→{1})
16266nnred 11997 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑁 ∈ ℝ)
163162ltm1d 11916 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑁 − 1) < 𝑁)
164117zred 12435 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑁 − 1) ∈ ℝ)
165164, 162ltnled 11131 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
166163, 165mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
167 elfzle2 13269 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
168166, 167nsyl 140 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
169 disjsn 4648 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1)))
170168, 169sylibr 233 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅)
171 1re 10984 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 ∈ ℝ
172171ltp1i 11888 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 < (1 + 1)
173171, 171readdcli 10999 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (1 + 1) ∈ ℝ
174171, 173ltnlei 11105 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 < (1 + 1) ↔ ¬ (1 + 1) ≤ 1)
175172, 174mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . 25 ¬ (1 + 1) ≤ 1
176 elfzle1 13268 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ((1 + 1)...𝑁) → (1 + 1) ≤ 1)
177175, 176mto 196 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ 1 ∈ ((1 + 1)...𝑁)
178 disjsn 4648 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((1 + 1)...𝑁) ∩ {1}) = ∅ ↔ ¬ 1 ∈ ((1 + 1)...𝑁))
179177, 178mpbir 230 . . . . . . . . . . . . . . . . . . . . . . 23 (((1 + 1)...𝑁) ∩ {1}) = ∅
180 f1oun 6744 . . . . . . . . . . . . . . . . . . . . . . 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}))
181179, 180mpanr2 701 . . . . . . . . . . . . . . . . . . . . . 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}))
182159, 161, 170, 181syl21anc 835 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}):((1...(𝑁 − 1)) ∪ {𝑁})–1-1-onto→(((1 + 1)...𝑁) ∪ {1}))
18330a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ∈ V)
18466, 62eleqtrdi 2850 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑁 ∈ (ℤ‘1))
18569, 184eqeltrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘1))
186 uzid 12606 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
187 peano2uz 12650 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
188117, 186, 1873syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
18969, 188eqeltrrd 2841 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
190 fzsplit2 13290 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑁 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
191185, 189, 190syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
19269oveq1d 7299 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
193 fzsn 13307 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
194115, 193syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑁...𝑁) = {𝑁})
195192, 194eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
196195uneq2d 4098 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁}))
197191, 196eqtr2d 2780 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁))
198 iftrue 4466 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑁 → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = 1)
199198adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑛 = 𝑁) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = 1)
20066, 183, 197, 199fmptapd 7052 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∪ {⟨𝑁, 1⟩}) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))
201 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑁 → (𝑛 ∈ (1...(𝑁 − 1)) ↔ 𝑁 ∈ (1...(𝑁 − 1))))
202201notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑁 → (¬ 𝑛 ∈ (1...(𝑁 − 1)) ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1))))
203168, 202syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑛 = 𝑁 → ¬ 𝑛 ∈ (1...(𝑁 − 1))))
204203necon2ad 2959 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛𝑁))
205204imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → 𝑛𝑁)
206 ifnefalse 4472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛𝑁 → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1))
207205, 206syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑛 ∈ (1...(𝑁 − 1))) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1))
208207mpteq2dva 5175 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)))
209208uneq1d 4097 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∪ {⟨𝑁, 1⟩}) = ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}))
210200, 209eqtr3d 2781 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}))
211191, 196eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁}))
212 uzid 12606 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℤ → 1 ∈ (ℤ‘1))
213 peano2uz 12650 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ (ℤ‘1) → (1 + 1) ∈ (ℤ‘1))
214118, 212, 213mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 + 1) ∈ (ℤ‘1)
215 fzsplit2 13290 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘1)) → (1...𝑁) = ((1...1) ∪ ((1 + 1)...𝑁)))
216214, 184, 215sylancr 587 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑁) = ((1...1) ∪ ((1 + 1)...𝑁)))
217 fzsn 13307 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 ∈ ℤ → (1...1) = {1})
218118, 217ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1...1) = {1}
219218uneq1i 4094 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1...1) ∪ ((1 + 1)...𝑁)) = ({1} ∪ ((1 + 1)...𝑁))
220219equncomi 4090 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...1) ∪ ((1 + 1)...𝑁)) = (((1 + 1)...𝑁) ∪ {1})
221216, 220eqtrdi 2795 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1...𝑁) = (((1 + 1)...𝑁) ∪ {1}))
222210, 211, 221f1oeq123d 6719 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {⟨𝑁, 1⟩}):((1...(𝑁 − 1)) ∪ {𝑁})–1-1-onto→(((1 + 1)...𝑁) ∪ {1})))
223182, 222mpbird 256 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁))
224 f1oco 6748 . . . . . . . . . . . . . . . . . . . 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...𝑁))
22542, 223, 224syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁))
226 dff1o3 6731 . . . . . . . . . . . . . . . . . . . 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))))))
227226simprbi 497 . . . . . . . . . . . . . . . . . . 19 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))))
228225, 227syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → Fun ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))))
229 imain 6526 . . . . . . . . . . . . . . . . . 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)...𝑁))))
230228, 229syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))))
23148nn0red 12303 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
232231ltp1d 11914 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 < (𝑦 + 1))
233 fzdisj 13292 . . . . . . . . . . . . . . . . . . . 20 (𝑦 < (𝑦 + 1) → ((1...𝑦) ∩ ((𝑦 + 1)...𝑁)) = ∅)
234232, 233syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → ((1...𝑦) ∩ ((𝑦 + 1)...𝑁)) = ∅)
235234imaeq2d 5972 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0...(𝑁 − 1)) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ∅))
236 ima0 5988 . . . . . . . . . . . . . . . . . 18 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ∅) = ∅
237235, 236eqtrdi 2795 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = ∅)
238230, 237sylan9req 2800 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))) = ∅)
239 imassrn 5983 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)) ⊆ ran (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))
240 f1of 6725 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁) → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)⟶(1...𝑁))
241 frn 6616 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)⟶(1...𝑁) → ran (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ⊆ (1...𝑁))
242223, 240, 2413syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ran (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ⊆ (1...𝑁))
243239, 242sstrid 3933 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)) ⊆ (1...𝑁))
244243adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)) ⊆ (1...𝑁))
245 elfz1end 13295 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
24666, 245sylib 217 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑁 ∈ (1...𝑁))
247 eqid 2739 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))
248198, 247, 30fvmpt 6884 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (1...𝑁) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) = 1)
249246, 248syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) = 1)
250249adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) = 1)
251 f1ofn 6726 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁) → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁))
252223, 251syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁))
253252adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁))
254 fzss1 13304 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
25563, 254syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
256255adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
257 eluzfz2 13273 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (ℤ‘(𝑦 + 1)) → 𝑁 ∈ ((𝑦 + 1)...𝑁))
25875, 257syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑦 + 1)...𝑁))
259 fnfvima 7118 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁) ∧ ((𝑦 + 1)...𝑁) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑦 + 1)...𝑁)) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)))
260253, 256, 258, 259syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁) ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)))
261250, 260eqeltrrd 2841 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 1 ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)))
262 fnfvima 7118 . . . . . . . . . . . . . . . . . 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)...𝑁))))
263100, 244, 261, 262syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇))‘1) ∈ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁))))
264 imaco 6159 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...𝑁)))
265263, 264eleqtrrdi 2851 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇))‘1) ∈ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)))
266 fnconstg 6671 . . . . . . . . . . . . . . . . . 18 (1 ∈ V → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)))
26730, 266ax-mp 5 . . . . . . . . . . . . . . . . 17 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦))
268 fnconstg 6671 . . . . . . . . . . . . . . . . . 18 (0 ∈ V → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)))
26933, 268ax-mp 5 . . . . . . . . . . . . . . . . 17 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))
270 fvun2 6869 . . . . . . . . . . . . . . . . 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)))
271267, 269, 270mp3an12 1450 . . . . . . . . . . . . . . . 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)))
272238, 265, 271syl2anc 584 . . . . . . . . . . . . . . 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)))
27333fvconst2 7088 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇))‘1) ∈ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘1)) = 0)
274265, 273syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘1)) = 0)
275272, 274eqtrd 2779 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘1)) = 0)
276275oveq2d 7300 . . . . . . . . . . . . 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))
27797, 113, 2763eqtr4a 2805 . . . . . . . . . . . 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))))
278 fveq2 6783 . . . . . . . . . . . . 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)))
279 fveq2 6783 . . . . . . . . . . . . . 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)))
280279oveq2d 7300 . . . . . . . . . . . . 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))))
281278, 280eqeq12d 2755 . . . . . . . . . . . 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)))))
282277, 281syl5ibrcom 246 . . . . . . . . . . 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}))‘𝑛))))
283282imp 407 . . . . . . . . . 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}))‘𝑛)))
284283adantlr 712 . . . . . . . . 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}))‘𝑛)))
285 eldifsn 4721 . . . . . . . . . . . . . 14 (𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ↔ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘1)))
286 df-ne 2945 . . . . . . . . . . . . . . 15 (𝑛 ≠ ((2nd ‘(1st𝑇))‘1) ↔ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1))
287286anbi2i 623 . . . . . . . . . . . . . 14 ((𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘1)) ↔ (𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1)))
288285, 287bitri 274 . . . . . . . . . . . . 13 (𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ↔ (𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘1)))
289 fnconstg 6671 . . . . . . . . . . . . . . . . . 18 (1 ∈ V → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
29030, 289ax-mp 5 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1)))
291290, 35pm3.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)...𝑁)))
292 imain 6526 . . . . . . . . . . . . . . . . . 18 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
29345, 292syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
294 fzdisj 13292 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 + 1) < ((𝑦 + 1) + 1) → (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
29552, 294syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
296295imaeq2d 5972 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
297296, 56eqtrdi 2795 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ∅)
298293, 297sylan9req 2800 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∩ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅)
299 fnun 6554 . . . . . . . . . . . . . . . 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)...𝑁))))
300291, 298, 299sylancr 587 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
301 imaundi 6058 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
302 fzpred 13313 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ‘1) → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁)))
303184, 302syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁)))
304 uncom 4088 . . . . . . . . . . . . . . . . . . . . . . . 24 ({1} ∪ ((1 + 1)...𝑁)) = (((1 + 1)...𝑁) ∪ {1})
305303, 304eqtrdi 2795 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑁) = (((1 + 1)...𝑁) ∪ {1}))
306305difeq1d 4057 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...𝑁) ∖ {1}) = ((((1 + 1)...𝑁) ∪ {1}) ∖ {1}))
307 difun2 4415 . . . . . . . . . . . . . . . . . . . . . . 23 ((((1 + 1)...𝑁) ∪ {1}) ∖ {1}) = (((1 + 1)...𝑁) ∖ {1})
308 disj3 4388 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((1 + 1)...𝑁) ∩ {1}) = ∅ ↔ ((1 + 1)...𝑁) = (((1 + 1)...𝑁) ∖ {1}))
309179, 308mpbi 229 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 + 1)...𝑁) = (((1 + 1)...𝑁) ∖ {1})
310307, 309eqtr4i 2770 . . . . . . . . . . . . . . . . . . . . . 22 ((((1 + 1)...𝑁) ∪ {1}) ∖ {1}) = ((1 + 1)...𝑁)
311306, 310eqtrdi 2795 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((1...𝑁) ∖ {1}) = ((1 + 1)...𝑁))
312311adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1...𝑁) ∖ {1}) = ((1 + 1)...𝑁))
313 eluzp1p1 12619 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1) + 1) ∈ (ℤ‘(1 + 1)))
31463, 313syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ (ℤ‘(1 + 1)))
315 fzsplit2 13290 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 + 1) + 1) ∈ (ℤ‘(1 + 1)) ∧ 𝑁 ∈ (ℤ‘(𝑦 + 1))) → ((1 + 1)...𝑁) = (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
316314, 75, 315syl2an2 683 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1 + 1)...𝑁) = (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
317312, 316eqtrd 2779 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1...𝑁) ∖ {1}) = (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
318317imaeq2d 5972 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))))
319 imadif 6525 . . . . . . . . . . . . . . . . . . . . 21 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {1})))
32045, 319syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {1})))
321 eluzfz1 13272 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ‘1) → 1 ∈ (1...𝑁))
322184, 321syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 ∈ (1...𝑁))
323 fnsnfv 6856 . . . . . . . . . . . . . . . . . . . . . . 23 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ 1 ∈ (1...𝑁)) → {((2nd ‘(1st𝑇))‘1)} = ((2nd ‘(1st𝑇)) “ {1}))
32499, 322, 323syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {((2nd ‘(1st𝑇))‘1)} = ((2nd ‘(1st𝑇)) “ {1}))
325324eqcomd 2745 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((2nd ‘(1st𝑇)) “ {1}) = {((2nd ‘(1st𝑇))‘1)})
32681, 325difeq12d 4059 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {1})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
327320, 326eqtrd 2779 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
328327adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {1})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
329318, 328eqtr3d 2781 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (((1 + 1)...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
330301, 329eqtr3id 2793 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
331330fneq2d 6536 . . . . . . . . . . . . . . 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)})))
332300, 331mpbid 231 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}))
333 disjdifr 4407 . . . . . . . . . . . . . . 15 (((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘1)}) ∩ {((2nd ‘(1st𝑇))‘1)}) = ∅
334 fnconstg 6671 . . . . . . . . . . . . . . . . . 18 (1 ∈ V → ({((2nd ‘(1st𝑇))‘1)} × {1}) Fn {((2nd ‘(1st𝑇))‘1)})
33530, 334ax-mp 5 . . . . . . . . . . . . . . . . 17 ({((2nd ‘(1st𝑇))‘1)} × {1}) Fn {((2nd ‘(1st𝑇))‘1)}
336 fvun1 6868 . . . . . . . . . . . . . . . . 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}))‘𝑛))
337335, 336mp3an2 1448 . . . . . . . . . . . . . . . 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}))‘𝑛))
338 fnconstg 6671 . . . . . . . . . . . . . . . . . 18 (0 ∈ V → ({((2nd ‘(1st𝑇))‘1)} × {0}) Fn {((2nd ‘(1st𝑇))‘1)})
33933, 338ax-mp 5 . . . . . . . . . . . . . . . . 17 ({((2nd ‘(1st𝑇))‘1)} × {0}) Fn {((2nd ‘(1st𝑇))‘1)}
340 fvun1 6868 . . . . . . . . . . . . . . . . 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}))‘𝑛))
341339, 340mp3an2 1448 . . . . . . . . . . . . . . . 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}))‘𝑛))
342337, 341eqtr4d 2782 . . . . . . . . . . . . . . 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}))‘𝑛))
343333, 342mpanr1 700 . . . . . . . . . . . . . 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}))‘𝑛))
344332, 343sylan 580 . . . . . . . . . . . . 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}))‘𝑛))
345288, 344sylan2br 595 . . . . . . . . . . . 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}))‘𝑛))
346345anassrs 468 . . . . . . . . . . 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}))‘𝑛))
347 fzpred 13313 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 + 1) ∈ (ℤ‘1) → (1...(𝑦 + 1)) = ({1} ∪ ((1 + 1)...(𝑦 + 1))))
34863, 347syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (0...(𝑁 − 1)) → (1...(𝑦 + 1)) = ({1} ∪ ((1 + 1)...(𝑦 + 1))))
349348imaeq2d 5972 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) = ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))))
350349adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) = ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))))
351324uneq1d 4097 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1)))) = (((2nd ‘(1st𝑇)) “ {1}) ∪ ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1)))))
352 uncom 4088 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) = ({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
353 imaundi 6058 . . . . . . . . . . . . . . . . . . . 20 ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))) = (((2nd ‘(1st𝑇)) “ {1}) ∪ ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
354351, 352, 3533eqtr4g 2804 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) = ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))))
355354adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) = ((2nd ‘(1st𝑇)) “ ({1} ∪ ((1 + 1)...(𝑦 + 1)))))
356350, 355eqtr4d 2782 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}))
357356xpeq1d 5619 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) = ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) × {1}))
358 xpundir 5657 . . . . . . . . . . . . . . . 16 ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) ∪ {((2nd ‘(1st𝑇))‘1)}) × {1}) = ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1}))
359357, 358eqtrdi 2795 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) = ((((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘1)} × {1})))
360359uneq1d 4097 . . . . . . . . . . . . . 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})))
361 un23 4103 . . . . . . . . . . . . . 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}))
362360, 361eqtrdi 2795 . . . . . . . . . . . . 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})))
363362fveq1d 6785 . . . . . . . . . . . 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}))‘𝑛))
364363ad2antrr 723 . . . . . . . . . . 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}))‘𝑛))
365 imaco 6159 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦)))
366 df-ima 5603 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦)) = ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ (1...𝑦))
367 peano2uz 12650 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 − 1) ∈ (ℤ𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
36871, 367syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
369368adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
37070, 369eqeltrrd 2841 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ𝑦))
371 fzss2 13305 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ𝑦) → (1...𝑦) ⊆ (1...𝑁))
372370, 371syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑦) ⊆ (1...𝑁))
373372resmptd 5951 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ (1...𝑦)) = (𝑛 ∈ (1...𝑦) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))
374 fzss2 13305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑁 − 1) ∈ (ℤ𝑦) → (1...𝑦) ⊆ (1...(𝑁 − 1)))
37571, 374syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ (0...(𝑁 − 1)) → (1...𝑦) ⊆ (1...(𝑁 − 1)))
376375adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑦) ⊆ (1...(𝑁 − 1)))
377168adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
378376, 377ssneldd 3925 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ¬ 𝑁 ∈ (1...𝑦))
379 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑁 → (𝑛 ∈ (1...𝑦) ↔ 𝑁 ∈ (1...𝑦)))
380379notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑁 → (¬ 𝑛 ∈ (1...𝑦) ↔ ¬ 𝑁 ∈ (1...𝑦)))
381378, 380syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 = 𝑁 → ¬ 𝑛 ∈ (1...𝑦)))
382381necon2ad 2959 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑦) → 𝑛𝑁))
383382imp 407 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑦)) → 𝑛𝑁)
384383, 206syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑦)) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1))
385384mpteq2dva 5175 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑦) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)))
386373, 385eqtrd 2779 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ (1...𝑦)) = (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)))
387386rneqd 5850 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ (1...𝑦)) = ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)))
388366, 387eqtrid 2791 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦)) = ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)))
389 eqid 2739 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) = (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1))
390389elrnmpt 5868 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ V → (𝑗 ∈ ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) ↔ ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1)))
391390elv 3439 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) ↔ ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1))
392 elfzelz 13265 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
393392adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℤ)
394 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ (1...𝑦)) → 𝑛 ∈ (1...𝑦))
395118jctl 524 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℤ → (1 ∈ ℤ ∧ 𝑦 ∈ ℤ))
396 elfzelz 13265 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ (1...𝑦) → 𝑛 ∈ ℤ)
397396, 118jctir 521 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ (1...𝑦) → (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
398 fzaddel 13299 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ (1...𝑦) ↔ (𝑛 + 1) ∈ ((1 + 1)...(𝑦 + 1))))
399395, 397, 398syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ (1...𝑦)) → (𝑛 ∈ (1...𝑦) ↔ (𝑛 + 1) ∈ ((1 + 1)...(𝑦 + 1))))
400394, 399mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ (1...𝑦)) → (𝑛 + 1) ∈ ((1 + 1)...(𝑦 + 1)))
401 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = (𝑛 + 1) → (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) ↔ (𝑛 + 1) ∈ ((1 + 1)...(𝑦 + 1))))
402400, 401syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ (1...𝑦)) → (𝑗 = (𝑛 + 1) → 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
403402rexlimdva 3214 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℤ → (∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1) → 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
404 elfzelz 13265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → 𝑗 ∈ ℤ)
405404zcnd 12436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → 𝑗 ∈ ℂ)
406 npcan1 11409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ ℂ → ((𝑗 − 1) + 1) = 𝑗)
407405, 406syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → ((𝑗 − 1) + 1) = 𝑗)
408407eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → (((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1)) ↔ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
409408ibir 267 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → ((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1)))
410409adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → ((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1)))
411 peano2zm 12372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
412404, 411syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → (𝑗 − 1) ∈ ℤ)
413412, 118jctir 521 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → ((𝑗 − 1) ∈ ℤ ∧ 1 ∈ ℤ))
414 fzaddel 13299 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ((𝑗 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝑗 − 1) ∈ (1...𝑦) ↔ ((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1))))
415395, 413, 414syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → ((𝑗 − 1) ∈ (1...𝑦) ↔ ((𝑗 − 1) + 1) ∈ ((1 + 1)...(𝑦 + 1))))
416410, 415mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → (𝑗 − 1) ∈ (1...𝑦))
417405adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → 𝑗 ∈ ℂ)
418406eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ ℂ → 𝑗 = ((𝑗 − 1) + 1))
419417, 418syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → 𝑗 = ((𝑗 − 1) + 1))
420 oveq1 7291 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑗 − 1) → (𝑛 + 1) = ((𝑗 − 1) + 1))
421420rspceeqv 3576 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑗 − 1) ∈ (1...𝑦) ∧ 𝑗 = ((𝑗 − 1) + 1)) → ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1))
422416, 419, 421syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))) → ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1))
423422ex 413 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℤ → (𝑗 ∈ ((1 + 1)...(𝑦 + 1)) → ∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1)))
424403, 423impbid 211 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℤ → (∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1) ↔ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
425393, 424syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (∃𝑛 ∈ (1...𝑦)𝑗 = (𝑛 + 1) ↔ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
426391, 425syl5bb 283 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑗 ∈ ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) ↔ 𝑗 ∈ ((1 + 1)...(𝑦 + 1))))
427426eqrdv 2737 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ran (𝑛 ∈ (1...𝑦) ↦ (𝑛 + 1)) = ((1 + 1)...(𝑦 + 1)))
428388, 427eqtrd 2779 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦)) = ((1 + 1)...(𝑦 + 1)))
429428imaeq2d 5972 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ (1...𝑦))) = ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
430365, 429eqtrid 2791 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) = ((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))))
431430xpeq1d 5619 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) = (((2nd ‘(1st𝑇)) “ ((1 + 1)...(𝑦 + 1))) × {1}))
432 imaundi 6058 . . . . . . . . . . . . . . . . . . 19 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1)))) = ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ {𝑁}) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...(𝑁 − 1))))
433 imaco 6159 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ {𝑁}) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁}))
434 imaco 6159 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...(𝑁 − 1))) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))))
435433, 434uneq12i 4096 . . . . . . . . . . . . . . . . . . 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)))))
436432, 435eqtri 2767 . . . . . . . . . . . . . . . . . 18 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1)))) = (((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})) ∪ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1)))))
437189adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
438 fzsplit2 13290 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)) ∧ 𝑁 ∈ (ℤ‘(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
43973, 437, 438syl2an2 683 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
440195uneq2d 4098 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}))
441440adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}))
442439, 441eqtrd 2779 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}))
443 uncom 4088 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}) = ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1)))
444442, 443eqtrdi 2795 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1))))
445444imaeq2d 5972 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) = (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ({𝑁} ∪ ((𝑦 + 1)...(𝑁 − 1)))))
446249sneqd 4574 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁)} = {1})
447 fnsnfv 6856 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) Fn (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → {((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁)} = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁}))
448252, 246, 447syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))‘𝑁)} = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁}))
449446, 448eqtr3d 2781 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {1} = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁}))
450449imaeq2d 5972 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((2nd ‘(1st𝑇)) “ {1}) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})))
451324, 450eqtrd 2779 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {((2nd ‘(1st𝑇))‘1)} = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})))
452451adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → {((2nd ‘(1st𝑇))‘1)} = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})))
453 df-ima 5603 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))) = ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ ((𝑦 + 1)...(𝑁 − 1)))
454 fzss1 13304 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1)...(𝑁 − 1)) ⊆ (1...(𝑁 − 1)))
45563, 454syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...(𝑁 − 1)) ⊆ (1...(𝑁 − 1)))
456 fzss2 13305 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
457189, 456syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
458455, 457sylan9ssr 3936 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...(𝑁 − 1)) ⊆ (1...𝑁))
459458resmptd 5951 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ ((𝑦 + 1)...(𝑁 − 1))) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))
460 elfzle2 13269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑁 ∈ ((𝑦 + 1)...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
461166, 460nsyl 140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ¬ 𝑁 ∈ ((𝑦 + 1)...(𝑁 − 1)))
462 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑁 → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ 𝑁 ∈ ((𝑦 + 1)...(𝑁 − 1))))
463462notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑁 → (¬ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ ¬ 𝑁 ∈ ((𝑦 + 1)...(𝑁 − 1))))
464461, 463syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝑛 = 𝑁 → ¬ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))))
465464con2d 134 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) → ¬ 𝑛 = 𝑁))
466465imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → ¬ 𝑛 = 𝑁)
467466iffalsed 4471 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1))
468467mpteq2dva 5175 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
469468adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
470459, 469eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ ((𝑦 + 1)...(𝑁 − 1))) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
471470rneqd 5850 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ↾ ((𝑦 + 1)...(𝑁 − 1))) = ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
472453, 471eqtrid 2791 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))) = ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
473 elfzelz 13265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → 𝑗 ∈ ℤ)
474473zcnd 12436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → 𝑗 ∈ ℂ)
475474, 406syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → ((𝑗 − 1) + 1) = 𝑗)
476475eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → (((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) ↔ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
477476ibir 267 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → ((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)))
478477adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → ((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)))
47950nnzd 12434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℤ)
480117, 479anim12ci 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1) ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ))
481473, 411syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → (𝑗 − 1) ∈ ℤ)
482481, 118jctir 521 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → ((𝑗 − 1) ∈ ℤ ∧ 1 ∈ ℤ))
483 fzaddel 13299 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑦 + 1) ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) ∧ ((𝑗 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝑗 − 1) ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ ((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
484480, 482, 483syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → ((𝑗 − 1) ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ ((𝑗 − 1) + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
485478, 484mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → (𝑗 − 1) ∈ ((𝑦 + 1)...(𝑁 − 1)))
486474, 418syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → 𝑗 = ((𝑗 − 1) + 1))
487486adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → 𝑗 = ((𝑗 − 1) + 1))
488420rspceeqv 3576 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑗 − 1) ∈ ((𝑦 + 1)...(𝑁 − 1)) ∧ 𝑗 = ((𝑗 − 1) + 1)) → ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1))
489485, 487, 488syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))) → ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1))
490489ex 413 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) → ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1)))
491 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)))
492 elfzelz 13265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) → 𝑛 ∈ ℤ)
493492, 118jctir 521 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) → (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
494 fzaddel 13299 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑦 + 1) ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
495480, 493, 494syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
496491, 495mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → (𝑛 + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)))
497 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = (𝑛 + 1) → (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) ↔ (𝑛 + 1) ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
498496, 497syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))) → (𝑗 = (𝑛 + 1) → 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
499498rexlimdva 3214 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1) → 𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1))))
500490, 499impbid 211 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) ↔ ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1)))
501 eqid 2739 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)) = (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1))
502501elrnmpt 5868 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ V → (𝑗 ∈ ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)) ↔ ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1)))
503502elv 3439 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)) ↔ ∃𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1))𝑗 = (𝑛 + 1))
504500, 503bitr4di 289 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑗 ∈ (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) ↔ 𝑗 ∈ ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1))))
505504eqrdv 2737 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) = ran (𝑛 ∈ ((𝑦 + 1)...(𝑁 − 1)) ↦ (𝑛 + 1)))
50669oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) = (((𝑦 + 1) + 1)...𝑁))
507506adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1) + 1)...((𝑁 − 1) + 1)) = (((𝑦 + 1) + 1)...𝑁))
508472, 505, 5073eqtr2rd 2786 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1) + 1)...𝑁) = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))))
509508imaeq2d 5972 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1)))))
510452, 509uneq12d 4099 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ {𝑁})) ∪ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) “ ((𝑦 + 1)...(𝑁 − 1))))))
511436, 445, 5103eqtr4a 2805 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) = ({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))))
512511xpeq1d 5619 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}) = (({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) × {0}))
513 xpundir 5657 . . . . . . . . . . . . . . . 16 (({((2nd ‘(1st𝑇))‘1)} ∪ ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) × {0}) = (({((2nd ‘(1st𝑇))‘1)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
514512, 513eqtrdi 2795 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}) = (({((2nd ‘(1st𝑇))‘1)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
515431, 514uneq12d 4099 . . . . . . . . . . . . . 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}))))
516 unass 4101 . . . . . . . . . . . . . . 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})))
517 un23 4103 . . . . . . . . . . . . . . 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}))
518516, 517eqtr3i 2769 . . . . . . . . . . . . . 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}))
519515, 518eqtrdi 2795 . . . . . . . . . . . . 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})))
520519fveq1d 6785 . . . . . . . . . . . 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}))‘𝑛))
521520ad2antrr 723 . . . . . . . . . . 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}))‘𝑛))
522346, 364, 5213eqtr4d 2789 . . . . . . . . . 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}))‘𝑛))
523 snssi 4742 . . . . . . . . . . . . . . 15 (1 ∈ ℂ → {1} ⊆ ℂ)
524138, 523ax-mp 5 . . . . . . . . . . . . . 14 {1} ⊆ ℂ
525 0cn 10976 . . . . . . . . . . . . . . 15 0 ∈ ℂ
526 snssi 4742 . . . . . . . . . . . . . . 15 (0 ∈ ℂ → {0} ⊆ ℂ)
527525, 526ax-mp 5 . . . . . . . . . . . . . 14 {0} ⊆ ℂ
528524, 527unssi 4120 . . . . . . . . . . . . 13 ({1} ∪ {0}) ⊆ ℂ
52930fconst 6669 . . . . . . . . . . . . . . . . 17 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦))⟶{1}
53033fconst 6669 . . . . . . . . . . . . . . . . 17 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))⟶{0}
531529, 530pm3.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})
532 fun 6645 . . . . . . . . . . . . . . . 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}))
533531, 238, 532sylancr 587 . . . . . . . . . . . . . . 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}))
534 imaundi 6058 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))) = ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)))
535 fzsplit2 13290 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑦)) → (1...𝑁) = ((1...𝑦) ∪ ((𝑦 + 1)...𝑁)))
53663, 370, 535syl2an2 683 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) = ((1...𝑦) ∪ ((𝑦 + 1)...𝑁)))
537536imaeq2d 5972 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑁)) = (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))))
538 f1ofo 6732 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–onto→(1...𝑁))
539 foima 6702 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–onto→(1...𝑁) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑁)) = (1...𝑁))
540225, 538, 5393syl 18 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑁)) = (1...𝑁))
541540adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑁)) = (1...𝑁))
542537, 541eqtr3d 2781 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))) = (1...𝑁))
543534, 542eqtr3id 2793 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))) = (1...𝑁))
544543feq2d 6595 . . . . . . . . . . . . . . 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})))
545533, 544mpbid 231 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
546545ffvelrnda 6970 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) ∈ ({1} ∪ {0}))
547528, 546sselid 3920 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) ∈ ℂ)
548547addid2d 11185 . . . . . . . . . . 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}))‘𝑛))
549548adantr 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}))‘𝑛))
550522, 549eqtr4d 2782 . . . . . . . . 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}))‘𝑛)))
55193, 95, 284, 550ifbothda 4498 . . . . . . . 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}))‘𝑛)))
552551oveq2d 7300 . . . . . . 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}))‘𝑛))))
553 elmapi 8646 . . . . . . . . . . . . 13 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
55426, 553syl 17 . . . . . . . . . . . 12 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
555554ffvelrnda 6970 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ (0..^𝐾))
556 elfzonn0 13441 . . . . . . . . . . 11 (((1st ‘(1st𝑇))‘𝑛) ∈ (0..^𝐾) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℕ0)
557555, 556syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℕ0)
558557nn0cnd 12304 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℂ)
559558adantlr 712 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℂ)
560138, 525ifcli 4507 . . . . . . . . 9 if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) ∈ ℂ
561560a1i 11 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0) ∈ ℂ)
562559, 561, 547addassd 11006 . . . . . . 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}))‘𝑛))))
563552, 562eqtr4d 2782 . . . . . 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}))‘𝑛)))
564563mpteq2dva 5175 . . . . 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}))‘𝑛))))
56591, 564eqtrd 2779 . . . 4 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) = (𝑛 ∈ (1...𝑁) ↦ ((((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0)) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))))
566 poimirlem18.4 . . . . . . . . . 10 (𝜑 → (2nd𝑇) = 0)
567566adantr 481 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (2nd𝑇) = 0)
568 elfzle1 13268 . . . . . . . . . 10 (𝑦 ∈ (0...(𝑁 − 1)) → 0 ≤ 𝑦)
569568adantl 482 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 0 ≤ 𝑦)
570567, 569eqbrtrd 5097 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (2nd𝑇) ≤ 𝑦)
571 0re 10986 . . . . . . . . . 10 0 ∈ ℝ
572566, 571eqeltrdi 2848 . . . . . . . . 9 (𝜑 → (2nd𝑇) ∈ ℝ)
573 lenlt 11062 . . . . . . . . 9 (((2nd𝑇) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((2nd𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd𝑇)))
574572, 231, 573syl2an 596 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd𝑇)))
575570, 574mpbid 231 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ¬ 𝑦 < (2nd𝑇))
576575iffalsed 4471 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = (𝑦 + 1))
577576csbeq1d 3837 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑦 + 1) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
578 ovex 7317 . . . . . 6 (𝑦 + 1) ∈ V
579 oveq2 7292 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → (1...𝑗) = (1...(𝑦 + 1)))
580579imaeq2d 5972 . . . . . . . . 9 (𝑗 = (𝑦 + 1) → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
581580xpeq1d 5619 . . . . . . . 8 (𝑗 = (𝑦 + 1) → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}))
582 oveq1 7291 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (𝑗 + 1) = ((𝑦 + 1) + 1))
583582oveq1d 7299 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → ((𝑗 + 1)...𝑁) = (((𝑦 + 1) + 1)...𝑁))
584583imaeq2d 5972 . . . . . . . . 9 (𝑗 = (𝑦 + 1) → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
585584xpeq1d 5619 . . . . . . . 8 (𝑗 = (𝑦 + 1) → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
586581, 585uneq12d 4099 . . . . . . 7 (𝑗 = (𝑦 + 1) → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
587586oveq2d 7300 . . . . . 6 (𝑗 = (𝑦 + 1) → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
588578, 587csbie 3869 . . . . 5 (𝑦 + 1) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
589577, 588eqtrdi 2795 . . . 4 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
590 ovexd 7319 . . . . 5 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0)) ∈ V)
591 fvexd 6798 . . . . 5 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) ∈ V)
592 eqidd 2740 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))) = (𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))))
593545ffnd 6610 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (1...𝑁))
594 nfcv 2908 . . . . . . . . . . 11 𝑛(2nd ‘(1st𝑇))
595 nfmpt1 5183 . . . . . . . . . . 11 𝑛(𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))
596594, 595nfco 5777 . . . . . . . . . 10 𝑛((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))
597 nfcv 2908 . . . . . . . . . 10 𝑛(1...𝑦)
598596, 597nfima 5980 . . . . . . . . 9 𝑛(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦))
599 nfcv 2908 . . . . . . . . 9 𝑛{1}
600598, 599nfxp 5623 . . . . . . . 8 𝑛((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1})
601 nfcv 2908 . . . . . . . . . 10 𝑛((𝑦 + 1)...𝑁)
602596, 601nfima 5980 . . . . . . . . 9 𝑛(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))
603 nfcv 2908 . . . . . . . . 9 𝑛{0}
604602, 603nfxp 5623 . . . . . . . 8 𝑛((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})
605600, 604nfun 4100 . . . . . . 7 𝑛(((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))
606605dffn5f 6849 . . . . . 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}))‘𝑛)))
607593, 606sylib 217 . . . . 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}))‘𝑛)))
60887, 590, 591, 592, 607offval2 7562 . . . 4 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))) ∘f + (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))) = (𝑛 ∈ (1...𝑁) ↦ ((((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0)) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))))
609565, 589, 6083eqtr4rd 2790 . . 3 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))) ∘f + (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
610609mpteq2dva 5175 . 2 (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))) ∘f + (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
61119, 610eqtr4d 2782 1 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st𝑇))‘1), 1, 0))) ∘f + (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1539  wcel 2107  {cab 2716  wne 2944  wral 3065  wrex 3066  ∃!wreu 3067  {crab 3069  Vcvv 3433  csb 3833  cdif 3885  cun 3886  cin 3887  wss 3888  c0 4257  ifcif 4460  {csn 4562  cop 4568   class class class wbr 5075  cmpt 5158   × cxp 5588  ccnv 5589  ran crn 5591  cres 5592  cima 5593  ccom 5594  Fun wfun 6431   Fn wfn 6432  wf 6433  ontowfo 6435  1-1-ontowf1o 6436  cfv 6437  (class class class)co 7284  f cof 7540  1st c1st 7838  2nd c2nd 7839  m cmap 8624  cc 10878  cr 10879  0cc0 10880  1c1 10881   + caddc 10883   < clt 11018  cle 11019  cmin 11214  cn 11982  0cn0 12242  cz 12328  cuz 12591  ...cfz 13248  ..^cfzo 13391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-of 7542  df-om 7722  df-1st 7840  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-er 8507  df-map 8626  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-nn 11983  df-n0 12243  df-z 12329  df-uz 12592  df-fz 13249  df-fzo 13392
This theorem is referenced by:  poimirlem17  35803
  Copyright terms: Public domain W3C validator