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

Theorem poimirlem15 33757
Description: Lemma for poimir 33775, that the face in poimirlem22 33764 is a face. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimirlem22.s 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
poimirlem22.1 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
poimirlem22.2 (𝜑𝑇𝑆)
poimirlem15.3 (𝜑 → (2nd𝑇) ∈ (1...(𝑁 − 1)))
Assertion
Ref Expression
poimirlem15 (𝜑 → ⟨⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩, (2nd𝑇)⟩ ∈ 𝑆)
Distinct variable groups:   𝑓,𝑗,𝑡,𝑦   𝜑,𝑗,𝑦   𝑗,𝐹,𝑦   𝑗,𝑁,𝑦   𝑇,𝑗,𝑦   𝜑,𝑡   𝑓,𝐾,𝑗,𝑡   𝑓,𝑁,𝑡   𝑇,𝑓   𝑓,𝐹,𝑡   𝑡,𝑇   𝑆,𝑗,𝑡,𝑦
Allowed substitution hints:   𝜑(𝑓)   𝑆(𝑓)   𝐾(𝑦)

Proof of Theorem poimirlem15
StepHypRef Expression
1 poimirlem22.2 . . . . . 6 (𝜑𝑇𝑆)
2 elrabi 3510 . . . . . . 7 (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
3 poimirlem22.s . . . . . . 7 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
42, 3eleq2s 2868 . . . . . 6 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
51, 4syl 17 . . . . 5 (𝜑𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
6 xp1st 7347 . . . . 5 (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
7 xp1st 7347 . . . . 5 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
85, 6, 73syl 18 . . . 4 (𝜑 → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
9 xp2nd 7348 . . . . . . . 8 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
105, 6, 93syl 18 . . . . . . 7 (𝜑 → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
11 fvex 6342 . . . . . . . 8 (2nd ‘(1st𝑇)) ∈ V
12 f1oeq1 6268 . . . . . . . 8 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
1311, 12elab 3501 . . . . . . 7 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
1410, 13sylib 208 . . . . . 6 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
15 poimirlem15.3 . . . . . . . . . . . . 13 (𝜑 → (2nd𝑇) ∈ (1...(𝑁 − 1)))
16 elfznn 12577 . . . . . . . . . . . . 13 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ∈ ℕ)
1715, 16syl 17 . . . . . . . . . . . 12 (𝜑 → (2nd𝑇) ∈ ℕ)
1817nnred 11237 . . . . . . . . . . 11 (𝜑 → (2nd𝑇) ∈ ℝ)
1918ltp1d 11156 . . . . . . . . . . 11 (𝜑 → (2nd𝑇) < ((2nd𝑇) + 1))
2018, 19ltned 10375 . . . . . . . . . 10 (𝜑 → (2nd𝑇) ≠ ((2nd𝑇) + 1))
2120necomd 2998 . . . . . . . . . 10 (𝜑 → ((2nd𝑇) + 1) ≠ (2nd𝑇))
22 fvex 6342 . . . . . . . . . . 11 (2nd𝑇) ∈ V
23 ovex 6823 . . . . . . . . . . 11 ((2nd𝑇) + 1) ∈ V
24 f1oprg 6322 . . . . . . . . . . 11 ((((2nd𝑇) ∈ V ∧ ((2nd𝑇) + 1) ∈ V) ∧ (((2nd𝑇) + 1) ∈ V ∧ (2nd𝑇) ∈ V)) → (((2nd𝑇) ≠ ((2nd𝑇) + 1) ∧ ((2nd𝑇) + 1) ≠ (2nd𝑇)) → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd𝑇) + 1), (2nd𝑇)}))
2522, 23, 23, 22, 24mp4an 665 . . . . . . . . . 10 (((2nd𝑇) ≠ ((2nd𝑇) + 1) ∧ ((2nd𝑇) + 1) ≠ (2nd𝑇)) → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd𝑇) + 1), (2nd𝑇)})
2620, 21, 25syl2anc 565 . . . . . . . . 9 (𝜑 → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd𝑇) + 1), (2nd𝑇)})
27 prcom 4403 . . . . . . . . . 10 {((2nd𝑇) + 1), (2nd𝑇)} = {(2nd𝑇), ((2nd𝑇) + 1)}
28 f1oeq3 6270 . . . . . . . . . 10 ({((2nd𝑇) + 1), (2nd𝑇)} = {(2nd𝑇), ((2nd𝑇) + 1)} → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd𝑇) + 1), (2nd𝑇)} ↔ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)}))
2927, 28ax-mp 5 . . . . . . . . 9 ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd𝑇) + 1), (2nd𝑇)} ↔ {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)})
3026, 29sylib 208 . . . . . . . 8 (𝜑 → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)})
31 f1oi 6315 . . . . . . . 8 ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})):((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})–1-1-onto→((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})
32 disjdif 4182 . . . . . . . . 9 ({(2nd𝑇), ((2nd𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ∅
33 f1oun 6297 . . . . . . . . 9 ((({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)} ∧ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})):((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})–1-1-onto→((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) ∧ (({(2nd𝑇), ((2nd𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ∅ ∧ ({(2nd𝑇), ((2nd𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ∅)) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))):({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))–1-1-onto→({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
3432, 32, 33mpanr12 677 . . . . . . . 8 (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{(2nd𝑇), ((2nd𝑇) + 1)} ∧ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})):((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})–1-1-onto→((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))):({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))–1-1-onto→({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
3530, 31, 34sylancl 566 . . . . . . 7 (𝜑 → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))):({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))–1-1-onto→({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
36 poimir.0 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℕ)
3736nncnd 11238 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℂ)
38 npcan1 10657 . . . . . . . . . . . . . 14 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
3937, 38syl 17 . . . . . . . . . . . . 13 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
4036nnzd 11683 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℤ)
41 peano2zm 11622 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
4240, 41syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 − 1) ∈ ℤ)
43 uzid 11903 . . . . . . . . . . . . . 14 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
44 peano2uz 11943 . . . . . . . . . . . . . 14 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
4542, 43, 443syl 18 . . . . . . . . . . . . 13 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
4639, 45eqeltrrd 2851 . . . . . . . . . . . 12 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
47 fzss2 12588 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
4846, 47syl 17 . . . . . . . . . . 11 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
4948, 15sseldd 3753 . . . . . . . . . 10 (𝜑 → (2nd𝑇) ∈ (1...𝑁))
5017peano2nnd 11239 . . . . . . . . . . 11 (𝜑 → ((2nd𝑇) + 1) ∈ ℕ)
5142zred 11684 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ ℝ)
5236nnred 11237 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℝ)
53 elfzle2 12552 . . . . . . . . . . . . . 14 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ≤ (𝑁 − 1))
5415, 53syl 17 . . . . . . . . . . . . 13 (𝜑 → (2nd𝑇) ≤ (𝑁 − 1))
5552ltm1d 11158 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) < 𝑁)
5618, 51, 52, 54, 55lelttrd 10397 . . . . . . . . . . . 12 (𝜑 → (2nd𝑇) < 𝑁)
5717nnzd 11683 . . . . . . . . . . . . 13 (𝜑 → (2nd𝑇) ∈ ℤ)
58 zltp1le 11629 . . . . . . . . . . . . 13 (((2nd𝑇) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((2nd𝑇) < 𝑁 ↔ ((2nd𝑇) + 1) ≤ 𝑁))
5957, 40, 58syl2anc 565 . . . . . . . . . . . 12 (𝜑 → ((2nd𝑇) < 𝑁 ↔ ((2nd𝑇) + 1) ≤ 𝑁))
6056, 59mpbid 222 . . . . . . . . . . 11 (𝜑 → ((2nd𝑇) + 1) ≤ 𝑁)
61 fznn 12615 . . . . . . . . . . . 12 (𝑁 ∈ ℤ → (((2nd𝑇) + 1) ∈ (1...𝑁) ↔ (((2nd𝑇) + 1) ∈ ℕ ∧ ((2nd𝑇) + 1) ≤ 𝑁)))
6240, 61syl 17 . . . . . . . . . . 11 (𝜑 → (((2nd𝑇) + 1) ∈ (1...𝑁) ↔ (((2nd𝑇) + 1) ∈ ℕ ∧ ((2nd𝑇) + 1) ≤ 𝑁)))
6350, 60, 62mpbir2and 684 . . . . . . . . . 10 (𝜑 → ((2nd𝑇) + 1) ∈ (1...𝑁))
64 prssi 4487 . . . . . . . . . 10 (((2nd𝑇) ∈ (1...𝑁) ∧ ((2nd𝑇) + 1) ∈ (1...𝑁)) → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...𝑁))
6549, 63, 64syl2anc 565 . . . . . . . . 9 (𝜑 → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...𝑁))
66 undif 4191 . . . . . . . . 9 ({(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...𝑁) ↔ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = (1...𝑁))
6765, 66sylib 208 . . . . . . . 8 (𝜑 → ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = (1...𝑁))
68 f1oeq23 6271 . . . . . . . 8 ((({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = (1...𝑁) ∧ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = (1...𝑁)) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))):({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))–1-1-onto→({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) ↔ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))):(1...𝑁)–1-1-onto→(1...𝑁)))
6967, 67, 68syl2anc 565 . . . . . . 7 (𝜑 → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))):({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))–1-1-onto→({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) ↔ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))):(1...𝑁)–1-1-onto→(1...𝑁)))
7035, 69mpbid 222 . . . . . 6 (𝜑 → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))):(1...𝑁)–1-1-onto→(1...𝑁))
71 f1oco 6300 . . . . . 6 (((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ∧ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))):(1...𝑁)–1-1-onto→(1...𝑁)) → ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))):(1...𝑁)–1-1-onto→(1...𝑁))
7214, 70, 71syl2anc 565 . . . . 5 (𝜑 → ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))):(1...𝑁)–1-1-onto→(1...𝑁))
73 prex 5037 . . . . . . . 8 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∈ V
74 ovex 6823 . . . . . . . . 9 (1...𝑁) ∈ V
75 difexg 4942 . . . . . . . . 9 ((1...𝑁) ∈ V → ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ V)
76 resiexg 7249 . . . . . . . . 9 (((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ V → ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) ∈ V)
7774, 75, 76mp2b 10 . . . . . . . 8 ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) ∈ V
7873, 77unex 7103 . . . . . . 7 ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) ∈ V
7911, 78coex 7265 . . . . . 6 ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) ∈ V
80 f1oeq1 6268 . . . . . 6 (𝑓 = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))):(1...𝑁)–1-1-onto→(1...𝑁)))
8179, 80elab 3501 . . . . 5 (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))):(1...𝑁)–1-1-onto→(1...𝑁))
8272, 81sylibr 224 . . . 4 (𝜑 → ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
83 opelxpi 5288 . . . 4 (((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) ∧ ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
848, 82, 83syl2anc 565 . . 3 (𝜑 → ⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
85 fz1ssfz0 12643 . . . . 5 (1...𝑁) ⊆ (0...𝑁)
8648, 85syl6ss 3764 . . . 4 (𝜑 → (1...(𝑁 − 1)) ⊆ (0...𝑁))
8786, 15sseldd 3753 . . 3 (𝜑 → (2nd𝑇) ∈ (0...𝑁))
88 opelxpi 5288 . . 3 ((⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩ ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (2nd𝑇) ∈ (0...𝑁)) → ⟨⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩, (2nd𝑇)⟩ ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
8984, 87, 88syl2anc 565 . 2 (𝜑 → ⟨⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩, (2nd𝑇)⟩ ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
90 fveq2 6332 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
9190breq2d 4798 . . . . . . . . . . 11 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
9291ifbid 4247 . . . . . . . . . 10 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
9392csbeq1d 3689 . . . . . . . . 9 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
94 fveq2 6332 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (1st𝑡) = (1st𝑇))
9594fveq2d 6336 . . . . . . . . . . 11 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
9694fveq2d 6336 . . . . . . . . . . . . . 14 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
9796imaeq1d 5606 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
9897xpeq1d 5278 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
9996imaeq1d 5606 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
10099xpeq1d 5278 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
10198, 100uneq12d 3919 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
10295, 101oveq12d 6811 . . . . . . . . . 10 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
103102csbeq2dv 4136 . . . . . . . . 9 (𝑡 = 𝑇if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
10493, 103eqtrd 2805 . . . . . . . 8 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
105104mpteq2dv 4879 . . . . . . 7 (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
106105eqeq2d 2781 . . . . . 6 (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
107106, 3elrab2 3518 . . . . 5 (𝑇𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
108107simprbi 478 . . . 4 (𝑇𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
1091, 108syl 17 . . 3 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
110 imaco 5784 . . . . . . . . . 10 (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑦)) = ((2nd ‘(1st𝑇)) “ (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (1...𝑦)))
111 f1ofn 6279 . . . . . . . . . . . . . . . 16 ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd𝑇) + 1), (2nd𝑇)} → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} Fn {(2nd𝑇), ((2nd𝑇) + 1)})
11226, 111syl 17 . . . . . . . . . . . . . . 15 (𝜑 → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} Fn {(2nd𝑇), ((2nd𝑇) + 1)})
113112ad2antrr 697 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} Fn {(2nd𝑇), ((2nd𝑇) + 1)})
114 incom 3956 . . . . . . . . . . . . . . 15 ({(2nd𝑇), ((2nd𝑇) + 1)} ∩ (1...𝑦)) = ((1...𝑦) ∩ {(2nd𝑇), ((2nd𝑇) + 1)})
115 elfznn0 12640 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ0)
116115nn0red 11554 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
117 ltnle 10319 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ ℝ ∧ (2nd𝑇) ∈ ℝ) → (𝑦 < (2nd𝑇) ↔ ¬ (2nd𝑇) ≤ 𝑦))
118116, 18, 117syl2anr 576 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2nd𝑇) ↔ ¬ (2nd𝑇) ≤ 𝑦))
119118biimpa 462 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ¬ (2nd𝑇) ≤ 𝑦)
120 elfzle2 12552 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑇) ∈ (1...𝑦) → (2nd𝑇) ≤ 𝑦)
121119, 120nsyl 137 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ¬ (2nd𝑇) ∈ (1...𝑦))
122 disjsn 4383 . . . . . . . . . . . . . . . . . 18 (((1...𝑦) ∩ {(2nd𝑇)}) = ∅ ↔ ¬ (2nd𝑇) ∈ (1...𝑦))
123121, 122sylibr 224 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((1...𝑦) ∩ {(2nd𝑇)}) = ∅)
124116ad2antlr 698 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → 𝑦 ∈ ℝ)
12518ad2antrr 697 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (2nd𝑇) ∈ ℝ)
12650nnred 11237 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((2nd𝑇) + 1) ∈ ℝ)
127126ad2antrr 697 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((2nd𝑇) + 1) ∈ ℝ)
128 simpr 471 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → 𝑦 < (2nd𝑇))
12919ad2antrr 697 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (2nd𝑇) < ((2nd𝑇) + 1))
130124, 125, 127, 128, 129lttrd 10400 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → 𝑦 < ((2nd𝑇) + 1))
131 ltnle 10319 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℝ ∧ ((2nd𝑇) + 1) ∈ ℝ) → (𝑦 < ((2nd𝑇) + 1) ↔ ¬ ((2nd𝑇) + 1) ≤ 𝑦))
132116, 126, 131syl2anr 576 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < ((2nd𝑇) + 1) ↔ ¬ ((2nd𝑇) + 1) ≤ 𝑦))
133132adantr 466 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (𝑦 < ((2nd𝑇) + 1) ↔ ¬ ((2nd𝑇) + 1) ≤ 𝑦))
134130, 133mpbid 222 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ¬ ((2nd𝑇) + 1) ≤ 𝑦)
135 elfzle2 12552 . . . . . . . . . . . . . . . . . . 19 (((2nd𝑇) + 1) ∈ (1...𝑦) → ((2nd𝑇) + 1) ≤ 𝑦)
136134, 135nsyl 137 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ¬ ((2nd𝑇) + 1) ∈ (1...𝑦))
137 disjsn 4383 . . . . . . . . . . . . . . . . . 18 (((1...𝑦) ∩ {((2nd𝑇) + 1)}) = ∅ ↔ ¬ ((2nd𝑇) + 1) ∈ (1...𝑦))
138136, 137sylibr 224 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((1...𝑦) ∩ {((2nd𝑇) + 1)}) = ∅)
139123, 138uneq12d 3919 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (((1...𝑦) ∩ {(2nd𝑇)}) ∪ ((1...𝑦) ∩ {((2nd𝑇) + 1)})) = (∅ ∪ ∅))
140 df-pr 4319 . . . . . . . . . . . . . . . . . 18 {(2nd𝑇), ((2nd𝑇) + 1)} = ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)})
141140ineq2i 3962 . . . . . . . . . . . . . . . . 17 ((1...𝑦) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((1...𝑦) ∩ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)}))
142 indi 4022 . . . . . . . . . . . . . . . . 17 ((1...𝑦) ∩ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)})) = (((1...𝑦) ∩ {(2nd𝑇)}) ∪ ((1...𝑦) ∩ {((2nd𝑇) + 1)}))
143141, 142eqtr2i 2794 . . . . . . . . . . . . . . . 16 (((1...𝑦) ∩ {(2nd𝑇)}) ∪ ((1...𝑦) ∩ {((2nd𝑇) + 1)})) = ((1...𝑦) ∩ {(2nd𝑇), ((2nd𝑇) + 1)})
144 un0 4111 . . . . . . . . . . . . . . . 16 (∅ ∪ ∅) = ∅
145139, 143, 1443eqtr3g 2828 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((1...𝑦) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅)
146114, 145syl5eq 2817 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ({(2nd𝑇), ((2nd𝑇) + 1)} ∩ (1...𝑦)) = ∅)
147 fnimadisj 6152 . . . . . . . . . . . . . 14 (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} Fn {(2nd𝑇), ((2nd𝑇) + 1)} ∧ ({(2nd𝑇), ((2nd𝑇) + 1)} ∩ (1...𝑦)) = ∅) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...𝑦)) = ∅)
148113, 146, 147syl2anc 565 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...𝑦)) = ∅)
14939adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
150 elfzuz3 12546 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ𝑦))
151 peano2uz 11943 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 − 1) ∈ (ℤ𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
152150, 151syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
153152adantl 467 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
154149, 153eqeltrrd 2851 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ𝑦))
155 fzss2 12588 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝑦) → (1...𝑦) ⊆ (1...𝑁))
156 reldisj 4163 . . . . . . . . . . . . . . . . 17 ((1...𝑦) ⊆ (1...𝑁) → (((1...𝑦) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅ ↔ (1...𝑦) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
157154, 155, 1563syl 18 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((1...𝑦) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅ ↔ (1...𝑦) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
158157adantr 466 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (((1...𝑦) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅ ↔ (1...𝑦) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
159145, 158mpbid 222 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (1...𝑦) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
160 resiima 5621 . . . . . . . . . . . . . 14 ((1...𝑦) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (1...𝑦)) = (1...𝑦))
161159, 160syl 17 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (1...𝑦)) = (1...𝑦))
162148, 161uneq12d 3919 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...𝑦)) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (1...𝑦))) = (∅ ∪ (1...𝑦)))
163 imaundir 5687 . . . . . . . . . . . 12 (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (1...𝑦)) = (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...𝑦)) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (1...𝑦)))
164 uncom 3908 . . . . . . . . . . . . 13 (∅ ∪ (1...𝑦)) = ((1...𝑦) ∪ ∅)
165 un0 4111 . . . . . . . . . . . . 13 ((1...𝑦) ∪ ∅) = (1...𝑦)
166164, 165eqtr2i 2794 . . . . . . . . . . . 12 (1...𝑦) = (∅ ∪ (1...𝑦))
167162, 163, 1663eqtr4g 2830 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (1...𝑦)) = (1...𝑦))
168167imaeq2d 5607 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((2nd ‘(1st𝑇)) “ (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (1...𝑦))) = ((2nd ‘(1st𝑇)) “ (1...𝑦)))
169110, 168syl5eq 2817 . . . . . . . . 9 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑦)) = ((2nd ‘(1st𝑇)) “ (1...𝑦)))
170169xpeq1d 5278 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑦)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}))
171 imaco 5784 . . . . . . . . . 10 (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ ((𝑦 + 1)...𝑁)))
172 imaundir 5687 . . . . . . . . . . . . 13 (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ ((𝑦 + 1)...𝑁)) = (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ ((𝑦 + 1)...𝑁)) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ((𝑦 + 1)...𝑁)))
173 imassrn 5618 . . . . . . . . . . . . . . . . 17 ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ ((𝑦 + 1)...𝑁)) ⊆ ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}
174173a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ ((𝑦 + 1)...𝑁)) ⊆ ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
175 fnima 6150 . . . . . . . . . . . . . . . . . . 19 ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} Fn {(2nd𝑇), ((2nd𝑇) + 1)} → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ {(2nd𝑇), ((2nd𝑇) + 1)}) = ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
17626, 111, 1753syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ {(2nd𝑇), ((2nd𝑇) + 1)}) = ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
177176ad2antrr 697 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ {(2nd𝑇), ((2nd𝑇) + 1)}) = ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
178 elfzelz 12549 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
179 zltp1le 11629 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℤ ∧ (2nd𝑇) ∈ ℤ) → (𝑦 < (2nd𝑇) ↔ (𝑦 + 1) ≤ (2nd𝑇)))
180178, 57, 179syl2anr 576 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2nd𝑇) ↔ (𝑦 + 1) ≤ (2nd𝑇)))
181180biimpa 462 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (𝑦 + 1) ≤ (2nd𝑇))
18218, 52, 56ltled 10387 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2nd𝑇) ≤ 𝑁)
183182ad2antrr 697 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (2nd𝑇) ≤ 𝑁)
18457adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (2nd𝑇) ∈ ℤ)
185 nn0p1nn 11534 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℕ0 → (𝑦 + 1) ∈ ℕ)
186115, 185syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℕ)
187186nnzd 11683 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℤ)
188187adantl 467 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ ℤ)
18940adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℤ)
190 elfz 12539 . . . . . . . . . . . . . . . . . . . . . 22 (((2nd𝑇) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((2nd𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2nd𝑇) ∧ (2nd𝑇) ≤ 𝑁)))
191184, 188, 189, 190syl3anc 1476 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2nd𝑇) ∧ (2nd𝑇) ≤ 𝑁)))
192191adantr 466 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((2nd𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2nd𝑇) ∧ (2nd𝑇) ≤ 𝑁)))
193181, 183, 192mpbir2and 684 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (2nd𝑇) ∈ ((𝑦 + 1)...𝑁))
194 1red 10257 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → 1 ∈ ℝ)
195 ltle 10328 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ ℝ ∧ (2nd𝑇) ∈ ℝ) → (𝑦 < (2nd𝑇) → 𝑦 ≤ (2nd𝑇)))
196116, 18, 195syl2anr 576 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2nd𝑇) → 𝑦 ≤ (2nd𝑇)))
197196imp 393 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → 𝑦 ≤ (2nd𝑇))
198124, 125, 194, 197leadd1dd 10843 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (𝑦 + 1) ≤ ((2nd𝑇) + 1))
19960ad2antrr 697 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((2nd𝑇) + 1) ≤ 𝑁)
20057peano2zd 11687 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((2nd𝑇) + 1) ∈ ℤ)
201200adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd𝑇) + 1) ∈ ℤ)
202 elfz 12539 . . . . . . . . . . . . . . . . . . . . . 22 ((((2nd𝑇) + 1) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((2nd𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2nd𝑇) + 1) ∧ ((2nd𝑇) + 1) ≤ 𝑁)))
203201, 188, 189, 202syl3anc 1476 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2nd𝑇) + 1) ∧ ((2nd𝑇) + 1) ≤ 𝑁)))
204203adantr 466 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (((2nd𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2nd𝑇) + 1) ∧ ((2nd𝑇) + 1) ≤ 𝑁)))
205198, 199, 204mpbir2and 684 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((2nd𝑇) + 1) ∈ ((𝑦 + 1)...𝑁))
206 prssi 4487 . . . . . . . . . . . . . . . . . . 19 (((2nd𝑇) ∈ ((𝑦 + 1)...𝑁) ∧ ((2nd𝑇) + 1) ∈ ((𝑦 + 1)...𝑁)) → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁))
207193, 205, 206syl2anc 565 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁))
208 imass2 5642 . . . . . . . . . . . . . . . . . 18 ({(2nd𝑇), ((2nd𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ {(2nd𝑇), ((2nd𝑇) + 1)}) ⊆ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ ((𝑦 + 1)...𝑁)))
209207, 208syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ {(2nd𝑇), ((2nd𝑇) + 1)}) ⊆ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ ((𝑦 + 1)...𝑁)))
210177, 209eqsstr3d 3789 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ⊆ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ ((𝑦 + 1)...𝑁)))
211174, 210eqssd 3769 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ ((𝑦 + 1)...𝑁)) = ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
212 f1ofo 6285 . . . . . . . . . . . . . . . . . 18 ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd𝑇) + 1), (2nd𝑇)} → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–onto→{((2nd𝑇) + 1), (2nd𝑇)})
213 forn 6259 . . . . . . . . . . . . . . . . . 18 ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–onto→{((2nd𝑇) + 1), (2nd𝑇)} → ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = {((2nd𝑇) + 1), (2nd𝑇)})
21426, 212, 2133syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = {((2nd𝑇) + 1), (2nd𝑇)})
215214, 27syl6eq 2821 . . . . . . . . . . . . . . . 16 (𝜑 → ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = {(2nd𝑇), ((2nd𝑇) + 1)})
216215ad2antrr 697 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = {(2nd𝑇), ((2nd𝑇) + 1)})
217211, 216eqtrd 2805 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ ((𝑦 + 1)...𝑁)) = {(2nd𝑇), ((2nd𝑇) + 1)})
218 undif 4191 . . . . . . . . . . . . . . . . 17 ({(2nd𝑇), ((2nd𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁) ↔ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((𝑦 + 1)...𝑁))
219207, 218sylib 208 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((𝑦 + 1)...𝑁))
220219imaeq2d 5607 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ((𝑦 + 1)...𝑁)))
221 fnresi 6148 . . . . . . . . . . . . . . . . . . 19 ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) Fn ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})
222 incom 3956 . . . . . . . . . . . . . . . . . . . 20 (((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ({(2nd𝑇), ((2nd𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
223222, 32eqtri 2793 . . . . . . . . . . . . . . . . . . 19 (((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅
224 fnimadisj 6152 . . . . . . . . . . . . . . . . . . 19 ((( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) Fn ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∧ (((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅)
225221, 223, 224mp2an 664 . . . . . . . . . . . . . . . . . 18 (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅
226225a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅)
227 nnuz 11925 . . . . . . . . . . . . . . . . . . . . . 22 ℕ = (ℤ‘1)
228186, 227syl6eleq 2860 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (ℤ‘1))
229 fzss1 12587 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
230228, 229syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
231230ssdifd 3897 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
232 resiima 5621 . . . . . . . . . . . . . . . . . . 19 ((((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
233231, 232syl 17 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0...(𝑁 − 1)) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
234233ad2antlr 698 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
235226, 234uneq12d 3919 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (∅ ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
236 imaundi 5686 . . . . . . . . . . . . . . . 16 (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
237 uncom 3908 . . . . . . . . . . . . . . . . 17 (∅ ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ∅)
238 un0 4111 . . . . . . . . . . . . . . . . 17 ((((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ∅) = (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})
239237, 238eqtr2i 2794 . . . . . . . . . . . . . . . 16 (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) = (∅ ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
240235, 236, 2393eqtr4g 2830 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
241220, 240eqtr3d 2807 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ((𝑦 + 1)...𝑁)) = (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
242217, 241uneq12d 3919 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ ((𝑦 + 1)...𝑁)) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ((𝑦 + 1)...𝑁))) = ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
243172, 242syl5eq 2817 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ ((𝑦 + 1)...𝑁)) = ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
244243, 219eqtrd 2805 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ ((𝑦 + 1)...𝑁)) = ((𝑦 + 1)...𝑁))
245244imaeq2d 5607 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((2nd ‘(1st𝑇)) “ (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ ((𝑦 + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)))
246171, 245syl5eq 2817 . . . . . . . . 9 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)))
247246xpeq1d 5278 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))
248170, 247uneq12d 3919 . . . . . . 7 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))
249248oveq2d 6809 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
250 iftrue 4231 . . . . . . . . 9 (𝑦 < (2nd𝑇) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = 𝑦)
251250csbeq1d 3689 . . . . . . . 8 (𝑦 < (2nd𝑇) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑦 / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
252 vex 3354 . . . . . . . . 9 𝑦 ∈ V
253 oveq2 6801 . . . . . . . . . . . . 13 (𝑗 = 𝑦 → (1...𝑗) = (1...𝑦))
254253imaeq2d 5607 . . . . . . . . . . . 12 (𝑗 = 𝑦 → (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) = (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑦)))
255254xpeq1d 5278 . . . . . . . . . . 11 (𝑗 = 𝑦 → ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) = ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑦)) × {1}))
256 oveq1 6800 . . . . . . . . . . . . . 14 (𝑗 = 𝑦 → (𝑗 + 1) = (𝑦 + 1))
257256oveq1d 6808 . . . . . . . . . . . . 13 (𝑗 = 𝑦 → ((𝑗 + 1)...𝑁) = ((𝑦 + 1)...𝑁))
258257imaeq2d 5607 . . . . . . . . . . . 12 (𝑗 = 𝑦 → (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) = (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)))
259258xpeq1d 5278 . . . . . . . . . . 11 (𝑗 = 𝑦 → ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}) = ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0}))
260255, 259uneq12d 3919 . . . . . . . . . 10 (𝑗 = 𝑦 → (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0})) = (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0})))
261260oveq2d 6809 . . . . . . . . 9 (𝑗 = 𝑦 → ((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0}))))
262252, 261csbie 3708 . . . . . . . 8 𝑦 / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0})))
263251, 262syl6eq 2821 . . . . . . 7 (𝑦 < (2nd𝑇) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0}))))
264263adantl 467 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑦)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) × {0}))))
265250csbeq1d 3689 . . . . . . . 8 (𝑦 < (2nd𝑇) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑦 / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
266253imaeq2d 5607 . . . . . . . . . . . 12 (𝑗 = 𝑦 → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑦)))
267266xpeq1d 5278 . . . . . . . . . . 11 (𝑗 = 𝑦 → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}))
268257imaeq2d 5607 . . . . . . . . . . . 12 (𝑗 = 𝑦 → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)))
269268xpeq1d 5278 . . . . . . . . . . 11 (𝑗 = 𝑦 → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))
270267, 269uneq12d 3919 . . . . . . . . . 10 (𝑗 = 𝑦 → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))
271270oveq2d 6809 . . . . . . . . 9 (𝑗 = 𝑦 → ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
272252, 271csbie 3708 . . . . . . . 8 𝑦 / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))
273265, 272syl6eq 2821 . . . . . . 7 (𝑦 < (2nd𝑇) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
274273adantl 467 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
275249, 264, 2743eqtr4d 2815 . . . . 5 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
276 lenlt 10318 . . . . . . . . . 10 (((2nd𝑇) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((2nd𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd𝑇)))
27718, 116, 276syl2an 575 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd𝑇)))
278277biimpar 463 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2nd𝑇)) → (2nd𝑇) ≤ 𝑦)
279 imaco 5784 . . . . . . . . . . 11 (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...(𝑦 + 1))) = ((2nd ‘(1st𝑇)) “ (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (1...(𝑦 + 1))))
280 imaundir 5687 . . . . . . . . . . . . . 14 (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (1...(𝑦 + 1))) = (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...(𝑦 + 1))) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (1...(𝑦 + 1))))
281 imassrn 5618 . . . . . . . . . . . . . . . . . 18 ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...(𝑦 + 1))) ⊆ ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}
282281a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...(𝑦 + 1))) ⊆ ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
283176ad2antrr 697 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ {(2nd𝑇), ((2nd𝑇) + 1)}) = ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
28417ad2antrr 697 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (2nd𝑇) ∈ ℕ)
28518ad2antrr 697 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (2nd𝑇) ∈ ℝ)
286116ad2antlr 698 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → 𝑦 ∈ ℝ)
287186nnred 11237 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℝ)
288287ad2antlr 698 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (𝑦 + 1) ∈ ℝ)
289 simpr 471 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (2nd𝑇) ≤ 𝑦)
290116lep1d 11157 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑦 + 1))
291290ad2antlr 698 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → 𝑦 ≤ (𝑦 + 1))
292285, 286, 288, 289, 291letrd 10396 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (2nd𝑇) ≤ (𝑦 + 1))
293 fznn 12615 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 + 1) ∈ ℤ → ((2nd𝑇) ∈ (1...(𝑦 + 1)) ↔ ((2nd𝑇) ∈ ℕ ∧ (2nd𝑇) ≤ (𝑦 + 1))))
294187, 293syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd𝑇) ∈ (1...(𝑦 + 1)) ↔ ((2nd𝑇) ∈ ℕ ∧ (2nd𝑇) ≤ (𝑦 + 1))))
295294ad2antlr 698 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((2nd𝑇) ∈ (1...(𝑦 + 1)) ↔ ((2nd𝑇) ∈ ℕ ∧ (2nd𝑇) ≤ (𝑦 + 1))))
296284, 292, 295mpbir2and 684 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (2nd𝑇) ∈ (1...(𝑦 + 1)))
29750ad2antrr 697 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((2nd𝑇) + 1) ∈ ℕ)
298 1red 10257 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → 1 ∈ ℝ)
299285, 286, 298, 289leadd1dd 10843 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((2nd𝑇) + 1) ≤ (𝑦 + 1))
300 fznn 12615 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 + 1) ∈ ℤ → (((2nd𝑇) + 1) ∈ (1...(𝑦 + 1)) ↔ (((2nd𝑇) + 1) ∈ ℕ ∧ ((2nd𝑇) + 1) ≤ (𝑦 + 1))))
301187, 300syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (0...(𝑁 − 1)) → (((2nd𝑇) + 1) ∈ (1...(𝑦 + 1)) ↔ (((2nd𝑇) + 1) ∈ ℕ ∧ ((2nd𝑇) + 1) ≤ (𝑦 + 1))))
302301ad2antlr 698 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (((2nd𝑇) + 1) ∈ (1...(𝑦 + 1)) ↔ (((2nd𝑇) + 1) ∈ ℕ ∧ ((2nd𝑇) + 1) ≤ (𝑦 + 1))))
303297, 299, 302mpbir2and 684 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((2nd𝑇) + 1) ∈ (1...(𝑦 + 1)))
304 prssi 4487 . . . . . . . . . . . . . . . . . . . 20 (((2nd𝑇) ∈ (1...(𝑦 + 1)) ∧ ((2nd𝑇) + 1) ∈ (1...(𝑦 + 1))) → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...(𝑦 + 1)))
305296, 303, 304syl2anc 565 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...(𝑦 + 1)))
306 imass2 5642 . . . . . . . . . . . . . . . . . . 19 ({(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...(𝑦 + 1)) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ {(2nd𝑇), ((2nd𝑇) + 1)}) ⊆ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...(𝑦 + 1))))
307305, 306syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ {(2nd𝑇), ((2nd𝑇) + 1)}) ⊆ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...(𝑦 + 1))))
308283, 307eqsstr3d 3789 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ⊆ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...(𝑦 + 1))))
309282, 308eqssd 3769 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...(𝑦 + 1))) = ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
310215ad2antrr 697 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = {(2nd𝑇), ((2nd𝑇) + 1)})
311309, 310eqtrd 2805 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...(𝑦 + 1))) = {(2nd𝑇), ((2nd𝑇) + 1)})
312 undif 4191 . . . . . . . . . . . . . . . . . 18 ({(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...(𝑦 + 1)) ↔ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = (1...(𝑦 + 1)))
313305, 312sylib 208 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = (1...(𝑦 + 1)))
314313imaeq2d 5607 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (1...(𝑦 + 1))))
315225a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅)
316 eluzp1p1 11914 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 − 1) ∈ (ℤ𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
317150, 316syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
318317adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
319149, 318eqeltrrd 2851 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘(𝑦 + 1)))
320 fzss2 12588 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ (ℤ‘(𝑦 + 1)) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
321319, 320syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
322321ssdifd 3897 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
323322adantr 466 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
324 resiima 5621 . . . . . . . . . . . . . . . . . . 19 (((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
325323, 324syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
326315, 325uneq12d 3919 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (∅ ∪ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
327 imaundi 5686 . . . . . . . . . . . . . . . . 17 (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
328 uncom 3908 . . . . . . . . . . . . . . . . . 18 (∅ ∪ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = (((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ∅)
329 un0 4111 . . . . . . . . . . . . . . . . . 18 (((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ∅) = ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})
330328, 329eqtr2i 2794 . . . . . . . . . . . . . . . . 17 ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) = (∅ ∪ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
331326, 327, 3303eqtr4g 2830 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
332314, 331eqtr3d 2807 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (1...(𝑦 + 1))) = ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
333311, 332uneq12d 3919 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...(𝑦 + 1))) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (1...(𝑦 + 1)))) = ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
334280, 333syl5eq 2817 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (1...(𝑦 + 1))) = ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
335334, 313eqtrd 2805 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (1...(𝑦 + 1))) = (1...(𝑦 + 1)))
336335imaeq2d 5607 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((2nd ‘(1st𝑇)) “ (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (1...(𝑦 + 1)))) = ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
337279, 336syl5eq 2817 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...(𝑦 + 1))) = ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
338337xpeq1d 5278 . . . . . . . . 9 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}))
339 imaco 5784 . . . . . . . . . . 11 (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (((𝑦 + 1) + 1)...𝑁)))
340112ad2antrr 697 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} Fn {(2nd𝑇), ((2nd𝑇) + 1)})
341 incom 3956 . . . . . . . . . . . . . . . 16 ({(2nd𝑇), ((2nd𝑇) + 1)} ∩ (((𝑦 + 1) + 1)...𝑁)) = ((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)})
342126ad2antrr 697 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((2nd𝑇) + 1) ∈ ℝ)
343186peano2nnd 11239 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℕ)
344343nnred 11237 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℝ)
345344ad2antlr 698 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((𝑦 + 1) + 1) ∈ ℝ)
34619ad2antrr 697 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (2nd𝑇) < ((2nd𝑇) + 1))
347116ltp1d 11156 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 < (𝑦 + 1))
348347ad2antlr 698 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → 𝑦 < (𝑦 + 1))
349285, 286, 288, 289, 348lelttrd 10397 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (2nd𝑇) < (𝑦 + 1))
350285, 288, 298, 349ltadd1dd 10840 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((2nd𝑇) + 1) < ((𝑦 + 1) + 1))
351285, 342, 345, 346, 350lttrd 10400 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (2nd𝑇) < ((𝑦 + 1) + 1))
352 ltnle 10319 . . . . . . . . . . . . . . . . . . . . . . 23 (((2nd𝑇) ∈ ℝ ∧ ((𝑦 + 1) + 1) ∈ ℝ) → ((2nd𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2nd𝑇)))
35318, 344, 352syl2an 575 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2nd𝑇)))
354353adantr 466 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((2nd𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2nd𝑇)))
355351, 354mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ¬ ((𝑦 + 1) + 1) ≤ (2nd𝑇))
356 elfzle1 12551 . . . . . . . . . . . . . . . . . . . 20 ((2nd𝑇) ∈ (((𝑦 + 1) + 1)...𝑁) → ((𝑦 + 1) + 1) ≤ (2nd𝑇))
357355, 356nsyl 137 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ¬ (2nd𝑇) ∈ (((𝑦 + 1) + 1)...𝑁))
358 disjsn 4383 . . . . . . . . . . . . . . . . . . 19 (((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇)}) = ∅ ↔ ¬ (2nd𝑇) ∈ (((𝑦 + 1) + 1)...𝑁))
359357, 358sylibr 224 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇)}) = ∅)
360 ltnle 10319 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑇) + 1) ∈ ℝ ∧ ((𝑦 + 1) + 1) ∈ ℝ) → (((2nd𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2nd𝑇) + 1)))
361126, 344, 360syl2an 575 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2nd𝑇) + 1)))
362361adantr 466 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (((2nd𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2nd𝑇) + 1)))
363350, 362mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ¬ ((𝑦 + 1) + 1) ≤ ((2nd𝑇) + 1))
364 elfzle1 12551 . . . . . . . . . . . . . . . . . . . 20 (((2nd𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁) → ((𝑦 + 1) + 1) ≤ ((2nd𝑇) + 1))
365363, 364nsyl 137 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ¬ ((2nd𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁))
366 disjsn 4383 . . . . . . . . . . . . . . . . . . 19 (((((𝑦 + 1) + 1)...𝑁) ∩ {((2nd𝑇) + 1)}) = ∅ ↔ ¬ ((2nd𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁))
367365, 366sylibr 224 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {((2nd𝑇) + 1)}) = ∅)
368359, 367uneq12d 3919 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2nd𝑇) + 1)})) = (∅ ∪ ∅))
369140ineq2i 3962 . . . . . . . . . . . . . . . . . 18 ((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((((𝑦 + 1) + 1)...𝑁) ∩ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)}))
370 indi 4022 . . . . . . . . . . . . . . . . . 18 ((((𝑦 + 1) + 1)...𝑁) ∩ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)})) = (((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2nd𝑇) + 1)}))
371369, 370eqtr2i 2794 . . . . . . . . . . . . . . . . 17 (((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2nd𝑇) + 1)})) = ((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)})
372368, 371, 1443eqtr3g 2828 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅)
373341, 372syl5eq 2817 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ({(2nd𝑇), ((2nd𝑇) + 1)} ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
374 fnimadisj 6152 . . . . . . . . . . . . . . 15 (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} Fn {(2nd𝑇), ((2nd𝑇) + 1)} ∧ ({(2nd𝑇), ((2nd𝑇) + 1)} ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (((𝑦 + 1) + 1)...𝑁)) = ∅)
375340, 373, 374syl2anc 565 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (((𝑦 + 1) + 1)...𝑁)) = ∅)
376343, 227syl6eleq 2860 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ (ℤ‘1))
377 fzss1 12587 . . . . . . . . . . . . . . . . . 18 (((𝑦 + 1) + 1) ∈ (ℤ‘1) → (((𝑦 + 1) + 1)...𝑁) ⊆ (1...𝑁))
378 reldisj 4163 . . . . . . . . . . . . . . . . . 18 ((((𝑦 + 1) + 1)...𝑁) ⊆ (1...𝑁) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅ ↔ (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
379376, 377, 3783syl 18 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅ ↔ (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
380379ad2antlr 698 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅ ↔ (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))
381372, 380mpbid 222 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
382 resiima 5621 . . . . . . . . . . . . . . 15 ((((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (((𝑦 + 1) + 1)...𝑁)) = (((𝑦 + 1) + 1)...𝑁))
383381, 382syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (((𝑦 + 1) + 1)...𝑁)) = (((𝑦 + 1) + 1)...𝑁))
384375, 383uneq12d 3919 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (((𝑦 + 1) + 1)...𝑁)) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (((𝑦 + 1) + 1)...𝑁))) = (∅ ∪ (((𝑦 + 1) + 1)...𝑁)))
385 imaundir 5687 . . . . . . . . . . . . 13 (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (((𝑦 + 1) + 1)...𝑁)) = (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (((𝑦 + 1) + 1)...𝑁)) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (((𝑦 + 1) + 1)...𝑁)))
386 uncom 3908 . . . . . . . . . . . . . 14 (∅ ∪ (((𝑦 + 1) + 1)...𝑁)) = ((((𝑦 + 1) + 1)...𝑁) ∪ ∅)
387 un0 4111 . . . . . . . . . . . . . 14 ((((𝑦 + 1) + 1)...𝑁) ∪ ∅) = (((𝑦 + 1) + 1)...𝑁)
388386, 387eqtr2i 2794 . . . . . . . . . . . . 13 (((𝑦 + 1) + 1)...𝑁) = (∅ ∪ (((𝑦 + 1) + 1)...𝑁))
389384, 385, 3883eqtr4g 2830 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (((𝑦 + 1) + 1)...𝑁)) = (((𝑦 + 1) + 1)...𝑁))
390389imaeq2d 5607 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((2nd ‘(1st𝑇)) “ (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (((𝑦 + 1) + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
391339, 390syl5eq 2817 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
392391xpeq1d 5278 . . . . . . . . 9 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
393338, 392uneq12d 3919 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
394278, 393syldan 571 . . . . . . 7 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2nd𝑇)) → (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
395394oveq2d 6809 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2nd𝑇)) → ((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
396 iffalse 4234 . . . . . . . . 9 𝑦 < (2nd𝑇) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = (𝑦 + 1))
397396csbeq1d 3689 . . . . . . . 8 𝑦 < (2nd𝑇) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑦 + 1) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
398 ovex 6823 . . . . . . . . 9 (𝑦 + 1) ∈ V
399 oveq2 6801 . . . . . . . . . . . . 13 (𝑗 = (𝑦 + 1) → (1...𝑗) = (1...(𝑦 + 1)))
400399imaeq2d 5607 . . . . . . . . . . . 12 (𝑗 = (𝑦 + 1) → (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) = (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...(𝑦 + 1))))
401400xpeq1d 5278 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) = ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}))
402 oveq1 6800 . . . . . . . . . . . . . 14 (𝑗 = (𝑦 + 1) → (𝑗 + 1) = ((𝑦 + 1) + 1))
403402oveq1d 6808 . . . . . . . . . . . . 13 (𝑗 = (𝑦 + 1) → ((𝑗 + 1)...𝑁) = (((𝑦 + 1) + 1)...𝑁))
404403imaeq2d 5607 . . . . . . . . . . . 12 (𝑗 = (𝑦 + 1) → (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) = (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)))
405404xpeq1d 5278 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}) = ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
406401, 405uneq12d 3919 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0})) = (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
407406oveq2d 6809 . . . . . . . . 9 (𝑗 = (𝑦 + 1) → ((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
408398, 407csbie 3708 . . . . . . . 8 (𝑦 + 1) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
409397, 408syl6eq 2821 . . . . . . 7 𝑦 < (2nd𝑇) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
410409adantl 467 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2nd𝑇)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...(𝑦 + 1))) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
411396csbeq1d 3689 . . . . . . . 8 𝑦 < (2nd𝑇) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑦 + 1) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
412399imaeq2d 5607 . . . . . . . . . . . 12 (𝑗 = (𝑦 + 1) → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
413412xpeq1d 5278 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}))
414403imaeq2d 5607 . . . . . . . . . . . 12 (𝑗 = (𝑦 + 1) → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
415414xpeq1d 5278 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
416413, 415uneq12d 3919 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
417416oveq2d 6809 . . . . . . . . 9 (𝑗 = (𝑦 + 1) → ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
418398, 417csbie 3708 . . . . . . . 8 (𝑦 + 1) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
419411, 418syl6eq 2821 . . . . . . 7 𝑦 < (2nd𝑇) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
420419adantl 467 . . . . . 6 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2nd𝑇)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))
421395, 410, 4203eqtr4d 2815 . . . . 5 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2nd𝑇)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
422275, 421pm2.61dan 796 . . . 4 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
423422mpteq2dva 4878 . . 3 (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
424109, 423eqtr4d 2808 . 2 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0})))))
425 opex 5060 . . . . . . 7 ⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩ ∈ V
426425, 22op1std 7325 . . . . . 6 (𝑡 = ⟨⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩, (2nd𝑇)⟩ → (1st𝑡) = ⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩)
427425, 22op2ndd 7326 . . . . . 6 (𝑡 = ⟨⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩, (2nd𝑇)⟩ → (2nd𝑡) = (2nd𝑇))
428 breq2 4790 . . . . . . . . 9 ((2nd𝑡) = (2nd𝑇) → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
429428ifbid 4247 . . . . . . . 8 ((2nd𝑡) = (2nd𝑇) → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
430429csbeq1d 3689 . . . . . . 7 ((2nd𝑡) = (2nd𝑇) → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
431 fvex 6342 . . . . . . . . . 10 (1st ‘(1st𝑇)) ∈ V
432431, 79op1std 7325 . . . . . . . . 9 ((1st𝑡) = ⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩ → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
433431, 79op2ndd 7326 . . . . . . . . 9 ((1st𝑡) = ⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩ → (2nd ‘(1st𝑡)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))))
434 id 22 . . . . . . . . . 10 ((1st ‘(1st𝑡)) = (1st ‘(1st𝑇)) → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
435 imaeq1 5602 . . . . . . . . . . . 12 ((2nd ‘(1st𝑡)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)))
436435xpeq1d 5278 . . . . . . . . . . 11 ((2nd ‘(1st𝑡)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}))
437 imaeq1 5602 . . . . . . . . . . . 12 ((2nd ‘(1st𝑡)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)))
438437xpeq1d 5278 . . . . . . . . . . 11 ((2nd ‘(1st𝑡)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))
439436, 438uneq12d 3919 . . . . . . . . . 10 ((2nd ‘(1st𝑡)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0})))
440434, 439oveqan12d 6812 . . . . . . . . 9 (((1st ‘(1st𝑡)) = (1st ‘(1st𝑇)) ∧ (2nd ‘(1st𝑡)) = ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))) → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
441432, 433, 440syl2anc 565 . . . . . . . 8 ((1st𝑡) = ⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩ → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
442441csbeq2dv 4136 . . . . . . 7 ((1st𝑡) = ⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩ → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
443430, 442sylan9eqr 2827 . . . . . 6 (((1st𝑡) = ⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩ ∧ (2nd𝑡) = (2nd𝑇)) → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
444426, 427, 443syl2anc 565 . . . . 5 (𝑡 = ⟨⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩, (2nd𝑇)⟩ → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))
445444mpteq2dv 4879 . . . 4 (𝑡 = ⟨⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩, (2nd𝑇)⟩ → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0})))))
446445eqeq2d 2781 . . 3 (𝑡 = ⟨⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩, (2nd𝑇)⟩ → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))))
447446, 3elrab2 3518 . 2 (⟨⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩, (2nd𝑇)⟩ ∈ 𝑆 ↔ (⟨⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩, (2nd𝑇)⟩ ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + (((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑗)) × {1}) ∪ ((((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑗 + 1)...𝑁)) × {0}))))))
44889, 424, 447sylanbrc 564 1 (𝜑 → ⟨⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩, (2nd𝑇)⟩ ∈ 𝑆)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  {cab 2757  wne 2943  {crab 3065  Vcvv 3351  csb 3682  cdif 3720  cun 3721  cin 3722  wss 3723  c0 4063  ifcif 4225  {csn 4316  {cpr 4318  cop 4322   class class class wbr 4786  cmpt 4863   I cid 5156   × cxp 5247  ran crn 5250  cres 5251  cima 5252  ccom 5253   Fn wfn 6026  wf 6027  ontowfo 6029  1-1-ontowf1o 6030  cfv 6031  (class class class)co 6793  𝑓 cof 7042  1st c1st 7313  2nd c2nd 7314  𝑚 cmap 8009  cc 10136  cr 10137  0cc0 10138  1c1 10139   + caddc 10141   < clt 10276  cle 10277  cmin 10468  cn 11222  0cn0 11494  cz 11579  cuz 11888  ...cfz 12533  ..^cfzo 12673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-nn 11223  df-n0 11495  df-z 11580  df-uz 11889  df-fz 12534
This theorem is referenced by:  poimirlem22  33764
  Copyright terms: Public domain W3C validator