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

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

Proof of Theorem poimirlem19
StepHypRef Expression
1 poimirlem22.2 . . 3 (𝜑𝑇𝑆)
2 fveq2 6672 . . . . . . . . . . 11 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
32breq2d 5080 . . . . . . . . . 10 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
43ifbid 4491 . . . . . . . . 9 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
54csbeq1d 3889 . . . . . . . 8 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
6 2fveq3 6677 . . . . . . . . . 10 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
7 2fveq3 6677 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
87imaeq1d 5930 . . . . . . . . . . . 12 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
98xpeq1d 5586 . . . . . . . . . . 11 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
107imaeq1d 5930 . . . . . . . . . . . 12 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
1110xpeq1d 5586 . . . . . . . . . . 11 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
129, 11uneq12d 4142 . . . . . . . . . 10 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
136, 12oveq12d 7176 . . . . . . . . 9 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
1413csbeq2dv 3892 . . . . . . . 8 (𝑡 = 𝑇if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
155, 14eqtrd 2858 . . . . . . 7 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
1615mpteq2dv 5164 . . . . . 6 (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
1716eqeq2d 2834 . . . . 5 (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
18 poimirlem22.s . . . . 5 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
1917, 18elrab2 3685 . . . 4 (𝑇𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
2019simprbi 499 . . 3 (𝑇𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
211, 20syl 17 . 2 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
22 elrabi 3677 . . . . . . . . . . . 12 (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
2322, 18eleq2s 2933 . . . . . . . . . . 11 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
241, 23syl 17 . . . . . . . . . 10 (𝜑𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
25 xp1st 7723 . . . . . . . . . 10 (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
2624, 25syl 17 . . . . . . . . 9 (𝜑 → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
27 xp1st 7723 . . . . . . . . 9 ((1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
2826, 27syl 17 . . . . . . . 8 (𝜑 → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
29 elmapfn 8431 . . . . . . . 8 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑇)) Fn (1...𝑁))
3028, 29syl 17 . . . . . . 7 (𝜑 → (1st ‘(1st𝑇)) Fn (1...𝑁))
3130adantr 483 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1st ‘(1st𝑇)) Fn (1...𝑁))
32 1ex 10639 . . . . . . . . . 10 1 ∈ V
33 fnconstg 6569 . . . . . . . . . 10 (1 ∈ V → (((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑦)))
3432, 33ax-mp 5 . . . . . . . . 9 (((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑦))
35 c0ex 10637 . . . . . . . . . 10 0 ∈ V
36 fnconstg 6569 . . . . . . . . . 10 (0 ∈ V → (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)))
3735, 36ax-mp 5 . . . . . . . . 9 (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁))
3834, 37pm3.2i 473 . . . . . . . 8 ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑦)) ∧ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)))
39 xp2nd 7724 . . . . . . . . . . . . 13 ((1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
4026, 39syl 17 . . . . . . . . . . . 12 (𝜑 → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
41 fvex 6685 . . . . . . . . . . . . 13 (2nd ‘(1st𝑇)) ∈ V
42 f1oeq1 6606 . . . . . . . . . . . . 13 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
4341, 42elab 3669 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
4440, 43sylib 220 . . . . . . . . . . 11 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
45 dff1o3 6623 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑇))))
4645simprbi 499 . . . . . . . . . . 11 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑇)))
4744, 46syl 17 . . . . . . . . . 10 (𝜑 → Fun (2nd ‘(1st𝑇)))
48 imain 6441 . . . . . . . . . 10 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁))))
4947, 48syl 17 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁))))
50 elfznn0 13003 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ0)
5150nn0red 11959 . . . . . . . . . . . . 13 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
5251ltp1d 11572 . . . . . . . . . . . 12 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 < (𝑦 + 1))
53 fzdisj 12937 . . . . . . . . . . . 12 (𝑦 < (𝑦 + 1) → ((1...𝑦) ∩ ((𝑦 + 1)...𝑁)) = ∅)
5452, 53syl 17 . . . . . . . . . . 11 (𝑦 ∈ (0...(𝑁 − 1)) → ((1...𝑦) ∩ ((𝑦 + 1)...𝑁)) = ∅)
5554imaeq2d 5931 . . . . . . . . . 10 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
56 ima0 5947 . . . . . . . . . 10 ((2nd ‘(1st𝑇)) “ ∅) = ∅
5755, 56syl6eq 2874 . . . . . . . . 9 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ ((1...𝑦) ∩ ((𝑦 + 1)...𝑁))) = ∅)
5849, 57sylan9req 2879 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁))) = ∅)
59 fnun 6465 . . . . . . . 8 ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑦)) ∧ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁))) ∧ (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁))) = ∅) → ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁))))
6038, 58, 59sylancr 589 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁))))
61 imaundi 6010 . . . . . . . . 9 ((2nd ‘(1st𝑇)) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)))
62 nn0p1nn 11939 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ0 → (𝑦 + 1) ∈ ℕ)
6350, 62syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℕ)
64 nnuz 12284 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
6563, 64eleqtrdi 2925 . . . . . . . . . . . . 13 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (ℤ‘1))
6665adantl 484 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ (ℤ‘1))
67 poimir.0 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ)
6867nncnd 11656 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℂ)
69 npcan1 11067 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
7068, 69syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
7170adantr 483 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
72 elfzuz3 12908 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ𝑦))
73 peano2uz 12304 . . . . . . . . . . . . . . 15 ((𝑁 − 1) ∈ (ℤ𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
7472, 73syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
7574adantl 484 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
7671, 75eqeltrrd 2916 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ𝑦))
77 fzsplit2 12935 . . . . . . . . . . . 12 (((𝑦 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑦)) → (1...𝑁) = ((1...𝑦) ∪ ((𝑦 + 1)...𝑁)))
7866, 76, 77syl2anc 586 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) = ((1...𝑦) ∪ ((𝑦 + 1)...𝑁)))
7978imaeq2d 5931 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))))
80 f1ofo 6624 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
81 foima 6597 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
8244, 80, 813syl 18 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
8382adantr 483 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
8479, 83eqtr3d 2860 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((1...𝑦) ∪ ((𝑦 + 1)...𝑁))) = (1...𝑁))
8561, 84syl5eqr 2872 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁))) = (1...𝑁))
8685fneq2d 6449 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁))) ↔ ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (1...𝑁)))
8760, 86mpbid 234 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) Fn (1...𝑁))
88 ovexd 7193 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) ∈ V)
89 inidm 4197 . . . . . 6 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
90 eqidd 2824 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) = ((1st ‘(1st𝑇))‘𝑛))
91 eqidd 2824 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))
9231, 87, 88, 88, 89, 90, 91offval 7418 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))) = (𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))))
93 elmapi 8430 . . . . . . . . . . . . 13 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
9428, 93syl 17 . . . . . . . . . . . 12 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
9594ffvelrnda 6853 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ (0..^𝐾))
96 elfzonn0 13085 . . . . . . . . . . 11 (((1st ‘(1st𝑇))‘𝑛) ∈ (0..^𝐾) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℕ0)
9795, 96syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℕ0)
9897nn0cnd 11960 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℂ)
9998adantlr 713 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) ∈ ℂ)
100 ax-1cn 10597 . . . . . . . . . 10 1 ∈ ℂ
101 0cn 10635 . . . . . . . . . 10 0 ∈ ℂ
102100, 101ifcli 4515 . . . . . . . . 9 if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0) ∈ ℂ
103102a1i 11 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0) ∈ ℂ)
104 snssi 4743 . . . . . . . . . . 11 (1 ∈ ℂ → {1} ⊆ ℂ)
105100, 104ax-mp 5 . . . . . . . . . 10 {1} ⊆ ℂ
106 snssi 4743 . . . . . . . . . . 11 (0 ∈ ℂ → {0} ⊆ ℂ)
107101, 106ax-mp 5 . . . . . . . . . 10 {0} ⊆ ℂ
108105, 107unssi 4163 . . . . . . . . 9 ({1} ∪ {0}) ⊆ ℂ
10932fconst 6567 . . . . . . . . . . . . 13 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1)))⟶{1}
11035fconst 6567 . . . . . . . . . . . . 13 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁))⟶{0}
111109, 110pm3.2i 473 . . . . . . . . . . . 12 (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1)))⟶{1} ∧ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁))⟶{0})
112 simpr 487 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ((1 + 1)...𝑁)) → 𝑛 ∈ ((1 + 1)...𝑁))
11367nnzd 12089 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑁 ∈ ℤ)
114 1z 12015 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℤ
115 peano2z 12026 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 ∈ ℤ → (1 + 1) ∈ ℤ)
116114, 115ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (1 + 1) ∈ ℤ
117113, 116jctil 522 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ))
118 elfzelz 12911 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ((1 + 1)...𝑁) → 𝑛 ∈ ℤ)
119118, 114jctir 523 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ((1 + 1)...𝑁) → (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
120 fzsubel 12946 . . . . . . . . . . . . . . . . . . . . . 22 ((((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ ((1 + 1)...𝑁) ↔ (𝑛 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
121117, 119, 120syl2an 597 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ((1 + 1)...𝑁)) → (𝑛 ∈ ((1 + 1)...𝑁) ↔ (𝑛 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
122112, 121mpbid 234 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ((1 + 1)...𝑁)) → (𝑛 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1)))
123100, 100pncan3oi 10904 . . . . . . . . . . . . . . . . . . . . 21 ((1 + 1) − 1) = 1
124123oveq1i 7168 . . . . . . . . . . . . . . . . . . . 20 (((1 + 1) − 1)...(𝑁 − 1)) = (1...(𝑁 − 1))
125122, 124eleqtrdi 2925 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ((1 + 1)...𝑁)) → (𝑛 − 1) ∈ (1...(𝑁 − 1)))
126125ralrimiva 3184 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑛 ∈ ((1 + 1)...𝑁)(𝑛 − 1) ∈ (1...(𝑁 − 1)))
127 simpr 487 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (1...(𝑁 − 1))) → 𝑦 ∈ (1...(𝑁 − 1)))
128 peano2zm 12028 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
129113, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑁 − 1) ∈ ℤ)
130129, 114jctil 522 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ))
131 elfzelz 12911 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (1...(𝑁 − 1)) → 𝑦 ∈ ℤ)
132131, 114jctir 523 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (1...(𝑁 − 1)) → (𝑦 ∈ ℤ ∧ 1 ∈ ℤ))
133 fzaddel 12944 . . . . . . . . . . . . . . . . . . . . . . 23 (((1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) ∧ (𝑦 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑦 ∈ (1...(𝑁 − 1)) ↔ (𝑦 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1))))
134130, 132, 133syl2an 597 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (1...(𝑁 − 1))) → (𝑦 ∈ (1...(𝑁 − 1)) ↔ (𝑦 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1))))
135127, 134mpbid 234 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (1...(𝑁 − 1))) → (𝑦 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1)))
13670oveq2d 7174 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 + 1)...𝑁))
137136adantr 483 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (1...(𝑁 − 1))) → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 + 1)...𝑁))
138135, 137eleqtrd 2917 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (1...(𝑁 − 1))) → (𝑦 + 1) ∈ ((1 + 1)...𝑁))
139118zcnd 12091 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ((1 + 1)...𝑁) → 𝑛 ∈ ℂ)
140131zcnd 12091 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (1...(𝑁 − 1)) → 𝑦 ∈ ℂ)
141 subadd2 10892 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑛 − 1) = 𝑦 ↔ (𝑦 + 1) = 𝑛))
142100, 141mp3an2 1445 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑛 − 1) = 𝑦 ↔ (𝑦 + 1) = 𝑛))
143 eqcom 2830 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (𝑛 − 1) ↔ (𝑛 − 1) = 𝑦)
144 eqcom 2830 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = (𝑦 + 1) ↔ (𝑦 + 1) = 𝑛)
145142, 143, 1443bitr4g 316 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑦 = (𝑛 − 1) ↔ 𝑛 = (𝑦 + 1)))
146139, 140, 145syl2anr 598 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ (1...(𝑁 − 1)) ∧ 𝑛 ∈ ((1 + 1)...𝑁)) → (𝑦 = (𝑛 − 1) ↔ 𝑛 = (𝑦 + 1)))
147146ralrimiva 3184 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (1...(𝑁 − 1)) → ∀𝑛 ∈ ((1 + 1)...𝑁)(𝑦 = (𝑛 − 1) ↔ 𝑛 = (𝑦 + 1)))
148147adantl 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (1...(𝑁 − 1))) → ∀𝑛 ∈ ((1 + 1)...𝑁)(𝑦 = (𝑛 − 1) ↔ 𝑛 = (𝑦 + 1)))
149 reu6i 3721 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 + 1) ∈ ((1 + 1)...𝑁) ∧ ∀𝑛 ∈ ((1 + 1)...𝑁)(𝑦 = (𝑛 − 1) ↔ 𝑛 = (𝑦 + 1))) → ∃!𝑛 ∈ ((1 + 1)...𝑁)𝑦 = (𝑛 − 1))
150138, 148, 149syl2anc 586 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (1...(𝑁 − 1))) → ∃!𝑛 ∈ ((1 + 1)...𝑁)𝑦 = (𝑛 − 1))
151150ralrimiva 3184 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑦 ∈ (1...(𝑁 − 1))∃!𝑛 ∈ ((1 + 1)...𝑁)𝑦 = (𝑛 − 1))
152 eqid 2823 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) = (𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1))
153152f1ompt 6877 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)):((1 + 1)...𝑁)–1-1-onto→(1...(𝑁 − 1)) ↔ (∀𝑛 ∈ ((1 + 1)...𝑁)(𝑛 − 1) ∈ (1...(𝑁 − 1)) ∧ ∀𝑦 ∈ (1...(𝑁 − 1))∃!𝑛 ∈ ((1 + 1)...𝑁)𝑦 = (𝑛 − 1)))
154126, 151, 153sylanbrc 585 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)):((1 + 1)...𝑁)–1-1-onto→(1...(𝑁 − 1)))
155 f1osng 6657 . . . . . . . . . . . . . . . . . 18 ((1 ∈ V ∧ 𝑁 ∈ ℕ) → {⟨1, 𝑁⟩}:{1}–1-1-onto→{𝑁})
15632, 67, 155sylancr 589 . . . . . . . . . . . . . . . . 17 (𝜑 → {⟨1, 𝑁⟩}:{1}–1-1-onto→{𝑁})
15767nnred 11655 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑁 ∈ ℝ)
158157ltm1d 11574 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑁 − 1) < 𝑁)
159129zred 12090 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑁 − 1) ∈ ℝ)
160159, 157ltnled 10789 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
161158, 160mpbid 234 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
162 elfzle2 12914 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
163161, 162nsyl 142 . . . . . . . . . . . . . . . . . 18 (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
164 disjsn 4649 . . . . . . . . . . . . . . . . . 18 (((1...(𝑁 − 1)) ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1)))
165163, 164sylibr 236 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅)
166 1re 10643 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℝ
167166ltp1i 11546 . . . . . . . . . . . . . . . . . . . . 21 1 < (1 + 1)
168116zrei 11990 . . . . . . . . . . . . . . . . . . . . . 22 (1 + 1) ∈ ℝ
169166, 168ltnlei 10763 . . . . . . . . . . . . . . . . . . . . 21 (1 < (1 + 1) ↔ ¬ (1 + 1) ≤ 1)
170167, 169mpbi 232 . . . . . . . . . . . . . . . . . . . 20 ¬ (1 + 1) ≤ 1
171 elfzle1 12913 . . . . . . . . . . . . . . . . . . . 20 (1 ∈ ((1 + 1)...𝑁) → (1 + 1) ≤ 1)
172170, 171mto 199 . . . . . . . . . . . . . . . . . . 19 ¬ 1 ∈ ((1 + 1)...𝑁)
173 disjsn 4649 . . . . . . . . . . . . . . . . . . 19 ((((1 + 1)...𝑁) ∩ {1}) = ∅ ↔ ¬ 1 ∈ ((1 + 1)...𝑁))
174172, 173mpbir 233 . . . . . . . . . . . . . . . . . 18 (((1 + 1)...𝑁) ∩ {1}) = ∅
175 f1oun 6636 . . . . . . . . . . . . . . . . . 18 ((((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)):((1 + 1)...𝑁)–1-1-onto→(1...(𝑁 − 1)) ∧ {⟨1, 𝑁⟩}:{1}–1-1-onto→{𝑁}) ∧ ((((1 + 1)...𝑁) ∩ {1}) = ∅ ∧ ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅)) → ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {⟨1, 𝑁⟩}):(((1 + 1)...𝑁) ∪ {1})–1-1-onto→((1...(𝑁 − 1)) ∪ {𝑁}))
176174, 175mpanr1 701 . . . . . . . . . . . . . . . . 17 ((((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)):((1 + 1)...𝑁)–1-1-onto→(1...(𝑁 − 1)) ∧ {⟨1, 𝑁⟩}:{1}–1-1-onto→{𝑁}) ∧ ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅) → ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {⟨1, 𝑁⟩}):(((1 + 1)...𝑁) ∪ {1})–1-1-onto→((1...(𝑁 − 1)) ∪ {𝑁}))
177154, 156, 165, 176syl21anc 835 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {⟨1, 𝑁⟩}):(((1 + 1)...𝑁) ∪ {1})–1-1-onto→((1...(𝑁 − 1)) ∪ {𝑁}))
178 eleq1 2902 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 1 → (𝑛 ∈ ((1 + 1)...𝑁) ↔ 1 ∈ ((1 + 1)...𝑁)))
179172, 178mtbiri 329 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 1 → ¬ 𝑛 ∈ ((1 + 1)...𝑁))
180179necon2ai 3047 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ((1 + 1)...𝑁) → 𝑛 ≠ 1)
181 ifnefalse 4481 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ≠ 1 → if(𝑛 = 1, 𝑁, (𝑛 − 1)) = (𝑛 − 1))
182180, 181syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ((1 + 1)...𝑁) → if(𝑛 = 1, 𝑁, (𝑛 − 1)) = (𝑛 − 1))
183182mpteq2ia 5159 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ((1 + 1)...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) = (𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1))
184183uneq1i 4137 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ((1 + 1)...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ∪ {⟨1, 𝑁⟩}) = ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {⟨1, 𝑁⟩})
18532a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 1 ∈ V)
186 ssv 3993 . . . . . . . . . . . . . . . . . . . 20 ℕ ⊆ V
187186, 67sseldi 3967 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ V)
18867, 64eleqtrdi 2925 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑁 ∈ (ℤ‘1))
189 fzpred 12958 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (ℤ‘1) → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁)))
190188, 189syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1...𝑁) = ({1} ∪ ((1 + 1)...𝑁)))
191 uncom 4131 . . . . . . . . . . . . . . . . . . . 20 ({1} ∪ ((1 + 1)...𝑁)) = (((1 + 1)...𝑁) ∪ {1})
192190, 191syl6req 2875 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((1 + 1)...𝑁) ∪ {1}) = (1...𝑁))
193 iftrue 4475 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → if(𝑛 = 1, 𝑁, (𝑛 − 1)) = 𝑁)
194193adantl 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 = 1) → if(𝑛 = 1, 𝑁, (𝑛 − 1)) = 𝑁)
195185, 187, 192, 194fmptapd 6935 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑛 ∈ ((1 + 1)...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ∪ {⟨1, 𝑁⟩}) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))
196184, 195syl5eqr 2872 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {⟨1, 𝑁⟩}) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))
19770, 188eqeltrd 2915 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘1))
198 uzid 12261 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
199 peano2uz 12304 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
200129, 198, 1993syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
20170, 200eqeltrrd 2916 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
202 fzsplit2 12935 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
203197, 201, 202syl2anc 586 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
20470oveq1d 7173 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁))
205 fzsn 12952 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁})
206113, 205syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑁...𝑁) = {𝑁})
207204, 206eqtrd 2858 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁})
208207uneq2d 4141 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁}))
209203, 208eqtr2d 2859 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁))
210196, 192, 209f1oeq123d 6612 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑛 ∈ ((1 + 1)...𝑁) ↦ (𝑛 − 1)) ∪ {⟨1, 𝑁⟩}):(((1 + 1)...𝑁) ∪ {1})–1-1-onto→((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))):(1...𝑁)–1-1-onto→(1...𝑁)))
211177, 210mpbid 234 . . . . . . . . . . . . . . 15 (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))):(1...𝑁)–1-1-onto→(1...𝑁))
212 f1oco 6639 . . . . . . . . . . . . . . 15 (((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...𝑁))
21344, 211, 212syl2anc 586 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))):(1...𝑁)–1-1-onto→(1...𝑁))
214 dff1o3 6623 . . . . . . . . . . . . . . 15 (((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))))))
215214simprbi 499 . . . . . . . . . . . . . 14 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))))
216 imain 6441 . . . . . . . . . . . . . 14 (Fun ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁))))
217213, 215, 2163syl 18 . . . . . . . . . . . . 13 (𝜑 → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁))))
21863nnred 11655 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℝ)
219218ltp1d 11572 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) < ((𝑦 + 1) + 1))
220 fzdisj 12937 . . . . . . . . . . . . . . . 16 ((𝑦 + 1) < ((𝑦 + 1) + 1) → ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
221219, 220syl 17 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0...(𝑁 − 1)) → ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
222221imaeq2d 5931 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ∅))
223 ima0 5947 . . . . . . . . . . . . . 14 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ∅) = ∅
224222, 223syl6eq 2874 . . . . . . . . . . . . 13 (𝑦 ∈ (0...(𝑁 − 1)) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ∅)
225217, 224sylan9req 2879 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁))) = ∅)
226 fun 6542 . . . . . . . . . . . 12 (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1)))⟶{1} ∧ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}):(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁))⟶{0}) ∧ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁))) = ∅) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (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) + 1)...𝑁)))⟶({1} ∪ {0}))
227111, 225, 226sylancr 589 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (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) + 1)...𝑁)))⟶({1} ∪ {0}))
228 imaundi 6010 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)))
22963peano2nnd 11657 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℕ)
230229, 64eleqtrdi 2925 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ (ℤ‘1))
231230adantl 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1) + 1) ∈ (ℤ‘1))
232 eluzp1p1 12273 . . . . . . . . . . . . . . . . . . 19 ((𝑁 − 1) ∈ (ℤ𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
23372, 232syl 17 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
234233adantl 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
23571, 234eqeltrrd 2916 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘(𝑦 + 1)))
236 fzsplit2 12935 . . . . . . . . . . . . . . . 16 ((((𝑦 + 1) + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘(𝑦 + 1))) → (1...𝑁) = ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
237231, 235, 236syl2anc 586 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) = ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁)))
238237imaeq2d 5931 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑁)) = (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))))
239 f1ofo 6624 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))):(1...𝑁)–1-1-onto→(1...𝑁) → ((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))):(1...𝑁)–onto→(1...𝑁))
240 foima 6597 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))):(1...𝑁)–onto→(1...𝑁) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑁)) = (1...𝑁))
241213, 239, 2403syl 18 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑁)) = (1...𝑁))
242241adantr 483 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...𝑁)) = (1...𝑁))
243238, 242eqtr3d 2860 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (1...𝑁))
244228, 243syl5eqr 2872 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁))) = (1...𝑁))
245244feq2d 6502 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (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) + 1)...𝑁)))⟶({1} ∪ {0}) ↔ (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})))
246227, 245mpbid 234 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
247246ffvelrnda 6853 . . . . . . . . 9 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) ∈ ({1} ∪ {0}))
248108, 247sseldi 3967 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) ∈ ℂ)
24999, 103, 248subadd23d 11021 . . . . . . 7 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((1st ‘(1st𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0)) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛)) = (((1st ‘(1st𝑇))‘𝑛) + (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0))))
250 oveq2 7166 . . . . . . . . . 10 (1 = if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0) → (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − 1) = (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0)))
251250eqeq1d 2825 . . . . . . . . 9 (1 = if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0) → ((((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − 1) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) ↔ (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0)) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)))
252 oveq2 7166 . . . . . . . . . 10 (0 = if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0) → (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − 0) = (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0)))
253252eqeq1d 2825 . . . . . . . . 9 (0 = if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0) → ((((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − 0) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) ↔ (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0)) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)))
254 1m1e0 11712 . . . . . . . . . . . . 13 (1 − 1) = 0
255 f1ofn 6618 . . . . . . . . . . . . . . . . . . . 20 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
25644, 255syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (2nd ‘(1st𝑇)) Fn (1...𝑁))
257256adantr 483 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
258 imassrn 5942 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ (1...(𝑦 + 1))) ⊆ ran (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))
259 f1of 6617 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))):(1...𝑁)–1-1-onto→(1...𝑁) → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))):(1...𝑁)⟶(1...𝑁))
260211, 259syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))):(1...𝑁)⟶(1...𝑁))
261260frnd 6523 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ran (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ⊆ (1...𝑁))
262258, 261sstrid 3980 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ (1...(𝑦 + 1))) ⊆ (1...𝑁))
263262adantr 483 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ (1...(𝑦 + 1))) ⊆ (1...𝑁))
264 eqidd 2824 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))
265 eluzfz1 12917 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ (ℤ‘1) → 1 ∈ (1...𝑁))
266188, 265syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ∈ (1...𝑁))
267264, 194, 266, 67fvmptd 6777 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))‘1) = 𝑁)
268267adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))‘1) = 𝑁)
269 f1ofn 6618 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))):(1...𝑁)–1-1-onto→(1...𝑁) → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) Fn (1...𝑁))
270211, 269syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) Fn (1...𝑁))
271270adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) Fn (1...𝑁))
272 fzss2 12950 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (ℤ‘(𝑦 + 1)) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
273235, 272syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
274 eluzfz1 12917 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 + 1) ∈ (ℤ‘1) → 1 ∈ (1...(𝑦 + 1)))
27565, 274syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0...(𝑁 − 1)) → 1 ∈ (1...(𝑦 + 1)))
276275adantl 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 1 ∈ (1...(𝑦 + 1)))
277 fnfvima 6997 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) Fn (1...𝑁) ∧ (1...(𝑦 + 1)) ⊆ (1...𝑁) ∧ 1 ∈ (1...(𝑦 + 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))‘1) ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ (1...(𝑦 + 1))))
278271, 273, 276, 277syl3anc 1367 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))‘1) ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ (1...(𝑦 + 1))))
279268, 278eqeltrrd 2916 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ (1...(𝑦 + 1))))
280 fnfvima 6997 . . . . . . . . . . . . . . . . . 18 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ (1...(𝑦 + 1))) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ (1...(𝑦 + 1)))) → ((2nd ‘(1st𝑇))‘𝑁) ∈ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ (1...(𝑦 + 1)))))
281257, 263, 279, 280syl3anc 1367 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇))‘𝑁) ∈ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ (1...(𝑦 + 1)))))
282 imaco 6106 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ (1...(𝑦 + 1))))
283281, 282eleqtrrdi 2926 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇))‘𝑁) ∈ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))))
284 fnconstg 6569 . . . . . . . . . . . . . . . . . 18 (1 ∈ V → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))))
28532, 284ax-mp 5 . . . . . . . . . . . . . . . . 17 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1)))
286 fnconstg 6569 . . . . . . . . . . . . . . . . . 18 (0 ∈ V → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)))
28735, 286ax-mp 5 . . . . . . . . . . . . . . . . 17 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁))
288 fvun1 6756 . . . . . . . . . . . . . . . . 17 ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) ∧ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) ∧ (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁))) = ∅ ∧ ((2nd ‘(1st𝑇))‘𝑁) ∈ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))))) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑁)) = (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1})‘((2nd ‘(1st𝑇))‘𝑁)))
289285, 287, 288mp3an12 1447 . . . . . . . . . . . . . . . 16 ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) ∩ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁))) = ∅ ∧ ((2nd ‘(1st𝑇))‘𝑁) ∈ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1)))) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑁)) = (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1})‘((2nd ‘(1st𝑇))‘𝑁)))
290225, 283, 289syl2anc 586 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑁)) = (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1})‘((2nd ‘(1st𝑇))‘𝑁)))
29132fvconst2 6968 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇))‘𝑁) ∈ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1})‘((2nd ‘(1st𝑇))‘𝑁)) = 1)
292283, 291syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1})‘((2nd ‘(1st𝑇))‘𝑁)) = 1)
293290, 292eqtrd 2858 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑁)) = 1)
294293oveq1d 7173 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑁)) − 1) = (1 − 1))
295 fzss1 12949 . . . . . . . . . . . . . . . . . 18 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
29665, 295syl 17 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
297296adantl 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
298 eluzfz2 12918 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘(𝑦 + 1)) → 𝑁 ∈ ((𝑦 + 1)...𝑁))
299235, 298syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑦 + 1)...𝑁))
300 fnfvima 6997 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ ((𝑦 + 1)...𝑁) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑦 + 1)...𝑁)) → ((2nd ‘(1st𝑇))‘𝑁) ∈ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)))
301257, 297, 299, 300syl3anc 1367 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇))‘𝑁) ∈ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)))
302 fvun2 6757 . . . . . . . . . . . . . . . 16 (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑦)) ∧ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) ∧ ((((2nd ‘(1st𝑇)) “ (1...𝑦)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁))) = ∅ ∧ ((2nd ‘(1st𝑇))‘𝑁) ∈ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)))) → (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑁)) = ((((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘𝑁)))
30334, 37, 302mp3an12 1447 . . . . . . . . . . . . . . 15 (((((2nd ‘(1st𝑇)) “ (1...𝑦)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁))) = ∅ ∧ ((2nd ‘(1st𝑇))‘𝑁) ∈ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁))) → (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑁)) = ((((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘𝑁)))
30458, 301, 303syl2anc 586 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑁)) = ((((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘𝑁)))
30535fvconst2 6968 . . . . . . . . . . . . . . 15 (((2nd ‘(1st𝑇))‘𝑁) ∈ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) → ((((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘𝑁)) = 0)
306301, 305syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘𝑁)) = 0)
307304, 306eqtrd 2858 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑁)) = 0)
308254, 294, 3073eqtr4a 2884 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑁)) − 1) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑁)))
309 fveq2 6672 . . . . . . . . . . . . . 14 (𝑛 = ((2nd ‘(1st𝑇))‘𝑁) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑁)))
310309oveq1d 7173 . . . . . . . . . . . . 13 (𝑛 = ((2nd ‘(1st𝑇))‘𝑁) → (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − 1) = (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑁)) − 1))
311 fveq2 6672 . . . . . . . . . . . . 13 (𝑛 = ((2nd ‘(1st𝑇))‘𝑁) → (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑁)))
312310, 311eqeq12d 2839 . . . . . . . . . . . 12 (𝑛 = ((2nd ‘(1st𝑇))‘𝑁) → ((((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − 1) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) ↔ (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑁)) − 1) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑁))))
313308, 312syl5ibrcom 249 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 = ((2nd ‘(1st𝑇))‘𝑁) → (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − 1) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)))
314313imp 409 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 = ((2nd ‘(1st𝑇))‘𝑁)) → (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − 1) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))
315314adantlr 713 . . . . . . . . 9 ((((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 = ((2nd ‘(1st𝑇))‘𝑁)) → (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − 1) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))
316248subid1d 10988 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − 0) = ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛))
317316adantr 483 . . . . . . . . . 10 ((((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘𝑁)) → (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − 0) = ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛))
318 eldifsn 4721 . . . . . . . . . . . . . 14 (𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}) ↔ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑁)))
319 df-ne 3019 . . . . . . . . . . . . . . 15 (𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑁) ↔ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘𝑁))
320319anbi2i 624 . . . . . . . . . . . . . 14 ((𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑁)) ↔ (𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘𝑁)))
321318, 320bitri 277 . . . . . . . . . . . . 13 (𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}) ↔ (𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘𝑁)))
322 fnconstg 6569 . . . . . . . . . . . . . . . . . 18 (0 ∈ V → (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))))
32335, 322ax-mp 5 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1)))
32434, 323pm3.2i 473 . . . . . . . . . . . . . . . 16 ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑦)) ∧ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))))
325 imain 6441 . . . . . . . . . . . . . . . . . 18 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...𝑦) ∩ ((𝑦 + 1)...(𝑁 − 1)))) = (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1)))))
32647, 325syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑦) ∩ ((𝑦 + 1)...(𝑁 − 1)))) = (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1)))))
327 fzdisj 12937 . . . . . . . . . . . . . . . . . . . 20 (𝑦 < (𝑦 + 1) → ((1...𝑦) ∩ ((𝑦 + 1)...(𝑁 − 1))) = ∅)
32852, 327syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → ((1...𝑦) ∩ ((𝑦 + 1)...(𝑁 − 1))) = ∅)
329328imaeq2d 5931 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ ((1...𝑦) ∩ ((𝑦 + 1)...(𝑁 − 1)))) = ((2nd ‘(1st𝑇)) “ ∅))
330329, 56syl6eq 2874 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd ‘(1st𝑇)) “ ((1...𝑦) ∩ ((𝑦 + 1)...(𝑁 − 1)))) = ∅)
331326, 330sylan9req 2879 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1)))) = ∅)
332 fnun 6465 . . . . . . . . . . . . . . . 16 ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑦)) ∧ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1)))) ∧ (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1)))) = ∅) → ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1)))))
333324, 331, 332sylancr 589 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1)))))
334 imaundi 6010 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑇)) “ ((1...𝑦) ∪ ((𝑦 + 1)...(𝑁 − 1)))) = (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))))
335203, 208eqtrd 2858 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁}))
336335difeq1d 4100 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((1...𝑁) ∖ {𝑁}) = (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}))
337 difun2 4431 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...(𝑁 − 1)) ∖ {𝑁})
338336, 337syl6eq 2874 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...𝑁) ∖ {𝑁}) = ((1...(𝑁 − 1)) ∖ {𝑁}))
339 difsn 4733 . . . . . . . . . . . . . . . . . . . . . . 23 𝑁 ∈ (1...(𝑁 − 1)) → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
340163, 339syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
341338, 340eqtrd 2858 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
342341adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
34372adantl 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ (ℤ𝑦))
344 fzsplit2 12935 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦 + 1) ∈ (ℤ‘1) ∧ (𝑁 − 1) ∈ (ℤ𝑦)) → (1...(𝑁 − 1)) = ((1...𝑦) ∪ ((𝑦 + 1)...(𝑁 − 1))))
34566, 343, 344syl2anc 586 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...(𝑁 − 1)) = ((1...𝑦) ∪ ((𝑦 + 1)...(𝑁 − 1))))
346342, 345eqtrd 2858 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1...𝑁) ∖ {𝑁}) = ((1...𝑦) ∪ ((𝑦 + 1)...(𝑁 − 1))))
347346imaeq2d 5931 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {𝑁})) = ((2nd ‘(1st𝑇)) “ ((1...𝑦) ∪ ((𝑦 + 1)...(𝑁 − 1)))))
348 imadif 6440 . . . . . . . . . . . . . . . . . . . . 21 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {𝑁})) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {𝑁})))
34947, 348syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {𝑁})) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {𝑁})))
350 elfz1end 12940 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
35167, 350sylib 220 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑁 ∈ (1...𝑁))
352 fnsnfv 6745 . . . . . . . . . . . . . . . . . . . . . . 23 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → {((2nd ‘(1st𝑇))‘𝑁)} = ((2nd ‘(1st𝑇)) “ {𝑁}))
353256, 351, 352syl2anc 586 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {((2nd ‘(1st𝑇))‘𝑁)} = ((2nd ‘(1st𝑇)) “ {𝑁}))
354353eqcomd 2829 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((2nd ‘(1st𝑇)) “ {𝑁}) = {((2nd ‘(1st𝑇))‘𝑁)})
35582, 354difeq12d 4102 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {𝑁})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}))
356349, 355eqtrd 2858 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {𝑁})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}))
357356adantr 483 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {𝑁})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}))
358347, 357eqtr3d 2860 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((1...𝑦) ∪ ((𝑦 + 1)...(𝑁 − 1)))) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}))
359334, 358syl5eqr 2872 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1)))) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}))
360359fneq2d 6449 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1)))) ↔ ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)})))
361333, 360mpbid 234 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}))
362 incom 4180 . . . . . . . . . . . . . . . 16 (((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}) ∩ {((2nd ‘(1st𝑇))‘𝑁)}) = ({((2nd ‘(1st𝑇))‘𝑁)} ∩ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}))
363 disjdif 4423 . . . . . . . . . . . . . . . 16 ({((2nd ‘(1st𝑇))‘𝑁)} ∩ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)})) = ∅
364362, 363eqtri 2846 . . . . . . . . . . . . . . 15 (((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}) ∩ {((2nd ‘(1st𝑇))‘𝑁)}) = ∅
365 fnconstg 6569 . . . . . . . . . . . . . . . . . 18 (1 ∈ V → ({((2nd ‘(1st𝑇))‘𝑁)} × {1}) Fn {((2nd ‘(1st𝑇))‘𝑁)})
36632, 365ax-mp 5 . . . . . . . . . . . . . . . . 17 ({((2nd ‘(1st𝑇))‘𝑁)} × {1}) Fn {((2nd ‘(1st𝑇))‘𝑁)}
367 fvun1 6756 . . . . . . . . . . . . . . . . 17 ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}) ∧ ({((2nd ‘(1st𝑇))‘𝑁)} × {1}) Fn {((2nd ‘(1st𝑇))‘𝑁)} ∧ ((((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}) ∩ {((2nd ‘(1st𝑇))‘𝑁)}) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}))) → ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {1}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0}))‘𝑛))
368366, 367mp3an2 1445 . . . . . . . . . . . . . . . 16 ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}) ∧ ((((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}) ∩ {((2nd ‘(1st𝑇))‘𝑁)}) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}))) → ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {1}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0}))‘𝑛))
369 fnconstg 6569 . . . . . . . . . . . . . . . . . 18 (0 ∈ V → ({((2nd ‘(1st𝑇))‘𝑁)} × {0}) Fn {((2nd ‘(1st𝑇))‘𝑁)})
37035, 369ax-mp 5 . . . . . . . . . . . . . . . . 17 ({((2nd ‘(1st𝑇))‘𝑁)} × {0}) Fn {((2nd ‘(1st𝑇))‘𝑁)}
371 fvun1 6756 . . . . . . . . . . . . . . . . 17 ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}) ∧ ({((2nd ‘(1st𝑇))‘𝑁)} × {0}) Fn {((2nd ‘(1st𝑇))‘𝑁)} ∧ ((((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}) ∩ {((2nd ‘(1st𝑇))‘𝑁)}) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}))) → ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {0}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0}))‘𝑛))
372370, 371mp3an2 1445 . . . . . . . . . . . . . . . 16 ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}) ∧ ((((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}) ∩ {((2nd ‘(1st𝑇))‘𝑁)}) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}))) → ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {0}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0}))‘𝑛))
373368, 372eqtr4d 2861 . . . . . . . . . . . . . . 15 ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}) ∧ ((((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}) ∩ {((2nd ‘(1st𝑇))‘𝑁)}) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}))) → ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {1}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {0}))‘𝑛))
374364, 373mpanr1 701 . . . . . . . . . . . . . 14 ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)}) ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)})) → ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {1}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {0}))‘𝑛))
375361, 374sylan 582 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑁)})) → ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {1}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {0}))‘𝑛))
376321, 375sylan2br 596 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘𝑁))) → ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {1}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {0}))‘𝑛))
377376anassrs 470 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘𝑁)) → ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {1}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {0}))‘𝑛))
378 imaundi 6010 . . . . . . . . . . . . . . . . . . 19 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((1 + 1)...(𝑦 + 1)) ∪ {1})) = ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((1 + 1)...(𝑦 + 1))) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ {1}))
379 imaco 6106 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((1 + 1)...(𝑦 + 1))) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ ((1 + 1)...(𝑦 + 1))))
380 imaco 6106 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ {1}) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ {1}))
381379, 380uneq12i 4139 . . . . . . . . . . . . . . . . . . 19 ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ ((1 + 1)...(𝑦 + 1))) ∪ (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ {1})) = (((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ ((1 + 1)...(𝑦 + 1)))) ∪ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ {1})))
382378, 381eqtri 2846 . . . . . . . . . . . . . . . . . 18 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((1 + 1)...(𝑦 + 1)) ∪ {1})) = (((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ ((1 + 1)...(𝑦 + 1)))) ∪ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ {1})))
383 fzpred 12958 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 + 1) ∈ (ℤ‘1) → (1...(𝑦 + 1)) = ({1} ∪ ((1 + 1)...(𝑦 + 1))))
38465, 383syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0...(𝑁 − 1)) → (1...(𝑦 + 1)) = ({1} ∪ ((1 + 1)...(𝑦 + 1))))
385 uncom 4131 . . . . . . . . . . . . . . . . . . . . 21 ({1} ∪ ((1 + 1)...(𝑦 + 1))) = (((1 + 1)...(𝑦 + 1)) ∪ {1})
386384, 385syl6eq 2874 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (0...(𝑁 − 1)) → (1...(𝑦 + 1)) = (((1 + 1)...(𝑦 + 1)) ∪ {1}))
387386imaeq2d 5931 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) = (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((1 + 1)...(𝑦 + 1)) ∪ {1})))
388387adantl 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) = (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((1 + 1)...(𝑦 + 1)) ∪ {1})))
389 elfzelz 12911 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
390123a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℤ → ((1 + 1) − 1) = 1)
391 zcn 11989 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ℤ → 𝑦 ∈ ℂ)
392 pncan1 11066 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ℂ → ((𝑦 + 1) − 1) = 𝑦)
393391, 392syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℤ → ((𝑦 + 1) − 1) = 𝑦)
394390, 393oveq12d 7176 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ℤ → (((1 + 1) − 1)...((𝑦 + 1) − 1)) = (1...𝑦))
395 elfzelz 12911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1)) → 𝑗 ∈ ℤ)
396395zcnd 12091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1)) → 𝑗 ∈ ℂ)
397 pncan1 11066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ ℂ → ((𝑗 + 1) − 1) = 𝑗)
398396, 397syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1)) → ((𝑗 + 1) − 1) = 𝑗)
399398eleq1d 2899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1)) → (((𝑗 + 1) − 1) ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1)) ↔ 𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1))))
400399ibir 270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1)) → ((𝑗 + 1) − 1) ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1)))
401400adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1))) → ((𝑗 + 1) − 1) ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1)))
402 peano2z 12026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 ∈ ℤ → (𝑦 + 1) ∈ ℤ)
403402, 116jctil 522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ ℤ → ((1 + 1) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ))
404395peano2zd 12093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1)) → (𝑗 + 1) ∈ ℤ)
405404, 114jctir 523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1)) → ((𝑗 + 1) ∈ ℤ ∧ 1 ∈ ℤ))
406 fzsubel 12946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((1 + 1) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ) ∧ ((𝑗 + 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝑗 + 1) ∈ ((1 + 1)...(𝑦 + 1)) ↔ ((𝑗 + 1) − 1) ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1))))
407403, 405, 406syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1))) → ((𝑗 + 1) ∈ ((1 + 1)...(𝑦 + 1)) ↔ ((𝑗 + 1) − 1) ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1))))
408401, 407mpbird 259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1))) → (𝑗 + 1) ∈ ((1 + 1)...(𝑦 + 1)))
409398eqcomd 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1)) → 𝑗 = ((𝑗 + 1) − 1))
410409adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1))) → 𝑗 = ((𝑗 + 1) − 1))
411 oveq1 7165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = (𝑗 + 1) → (𝑛 − 1) = ((𝑗 + 1) − 1))
412411rspceeqv 3640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑗 + 1) ∈ ((1 + 1)...(𝑦 + 1)) ∧ 𝑗 = ((𝑗 + 1) − 1)) → ∃𝑛 ∈ ((1 + 1)...(𝑦 + 1))𝑗 = (𝑛 − 1))
413408, 410, 412syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ ℤ ∧ 𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1))) → ∃𝑛 ∈ ((1 + 1)...(𝑦 + 1))𝑗 = (𝑛 − 1))
414413ex 415 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℤ → (𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1)) → ∃𝑛 ∈ ((1 + 1)...(𝑦 + 1))𝑗 = (𝑛 − 1)))
415 simpr 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ ((1 + 1)...(𝑦 + 1))) → 𝑛 ∈ ((1 + 1)...(𝑦 + 1)))
416 elfzelz 12911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) → 𝑛 ∈ ℤ)
417416, 114jctir 523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) → (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
418 fzsubel 12946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((1 + 1) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↔ (𝑛 − 1) ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1))))
419403, 417, 418syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ ((1 + 1)...(𝑦 + 1))) → (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↔ (𝑛 − 1) ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1))))
420415, 419mpbid 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ ((1 + 1)...(𝑦 + 1))) → (𝑛 − 1) ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1)))
421 eleq1 2902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 = (𝑛 − 1) → (𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1)) ↔ (𝑛 − 1) ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1))))
422420, 421syl5ibrcom 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ ℤ ∧ 𝑛 ∈ ((1 + 1)...(𝑦 + 1))) → (𝑗 = (𝑛 − 1) → 𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1))))
423422rexlimdva 3286 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℤ → (∃𝑛 ∈ ((1 + 1)...(𝑦 + 1))𝑗 = (𝑛 − 1) → 𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1))))
424414, 423impbid 214 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ℤ → (𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1)) ↔ ∃𝑛 ∈ ((1 + 1)...(𝑦 + 1))𝑗 = (𝑛 − 1)))
425 vex 3499 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑗 ∈ V
426 eqid 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↦ (𝑛 − 1)) = (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↦ (𝑛 − 1))
427426elrnmpt 5830 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ V → (𝑗 ∈ ran (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↦ (𝑛 − 1)) ↔ ∃𝑛 ∈ ((1 + 1)...(𝑦 + 1))𝑗 = (𝑛 − 1)))
428425, 427ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ ran (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↦ (𝑛 − 1)) ↔ ∃𝑛 ∈ ((1 + 1)...(𝑦 + 1))𝑗 = (𝑛 − 1))
429424, 428syl6bbr 291 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℤ → (𝑗 ∈ (((1 + 1) − 1)...((𝑦 + 1) − 1)) ↔ 𝑗 ∈ ran (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↦ (𝑛 − 1))))
430429eqrdv 2821 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ℤ → (((1 + 1) − 1)...((𝑦 + 1) − 1)) = ran (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↦ (𝑛 − 1)))
431394, 430eqtr3d 2860 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℤ → (1...𝑦) = ran (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↦ (𝑛 − 1)))
432389, 431syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (0...(𝑁 − 1)) → (1...𝑦) = ran (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↦ (𝑛 − 1)))
433432adantl 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑦) = ran (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↦ (𝑛 − 1)))
434 df-ima 5570 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ ((1 + 1)...(𝑦 + 1))) = ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ↾ ((1 + 1)...(𝑦 + 1)))
435 uzid 12261 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1 ∈ ℤ → 1 ∈ (ℤ‘1))
436 peano2uz 12304 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1 ∈ (ℤ‘1) → (1 + 1) ∈ (ℤ‘1))
437114, 435, 436mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (1 + 1) ∈ (ℤ‘1)
438 fzss1 12949 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 + 1) ∈ (ℤ‘1) → ((1 + 1)...(𝑦 + 1)) ⊆ (1...(𝑦 + 1)))
439437, 438ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 + 1)...(𝑦 + 1)) ⊆ (1...(𝑦 + 1))
440439, 273sstrid 3980 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1 + 1)...(𝑦 + 1)) ⊆ (1...𝑁))
441440resmptd 5910 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ↾ ((1 + 1)...(𝑦 + 1))) = (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))
442 elfzle1 12913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (1 ∈ ((1 + 1)...(𝑦 + 1)) → (1 + 1) ≤ 1)
443170, 442mto 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ¬ 1 ∈ ((1 + 1)...(𝑦 + 1))
444 eleq1 2902 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 1 → (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↔ 1 ∈ ((1 + 1)...(𝑦 + 1))))
445443, 444mtbiri 329 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 1 → ¬ 𝑛 ∈ ((1 + 1)...(𝑦 + 1)))
446445necon2ai 3047 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) → 𝑛 ≠ 1)
447446, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) → if(𝑛 = 1, 𝑁, (𝑛 − 1)) = (𝑛 − 1))
448447mpteq2ia 5159 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) = (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↦ (𝑛 − 1))
449441, 448syl6eq 2874 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ↾ ((1 + 1)...(𝑦 + 1))) = (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↦ (𝑛 − 1)))
450449rneqd 5810 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ↾ ((1 + 1)...(𝑦 + 1))) = ran (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↦ (𝑛 − 1)))
451434, 450syl5eq 2870 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ ((1 + 1)...(𝑦 + 1))) = ran (𝑛 ∈ ((1 + 1)...(𝑦 + 1)) ↦ (𝑛 − 1)))
452433, 451eqtr4d 2861 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑦) = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ ((1 + 1)...(𝑦 + 1))))
453452imaeq2d 5931 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ (1...𝑦)) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ ((1 + 1)...(𝑦 + 1)))))
454267sneqd 4581 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))‘1)} = {𝑁})
455 fnsnfv 6745 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) Fn (1...𝑁) ∧ 1 ∈ (1...𝑁)) → {((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))‘1)} = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ {1}))
456270, 266, 455syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))‘1)} = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ {1}))
457454, 456eqtr3d 2860 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → {𝑁} = ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ {1}))
458457imaeq2d 5931 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((2nd ‘(1st𝑇)) “ {𝑁}) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ {1})))
459353, 458eqtrd 2858 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {((2nd ‘(1st𝑇))‘𝑁)} = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ {1})))
460459adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → {((2nd ‘(1st𝑇))‘𝑁)} = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ {1})))
461453, 460uneq12d 4142 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∪ {((2nd ‘(1st𝑇))‘𝑁)}) = (((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ ((1 + 1)...(𝑦 + 1)))) ∪ ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ {1}))))
462382, 388, 4613eqtr4a 2884 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) = (((2nd ‘(1st𝑇)) “ (1...𝑦)) ∪ {((2nd ‘(1st𝑇))‘𝑁)}))
463462xpeq1d 5586 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) = ((((2nd ‘(1st𝑇)) “ (1...𝑦)) ∪ {((2nd ‘(1st𝑇))‘𝑁)}) × {1}))
464 xpundir 5623 . . . . . . . . . . . . . . . 16 ((((2nd ‘(1st𝑇)) “ (1...𝑦)) ∪ {((2nd ‘(1st𝑇))‘𝑁)}) × {1}) = ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {1}))
465463, 464syl6eq 2874 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) = ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {1})))
466 imaco 6106 . . . . . . . . . . . . . . . . 17 (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ (((𝑦 + 1) + 1)...𝑁)))
467 df-ima 5570 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ (((𝑦 + 1) + 1)...𝑁)) = ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ↾ (((𝑦 + 1) + 1)...𝑁))
468 fzss1 12949 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 + 1) + 1) ∈ (ℤ‘1) → (((𝑦 + 1) + 1)...𝑁) ⊆ (1...𝑁))
469231, 468syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1) + 1)...𝑁) ⊆ (1...𝑁))
470469resmptd 5910 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ↾ (((𝑦 + 1) + 1)...𝑁)) = (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))
471 1red 10644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ (0...(𝑁 − 1)) → 1 ∈ ℝ)
47263nnzd 12089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℤ)
473472peano2zd 12093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℤ)
474473zred 12090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℝ)
47563nnge1d 11688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ (0...(𝑁 − 1)) → 1 ≤ (𝑦 + 1))
476471, 218, 474, 475, 219lelttrd 10800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ (0...(𝑁 − 1)) → 1 < ((𝑦 + 1) + 1))
477471, 474ltnled 10789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ (0...(𝑁 − 1)) → (1 < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ 1))
478476, 477mpbid 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ (0...(𝑁 − 1)) → ¬ ((𝑦 + 1) + 1) ≤ 1)
479 elfzle1 12913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (1 ∈ (((𝑦 + 1) + 1)...𝑁) → ((𝑦 + 1) + 1) ≤ 1)
480478, 479nsyl 142 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ (0...(𝑁 − 1)) → ¬ 1 ∈ (((𝑦 + 1) + 1)...𝑁))
481 eleq1 2902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 1 → (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↔ 1 ∈ (((𝑦 + 1) + 1)...𝑁)))
482481notbid 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 1 → (¬ 𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↔ ¬ 1 ∈ (((𝑦 + 1) + 1)...𝑁)))
483480, 482syl5ibrcom 249 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑛 = 1 → ¬ 𝑛 ∈ (((𝑦 + 1) + 1)...𝑁)))
484483necon2ad 3033 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) → 𝑛 ≠ 1))
485484imp 409 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ (0...(𝑁 − 1)) ∧ 𝑛 ∈ (((𝑦 + 1) + 1)...𝑁)) → 𝑛 ≠ 1)
486485, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ (0...(𝑁 − 1)) ∧ 𝑛 ∈ (((𝑦 + 1) + 1)...𝑁)) → if(𝑛 = 1, 𝑁, (𝑛 − 1)) = (𝑛 − 1))
487486mpteq2dva 5163 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) = (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↦ (𝑛 − 1)))
488487adantl 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) = (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↦ (𝑛 − 1)))
489470, 488eqtrd 2858 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ↾ (((𝑦 + 1) + 1)...𝑁)) = (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↦ (𝑛 − 1)))
490489rneqd 5810 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ran ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) ↾ (((𝑦 + 1) + 1)...𝑁)) = ran (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↦ (𝑛 − 1)))
491467, 490syl5eq 2870 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ (((𝑦 + 1) + 1)...𝑁)) = ran (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↦ (𝑛 − 1)))
492 eqid 2823 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↦ (𝑛 − 1)) = (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↦ (𝑛 − 1))
493492elrnmpt 5830 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ V → (𝑗 ∈ ran (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↦ (𝑛 − 1)) ↔ ∃𝑛 ∈ (((𝑦 + 1) + 1)...𝑁)𝑗 = (𝑛 − 1)))
494425, 493ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ran (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↦ (𝑛 − 1)) ↔ ∃𝑛 ∈ (((𝑦 + 1) + 1)...𝑁)𝑗 = (𝑛 − 1))
495 simpr 487 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (((𝑦 + 1) + 1)...𝑁)) → 𝑛 ∈ (((𝑦 + 1) + 1)...𝑁))
496113, 473anim12ci 615 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ))
497 elfzelz 12911 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) → 𝑛 ∈ ℤ)
498497, 114jctir 523 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) → (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
499 fzsubel 12946 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑦 + 1) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↔ (𝑛 − 1) ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1))))
500496, 498, 499syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (((𝑦 + 1) + 1)...𝑁)) → (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↔ (𝑛 − 1) ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1))))
501495, 500mpbid 234 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (((𝑦 + 1) + 1)...𝑁)) → (𝑛 − 1) ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)))
502 eleq1 2902 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝑛 − 1) → (𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)) ↔ (𝑛 − 1) ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1))))
503501, 502syl5ibrcom 249 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (((𝑦 + 1) + 1)...𝑁)) → (𝑗 = (𝑛 − 1) → 𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1))))
504503rexlimdva 3286 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (∃𝑛 ∈ (((𝑦 + 1) + 1)...𝑁)𝑗 = (𝑛 − 1) → 𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1))))
505 elfzelz 12911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)) → 𝑗 ∈ ℤ)
506505zcnd 12091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)) → 𝑗 ∈ ℂ)
507506, 397syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)) → ((𝑗 + 1) − 1) = 𝑗)
508507eleq1d 2899 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)) → (((𝑗 + 1) − 1) ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)) ↔ 𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1))))
509508ibir 270 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)) → ((𝑗 + 1) − 1) ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)))
510509adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1))) → ((𝑗 + 1) − 1) ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)))
511505peano2zd 12093 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)) → (𝑗 + 1) ∈ ℤ)
512511, 114jctir 523 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)) → ((𝑗 + 1) ∈ ℤ ∧ 1 ∈ ℤ))
513 fzsubel 12946 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑦 + 1) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑗 + 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝑗 + 1) ∈ (((𝑦 + 1) + 1)...𝑁) ↔ ((𝑗 + 1) − 1) ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1))))
514496, 512, 513syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1))) → ((𝑗 + 1) ∈ (((𝑦 + 1) + 1)...𝑁) ↔ ((𝑗 + 1) − 1) ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1))))
515510, 514mpbird 259 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ (((𝑦 + 1) + 1)...𝑁))
516507eqcomd 2829 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)) → 𝑗 = ((𝑗 + 1) − 1))
517516adantl 484 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1))) → 𝑗 = ((𝑗 + 1) − 1))
518411rspceeqv 3640 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑗 + 1) ∈ (((𝑦 + 1) + 1)...𝑁) ∧ 𝑗 = ((𝑗 + 1) − 1)) → ∃𝑛 ∈ (((𝑦 + 1) + 1)...𝑁)𝑗 = (𝑛 − 1))
519515, 517, 518syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1))) → ∃𝑛 ∈ (((𝑦 + 1) + 1)...𝑁)𝑗 = (𝑛 − 1))
520519ex 415 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)) → ∃𝑛 ∈ (((𝑦 + 1) + 1)...𝑁)𝑗 = (𝑛 − 1)))
521504, 520impbid 214 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (∃𝑛 ∈ (((𝑦 + 1) + 1)...𝑁)𝑗 = (𝑛 − 1) ↔ 𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1))))
522494, 521syl5bb 285 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑗 ∈ ran (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↦ (𝑛 − 1)) ↔ 𝑗 ∈ ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1))))
523522eqrdv 2821 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ran (𝑛 ∈ (((𝑦 + 1) + 1)...𝑁) ↦ (𝑛 − 1)) = ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)))
52463nncnd 11656 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℂ)
525 pncan1 11066 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 + 1) ∈ ℂ → (((𝑦 + 1) + 1) − 1) = (𝑦 + 1))
526524, 525syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0...(𝑁 − 1)) → (((𝑦 + 1) + 1) − 1) = (𝑦 + 1))
527526oveq1d 7173 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (0...(𝑁 − 1)) → ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)) = ((𝑦 + 1)...(𝑁 − 1)))
528527adantl 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((𝑦 + 1) + 1) − 1)...(𝑁 − 1)) = ((𝑦 + 1)...(𝑁 − 1)))
529491, 523, 5283eqtrd 2862 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ (((𝑦 + 1) + 1)...𝑁)) = ((𝑦 + 1)...(𝑁 − 1)))
530529imaeq2d 5931 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))) “ (((𝑦 + 1) + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))))
531466, 530syl5eq 2870 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))))
532531xpeq1d 5586 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0}))
533465, 532uneq12d 4142 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {1})) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})))
534 un23 4146 . . . . . . . . . . . . . 14 (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {1})) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {1}))
535533, 534syl6eq 2874 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {1})))
536535fveq1d 6674 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {1}))‘𝑛))
537536ad2antrr 724 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {1}))‘𝑛))
538 imaundi 6010 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)) “ (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁})) = (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) ∪ ((2nd ‘(1st𝑇)) “ {𝑁}))
539 fzsplit2 12935 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)) ∧ 𝑁 ∈ (ℤ‘(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
540233, 201, 539syl2anr 598 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)))
541207uneq2d 4141 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}))
542541adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((𝑦 + 1)...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}))
543540, 542eqtrd 2858 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1)...𝑁) = (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁}))
544543imaeq2d 5931 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ (((𝑦 + 1)...(𝑁 − 1)) ∪ {𝑁})))
545353adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → {((2nd ‘(1st𝑇))‘𝑁)} = ((2nd ‘(1st𝑇)) “ {𝑁}))
546545uneq2d 4141 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) ∪ {((2nd ‘(1st𝑇))‘𝑁)}) = (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) ∪ ((2nd ‘(1st𝑇)) “ {𝑁})))
547538, 544, 5463eqtr4a 2884 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) = (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) ∪ {((2nd ‘(1st𝑇))‘𝑁)}))
548547xpeq1d 5586 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) = ((((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) ∪ {((2nd ‘(1st𝑇))‘𝑁)}) × {0}))
549 xpundir 5623 . . . . . . . . . . . . . . . 16 ((((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) ∪ {((2nd ‘(1st𝑇))‘𝑁)}) × {0}) = ((((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0}) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {0}))
550548, 549syl6eq 2874 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}) = ((((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0}) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {0})))
551550uneq2d 4141 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0}) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {0}))))
552 unass 4144 . . . . . . . . . . . . . 14 (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0}) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {0})))
553551, 552syl6eqr 2876 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {0})))
554553fveq1d 6674 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {0}))‘𝑛))
555554ad2antrr 724 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛) = ((((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...(𝑁 − 1))) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑁)} × {0}))‘𝑛))
556377, 537, 5553eqtr4d 2868 . . . . . . . . . 10 ((((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))
557317, 556eqtrd 2858 . . . . . . . . 9 ((((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2nd ‘(1st𝑇))‘𝑁)) → (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − 0) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))
558251, 253, 315, 557ifbothda 4506 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0)) = (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))
559558oveq2d 7174 . . . . . . 7 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (((1st ‘(1st𝑇))‘𝑛) + (((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0))) = (((1st ‘(1st𝑇))‘𝑛) + (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)))
560249, 559eqtr2d 2859 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (((1st ‘(1st𝑇))‘𝑛) + (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛)) = ((((1st ‘(1st𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0)) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛)))
561560mpteq2dva 5163 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) + (((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))‘𝑛))) = (𝑛 ∈ (1...𝑁) ↦ ((((1st ‘(1st𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0)) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛))))
56292, 561eqtrd 2858 . . . 4 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))) = (𝑛 ∈ (1...𝑁) ↦ ((((1st ‘(1st𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0)) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛))))
56351adantl 484 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ)
564159adantr 483 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
565157adantr 483 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℝ)
566 elfzle2 12914 . . . . . . . . . 10 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑁 − 1))
567566adantl 484 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ≤ (𝑁 − 1))
568158adantr 483 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
569563, 564, 565, 567, 568lelttrd 10800 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁)
570 poimirlem21.4 . . . . . . . . 9 (𝜑 → (2nd𝑇) = 𝑁)
571570adantr 483 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (2nd𝑇) = 𝑁)
572569, 571breqtrrd 5096 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < (2nd𝑇))
573572iftrued 4477 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = 𝑦)
574573csbeq1d 3889 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑦 / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
575 vex 3499 . . . . . 6 𝑦 ∈ V
576 oveq2 7166 . . . . . . . . . 10 (𝑗 = 𝑦 → (1...𝑗) = (1...𝑦))
577576imaeq2d 5931 . . . . . . . . 9 (𝑗 = 𝑦 → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑦)))
578577xpeq1d 5586 . . . . . . . 8 (𝑗 = 𝑦 → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}))
579 oveq1 7165 . . . . . . . . . . 11 (𝑗 = 𝑦 → (𝑗 + 1) = (𝑦 + 1))
580579oveq1d 7173 . . . . . . . . . 10 (𝑗 = 𝑦 → ((𝑗 + 1)...𝑁) = ((𝑦 + 1)...𝑁))
581580imaeq2d 5931 . . . . . . . . 9 (𝑗 = 𝑦 → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)))
582581xpeq1d 5586 . . . . . . . 8 (𝑗 = 𝑦 → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))
583578, 582uneq12d 4142 . . . . . . 7 (𝑗 = 𝑦 → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))
584583oveq2d 7174 . . . . . 6 (𝑗 = 𝑦 → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
585575, 584csbie 3920 . . . . 5 𝑦 / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))
586574, 585syl6eq 2874 . . . 4 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
587 ovexd 7193 . . . . 5 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → (((1st ‘(1st𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0)) ∈ V)
588 fvexd 6687 . . . . 5 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑛 ∈ (1...𝑁)) → ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛) ∈ V)
589 eqidd 2824 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0))) = (𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0))))
590246ffnd 6517 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
591 nfcv 2979 . . . . . . . . . . 11 𝑛(2nd ‘(1st𝑇))
592 nfmpt1 5166 . . . . . . . . . . 11 𝑛(𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))
593591, 592nfco 5738 . . . . . . . . . 10 𝑛((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1))))
594 nfcv 2979 . . . . . . . . . 10 𝑛(1...(𝑦 + 1))
595593, 594nfima 5939 . . . . . . . . 9 𝑛(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1)))
596 nfcv 2979 . . . . . . . . 9 𝑛{1}
597595, 596nfxp 5590 . . . . . . . 8 𝑛((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1})
598 nfcv 2979 . . . . . . . . . 10 𝑛(((𝑦 + 1) + 1)...𝑁)
599593, 598nfima 5939 . . . . . . . . 9 𝑛(((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁))
600 nfcv 2979 . . . . . . . . 9 𝑛{0}
601599, 600nfxp 5590 . . . . . . . 8 𝑛((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})
602597, 601nfun 4143 . . . . . . 7 𝑛(((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
603602dffn5f 6738 . . . . . 6 ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁) ↔ (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) = (𝑛 ∈ (1...𝑁) ↦ ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛)))
604590, 603sylib 220 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) = (𝑛 ∈ (1...𝑁) ↦ ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛)))
60588, 587, 588, 589, 604offval2 7428 . . . 4 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0))) ∘f + (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) = (𝑛 ∈ (1...𝑁) ↦ ((((1st ‘(1st𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0)) + ((((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘𝑛))))
606562, 586, 6053eqtr4rd 2869 . . 3 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0))) ∘f + (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
607606mpteq2dva 5163 . 2 (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0))) ∘f + (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
60821, 607eqtr4d 2861 1 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st ‘(1st𝑇))‘𝑛) − if(𝑛 = ((2nd ‘(1st𝑇))‘𝑁), 1, 0))) ∘f + (((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 1, 𝑁, (𝑛 − 1)))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398   = wceq 1537  wcel 2114  {cab 2801  wne 3018  wral 3140  wrex 3141  ∃!wreu 3142  {crab 3144  Vcvv 3496  csb 3885  cdif 3935  cun 3936  cin 3937  wss 3938  c0 4293  ifcif 4469  {csn 4569  cop 4575   class class class wbr 5068  cmpt 5148   × cxp 5555  ccnv 5556  ran crn 5558  cres 5559  cima 5560  ccom 5561  Fun wfun 6351   Fn wfn 6352  wf 6353  ontowfo 6355  1-1-ontowf1o 6356  cfv 6357  (class class class)co 7158  f cof 7409  1st c1st 7689  2nd c2nd 7690  m cmap 8408  cc 10537  cr 10538  0cc0 10539  1c1 10540   + caddc 10542   < clt 10677  cle 10678  cmin 10872  cn 11640  0cn0 11900  cz 11984  cuz 12246  ...cfz 12895  ..^cfzo 13036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-of 7411  df-om 7583  df-1st 7691  df-2nd 7692  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-er 8291  df-map 8410  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-nn 11641  df-n0 11901  df-z 11985  df-uz 12247  df-fz 12896  df-fzo 13037
This theorem is referenced by:  poimirlem20  34914
  Copyright terms: Public domain W3C validator