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

Theorem poimirlem15 33554
 Description: Lemma for poimir 33572, that the face in poimirlem22 33561 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 3391 . . . . . . 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 2748 . . . . . 6 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
51, 4syl 17 . . . . 5 (𝜑𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
6 xp1st 7242 . . . . 5 (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
7 xp1st 7242 . . . . 5 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
85, 6, 73syl 18 . . . 4 (𝜑 → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
9 xp2nd 7243 . . . . . . . 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 6239 . . . . . . . 8 (2nd ‘(1st𝑇)) ∈ V
12 f1oeq1 6165 . . . . . . . 8 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
1311, 12elab 3382 . . . . . . 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 12408 . . . . . . . . . . . . 13 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ∈ ℕ)
1715, 16syl 17 . . . . . . . . . . . 12 (𝜑 → (2nd𝑇) ∈ ℕ)
1817nnred 11073 . . . . . . . . . . 11 (𝜑 → (2nd𝑇) ∈ ℝ)
1918ltp1d 10992 . . . . . . . . . . 11 (𝜑 → (2nd𝑇) < ((2nd𝑇) + 1))
2018, 19ltned 10211 . . . . . . . . . 10 (𝜑 → (2nd𝑇) ≠ ((2nd𝑇) + 1))
2120necomd 2878 . . . . . . . . . 10 (𝜑 → ((2nd𝑇) + 1) ≠ (2nd𝑇))
22 fvex 6239 . . . . . . . . . . 11 (2nd𝑇) ∈ V
23 ovex 6718 . . . . . . . . . . 11 ((2nd𝑇) + 1) ∈ V
24 f1oprg 6219 . . . . . . . . . . 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 709 . . . . . . . . . 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 694 . . . . . . . . 9 (𝜑 → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩}:{(2nd𝑇), ((2nd𝑇) + 1)}–1-1-onto→{((2nd𝑇) + 1), (2nd𝑇)})
27 prcom 4299 . . . . . . . . . 10 {((2nd𝑇) + 1), (2nd𝑇)} = {(2nd𝑇), ((2nd𝑇) + 1)}
28 f1oeq3 6167 . . . . . . . . . 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 6212 . . . . . . . 8 ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})):((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})–1-1-onto→((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})
32 disjdif 4073 . . . . . . . . 9 ({(2nd𝑇), ((2nd𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ∅
33 f1oun 6194 . . . . . . . . 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 721 . . . . . . . 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 695 . . . . . . 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 11074 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℂ)
38 npcan1 10493 . . . . . . . . . . . . . 14 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
3937, 38syl 17 . . . . . . . . . . . . 13 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
4036nnzd 11519 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℤ)
41 peano2zm 11458 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
4240, 41syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 − 1) ∈ ℤ)
43 uzid 11740 . . . . . . . . . . . . . 14 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
44 peano2uz 11779 . . . . . . . . . . . . . 14 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
4542, 43, 443syl 18 . . . . . . . . . . . . 13 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
4639, 45eqeltrrd 2731 . . . . . . . . . . . 12 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
47 fzss2 12419 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
4846, 47syl 17 . . . . . . . . . . 11 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
4948, 15sseldd 3637 . . . . . . . . . 10 (𝜑 → (2nd𝑇) ∈ (1...𝑁))
5017peano2nnd 11075 . . . . . . . . . . 11 (𝜑 → ((2nd𝑇) + 1) ∈ ℕ)
5142zred 11520 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ ℝ)
5236nnred 11073 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℝ)
53 elfzle2 12383 . . . . . . . . . . . . . 14 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ≤ (𝑁 − 1))
5415, 53syl 17 . . . . . . . . . . . . 13 (𝜑 → (2nd𝑇) ≤ (𝑁 − 1))
5552ltm1d 10994 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) < 𝑁)
5618, 51, 52, 54, 55lelttrd 10233 . . . . . . . . . . . 12 (𝜑 → (2nd𝑇) < 𝑁)
5717nnzd 11519 . . . . . . . . . . . . 13 (𝜑 → (2nd𝑇) ∈ ℤ)
58 zltp1le 11465 . . . . . . . . . . . . 13 (((2nd𝑇) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((2nd𝑇) < 𝑁 ↔ ((2nd𝑇) + 1) ≤ 𝑁))
5957, 40, 58syl2anc 694 . . . . . . . . . . . 12 (𝜑 → ((2nd𝑇) < 𝑁 ↔ ((2nd𝑇) + 1) ≤ 𝑁))
6056, 59mpbid 222 . . . . . . . . . . 11 (𝜑 → ((2nd𝑇) + 1) ≤ 𝑁)
61 fznn 12446 . . . . . . . . . . . 12 (𝑁 ∈ ℤ → (((2nd𝑇) + 1) ∈ (1...𝑁) ↔ (((2nd𝑇) + 1) ∈ ℕ ∧ ((2nd𝑇) + 1) ≤ 𝑁)))
6240, 61syl 17 . . . . . . . . . . 11 (𝜑 → (((2nd𝑇) + 1) ∈ (1...𝑁) ↔ (((2nd𝑇) + 1) ∈ ℕ ∧ ((2nd𝑇) + 1) ≤ 𝑁)))
6350, 60, 62mpbir2and 977 . . . . . . . . . 10 (𝜑 → ((2nd𝑇) + 1) ∈ (1...𝑁))
64 prssi 4385 . . . . . . . . . 10 (((2nd𝑇) ∈ (1...𝑁) ∧ ((2nd𝑇) + 1) ∈ (1...𝑁)) → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...𝑁))
6549, 63, 64syl2anc 694 . . . . . . . . 9 (𝜑 → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...𝑁))
66 undif 4082 . . . . . . . . 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 6168 . . . . . . . 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 694 . . . . . . 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 6197 . . . . . 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 694 . . . . 5 (𝜑 → ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))):(1...𝑁)–1-1-onto→(1...𝑁))
73 prex 4939 . . . . . . . 8 {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∈ V
74 ovex 6718 . . . . . . . . 9 (1...𝑁) ∈ V
75 difexg 4841 . . . . . . . . 9 ((1...𝑁) ∈ V → ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∈ V)
76 resiexg 7144 . . . . . . . . 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 6998 . . . . . . 7 ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) ∈ V
7911, 78coex 7160 . . . . . 6 ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) ∈ V
80 f1oeq1 6165 . . . . . 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 3382 . . . . 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 5182 . . . 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 694 . . 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 12474 . . . . 5 (1...𝑁) ⊆ (0...𝑁)
8648, 85syl6ss 3648 . . . 4 (𝜑 → (1...(𝑁 − 1)) ⊆ (0...𝑁))
8786, 15sseldd 3637 . . 3 (𝜑 → (2nd𝑇) ∈ (0...𝑁))
88 opelxpi 5182 . . 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 694 . 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 6229 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
9190breq2d 4697 . . . . . . . . . . 11 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
9291ifbid 4141 . . . . . . . . . 10 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
9392csbeq1d 3573 . . . . . . . . 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 6229 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (1st𝑡) = (1st𝑇))
9594fveq2d 6233 . . . . . . . . . . 11 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
9694fveq2d 6233 . . . . . . . . . . . . . 14 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
9796imaeq1d 5500 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
9897xpeq1d 5172 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
9996imaeq1d 5500 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
10099xpeq1d 5172 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
10198, 100uneq12d 3801 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
10295, 101oveq12d 6708 . . . . . . . . . 10 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
103102csbeq2dv 4025 . . . . . . . . 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 2685 . . . . . . . 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 4778 . . . . . . 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 2661 . . . . . 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 3399 . . . . 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 479 . . . 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 5678 . . . . . . . . . 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 6176 . . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} Fn {(2nd𝑇), ((2nd𝑇) + 1)})
114 incom 3838 . . . . . . . . . . . . . . 15 ({(2nd𝑇), ((2nd𝑇) + 1)} ∩ (1...𝑦)) = ((1...𝑦) ∩ {(2nd𝑇), ((2nd𝑇) + 1)})
115 elfznn0 12471 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ0)
116115nn0red 11390 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
117 ltnle 10155 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ ℝ ∧ (2nd𝑇) ∈ ℝ) → (𝑦 < (2nd𝑇) ↔ ¬ (2nd𝑇) ≤ 𝑦))
118116, 18, 117syl2anr 494 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2nd𝑇) ↔ ¬ (2nd𝑇) ≤ 𝑦))
119118biimpa 500 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ¬ (2nd𝑇) ≤ 𝑦)
120 elfzle2 12383 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑇) ∈ (1...𝑦) → (2nd𝑇) ≤ 𝑦)
121119, 120nsyl 135 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ¬ (2nd𝑇) ∈ (1...𝑦))
122 disjsn 4278 . . . . . . . . . . . . . . . . . 18 (((1...𝑦) ∩ {(2nd𝑇)}) = ∅ ↔ ¬ (2nd𝑇) ∈ (1...𝑦))
123121, 122sylibr 224 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((1...𝑦) ∩ {(2nd𝑇)}) = ∅)
124116ad2antlr 763 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → 𝑦 ∈ ℝ)
12518ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (2nd𝑇) ∈ ℝ)
12650nnred 11073 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((2nd𝑇) + 1) ∈ ℝ)
127126ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((2nd𝑇) + 1) ∈ ℝ)
128 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → 𝑦 < (2nd𝑇))
12919ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (2nd𝑇) < ((2nd𝑇) + 1))
130124, 125, 127, 128, 129lttrd 10236 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → 𝑦 < ((2nd𝑇) + 1))
131 ltnle 10155 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℝ ∧ ((2nd𝑇) + 1) ∈ ℝ) → (𝑦 < ((2nd𝑇) + 1) ↔ ¬ ((2nd𝑇) + 1) ≤ 𝑦))
132116, 126, 131syl2anr 494 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < ((2nd𝑇) + 1) ↔ ¬ ((2nd𝑇) + 1) ≤ 𝑦))
133132adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (𝑦 < ((2nd𝑇) + 1) ↔ ¬ ((2nd𝑇) + 1) ≤ 𝑦))
134130, 133mpbid 222 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ¬ ((2nd𝑇) + 1) ≤ 𝑦)
135 elfzle2 12383 . . . . . . . . . . . . . . . . . . 19 (((2nd𝑇) + 1) ∈ (1...𝑦) → ((2nd𝑇) + 1) ≤ 𝑦)
136134, 135nsyl 135 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ¬ ((2nd𝑇) + 1) ∈ (1...𝑦))
137 disjsn 4278 . . . . . . . . . . . . . . . . . 18 (((1...𝑦) ∩ {((2nd𝑇) + 1)}) = ∅ ↔ ¬ ((2nd𝑇) + 1) ∈ (1...𝑦))
138136, 137sylibr 224 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((1...𝑦) ∩ {((2nd𝑇) + 1)}) = ∅)
139123, 138uneq12d 3801 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (((1...𝑦) ∩ {(2nd𝑇)}) ∪ ((1...𝑦) ∩ {((2nd𝑇) + 1)})) = (∅ ∪ ∅))
140 df-pr 4213 . . . . . . . . . . . . . . . . . 18 {(2nd𝑇), ((2nd𝑇) + 1)} = ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)})
141140ineq2i 3844 . . . . . . . . . . . . . . . . 17 ((1...𝑦) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((1...𝑦) ∩ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)}))
142 indi 3906 . . . . . . . . . . . . . . . . 17 ((1...𝑦) ∩ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)})) = (((1...𝑦) ∩ {(2nd𝑇)}) ∪ ((1...𝑦) ∩ {((2nd𝑇) + 1)}))
143141, 142eqtr2i 2674 . . . . . . . . . . . . . . . 16 (((1...𝑦) ∩ {(2nd𝑇)}) ∪ ((1...𝑦) ∩ {((2nd𝑇) + 1)})) = ((1...𝑦) ∩ {(2nd𝑇), ((2nd𝑇) + 1)})
144 un0 4000 . . . . . . . . . . . . . . . 16 (∅ ∪ ∅) = ∅
145139, 143, 1443eqtr3g 2708 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((1...𝑦) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅)
146114, 145syl5eq 2697 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ({(2nd𝑇), ((2nd𝑇) + 1)} ∩ (1...𝑦)) = ∅)
147 fnimadisj 6050 . . . . . . . . . . . . . 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 694 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...𝑦)) = ∅)
14939adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
150 elfzuz3 12377 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ𝑦))
151 peano2uz 11779 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 − 1) ∈ (ℤ𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
152150, 151syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
153152adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ𝑦))
154149, 153eqeltrrd 2731 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ𝑦))
155 fzss2 12419 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝑦) → (1...𝑦) ⊆ (1...𝑁))
156 reldisj 4053 . . . . . . . . . . . . . . . . 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 480 . . . . . . . . . . . . . . 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 5515 . . . . . . . . . . . . . 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 3801 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...𝑦)) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (1...𝑦))) = (∅ ∪ (1...𝑦)))
163 imaundir 5581 . . . . . . . . . . . 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 3790 . . . . . . . . . . . . 13 (∅ ∪ (1...𝑦)) = ((1...𝑦) ∪ ∅)
165 un0 4000 . . . . . . . . . . . . 13 ((1...𝑦) ∪ ∅) = (1...𝑦)
166164, 165eqtr2i 2674 . . . . . . . . . . . 12 (1...𝑦) = (∅ ∪ (1...𝑦))
167162, 163, 1663eqtr4g 2710 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (1...𝑦)) = (1...𝑦))
168167imaeq2d 5501 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((2nd ‘(1st𝑇)) “ (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (1...𝑦))) = ((2nd ‘(1st𝑇)) “ (1...𝑦)))
169110, 168syl5eq 2697 . . . . . . . . 9 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...𝑦)) = ((2nd ‘(1st𝑇)) “ (1...𝑦)))
170169xpeq1d 5172 . . . . . . . 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 5678 . . . . . . . . . 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 5581 . . . . . . . . . . . . 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 5512 . . . . . . . . . . . . . . . . 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 6048 . . . . . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ {(2nd𝑇), ((2nd𝑇) + 1)}) = ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
178 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
179 zltp1le 11465 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℤ ∧ (2nd𝑇) ∈ ℤ) → (𝑦 < (2nd𝑇) ↔ (𝑦 + 1) ≤ (2nd𝑇)))
180178, 57, 179syl2anr 494 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2nd𝑇) ↔ (𝑦 + 1) ≤ (2nd𝑇)))
181180biimpa 500 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (𝑦 + 1) ≤ (2nd𝑇))
18218, 52, 56ltled 10223 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2nd𝑇) ≤ 𝑁)
183182ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (2nd𝑇) ≤ 𝑁)
18457adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (2nd𝑇) ∈ ℤ)
185 nn0p1nn 11370 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℕ0 → (𝑦 + 1) ∈ ℕ)
186115, 185syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℕ)
187186nnzd 11519 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℤ)
188187adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ ℤ)
18940adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℤ)
190 elfz 12370 . . . . . . . . . . . . . . . . . . . . . 22 (((2nd𝑇) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((2nd𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2nd𝑇) ∧ (2nd𝑇) ≤ 𝑁)))
191184, 188, 189, 190syl3anc 1366 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2nd𝑇) ∧ (2nd𝑇) ≤ 𝑁)))
192191adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((2nd𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2nd𝑇) ∧ (2nd𝑇) ≤ 𝑁)))
193181, 183, 192mpbir2and 977 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (2nd𝑇) ∈ ((𝑦 + 1)...𝑁))
194 1red 10093 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → 1 ∈ ℝ)
195 ltle 10164 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ ℝ ∧ (2nd𝑇) ∈ ℝ) → (𝑦 < (2nd𝑇) → 𝑦 ≤ (2nd𝑇)))
196116, 18, 195syl2anr 494 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2nd𝑇) → 𝑦 ≤ (2nd𝑇)))
197196imp 444 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → 𝑦 ≤ (2nd𝑇))
198124, 125, 194, 197leadd1dd 10679 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (𝑦 + 1) ≤ ((2nd𝑇) + 1))
19960ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((2nd𝑇) + 1) ≤ 𝑁)
20057peano2zd 11523 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((2nd𝑇) + 1) ∈ ℤ)
201200adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd𝑇) + 1) ∈ ℤ)
202 elfz 12370 . . . . . . . . . . . . . . . . . . . . . 22 ((((2nd𝑇) + 1) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((2nd𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2nd𝑇) + 1) ∧ ((2nd𝑇) + 1) ≤ 𝑁)))
203201, 188, 189, 202syl3anc 1366 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2nd𝑇) + 1) ∧ ((2nd𝑇) + 1) ≤ 𝑁)))
204203adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (((2nd𝑇) + 1) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2nd𝑇) + 1) ∧ ((2nd𝑇) + 1) ≤ 𝑁)))
205198, 199, 204mpbir2and 977 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((2nd𝑇) + 1) ∈ ((𝑦 + 1)...𝑁))
206 prssi 4385 . . . . . . . . . . . . . . . . . . 19 (((2nd𝑇) ∈ ((𝑦 + 1)...𝑁) ∧ ((2nd𝑇) + 1) ∈ ((𝑦 + 1)...𝑁)) → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁))
207193, 205, 206syl2anc 694 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁))
208 imass2 5536 . . . . . . . . . . . . . . . . . 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 3673 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ⊆ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ ((𝑦 + 1)...𝑁)))
211174, 210eqssd 3653 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ ((𝑦 + 1)...𝑁)) = ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
212 f1ofo 6182 . . . . . . . . . . . . . . . . . 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 6156 . . . . . . . . . . . . . . . . . 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 2701 . . . . . . . . . . . . . . . 16 (𝜑 → ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = {(2nd𝑇), ((2nd𝑇) + 1)})
216215ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = {(2nd𝑇), ((2nd𝑇) + 1)})
217211, 216eqtrd 2685 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ ((𝑦 + 1)...𝑁)) = {(2nd𝑇), ((2nd𝑇) + 1)})
218 undif 4082 . . . . . . . . . . . . . . . . 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 5501 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ((𝑦 + 1)...𝑁)))
221 fnresi 6046 . . . . . . . . . . . . . . . . . . 19 ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) Fn ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})
222 incom 3838 . . . . . . . . . . . . . . . . . . . 20 (((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ({(2nd𝑇), ((2nd𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
223222, 32eqtri 2673 . . . . . . . . . . . . . . . . . . 19 (((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅
224 fnimadisj 6050 . . . . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . . 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 11761 . . . . . . . . . . . . . . . . . . . . . 22 ℕ = (ℤ‘1)
228186, 227syl6eleq 2740 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (ℤ‘1))
229 fzss1 12418 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 + 1) ∈ (ℤ‘1) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
230228, 229syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁))
231230ssdifd 3779 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (0...(𝑁 − 1)) → (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
232 resiima 5515 . . . . . . . . . . . . . . . . . . 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 763 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
235226, 234uneq12d 3801 . . . . . . . . . . . . . . . 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 5580 . . . . . . . . . . . . . . . 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 3790 . . . . . . . . . . . . . . . . 17 (∅ ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = ((((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ∅)
238 un0 4000 . . . . . . . . . . . . . . . . 17 ((((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ∅) = (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})
239237, 238eqtr2i 2674 . . . . . . . . . . . . . . . 16 (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) = (∅ ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
240235, 236, 2393eqtr4g 2710 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
241220, 240eqtr3d 2687 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ((𝑦 + 1)...𝑁)) = (((𝑦 + 1)...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
242217, 241uneq12d 3801 . . . . . . . . . . . . 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 2697 . . . . . . . . . . . 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 2685 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ ((𝑦 + 1)...𝑁)) = ((𝑦 + 1)...𝑁))
245244imaeq2d 5501 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → ((2nd ‘(1st𝑇)) “ (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ ((𝑦 + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)))
246171, 245syl5eq 2697 . . . . . . . . 9 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd𝑇)) → (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ ((𝑦 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)))
247246xpeq1d 5172 . . . . . . . 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 3801 . . . . . . 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 6706 . . . . . 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 4125 . . . . . . . . 9 (𝑦 < (2nd𝑇) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = 𝑦)
251250csbeq1d 3573 . . . . . . . 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 3234 . . . . . . . . 9 𝑦 ∈ V
253 oveq2 6698 . . . . . . . . . . . . 13 (𝑗 = 𝑦 → (1...𝑗) = (1...𝑦))
254253imaeq2d 5501 . . . . . . . . . . . 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 5172 . . . . . . . . . . 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 6697 . . . . . . . . . . . . . 14 (𝑗 = 𝑦 → (𝑗 + 1) = (𝑦 + 1))
257256oveq1d 6705 . . . . . . . . . . . . 13 (𝑗 = 𝑦 → ((𝑗 + 1)...𝑁) = ((𝑦 + 1)...𝑁))
258257imaeq2d 5501 . . . . . . . . . . . 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 5172 . . . . . . . . . . 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 3801 . . . . . . . . . 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 6706 . . . . . . . . 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 3592 . . . . . . . 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 2701 . . . . . . 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 481 . . . . . 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 3573 . . . . . . . 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 5501 . . . . . . . . . . . 12 (𝑗 = 𝑦 → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑦)))
267266xpeq1d 5172 . . . . . . . . . . 11 (𝑗 = 𝑦 → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}))
268257imaeq2d 5501 . . . . . . . . . . . 12 (𝑗 = 𝑦 → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)))
269268xpeq1d 5172 . . . . . . . . . . 11 (𝑗 = 𝑦 → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))
270267, 269uneq12d 3801 . . . . . . . . . 10 (𝑗 = 𝑦 → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))
271270oveq2d 6706 . . . . . . . . 9 (𝑗 = 𝑦 → ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))))
272252, 271csbie 3592 . . . . . . . 8 𝑦 / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))
273265, 272syl6eq 2701 . . . . . . 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 481 . . . . . 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 2695 . . . . 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 10154 . . . . . . . . . 10 (((2nd𝑇) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((2nd𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd𝑇)))
27718, 116, 276syl2an 493 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd𝑇)))
278277biimpar 501 . . . . . . . 8 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2nd𝑇)) → (2nd𝑇) ≤ 𝑦)
279 imaco 5678 . . . . . . . . . . 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 5581 . . . . . . . . . . . . . 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 5512 . . . . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ {(2nd𝑇), ((2nd𝑇) + 1)}) = ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
28417ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (2nd𝑇) ∈ ℕ)
28518ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (2nd𝑇) ∈ ℝ)
286116ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → 𝑦 ∈ ℝ)
287186nnred 11073 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℝ)
288287ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (𝑦 + 1) ∈ ℝ)
289 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (2nd𝑇) ≤ 𝑦)
290116lep1d 10993 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑦 + 1))
291290ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → 𝑦 ≤ (𝑦 + 1))
292285, 286, 288, 289, 291letrd 10232 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (2nd𝑇) ≤ (𝑦 + 1))
293 fznn 12446 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 + 1) ∈ ℤ → ((2nd𝑇) ∈ (1...(𝑦 + 1)) ↔ ((2nd𝑇) ∈ ℕ ∧ (2nd𝑇) ≤ (𝑦 + 1))))
294187, 293syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd𝑇) ∈ (1...(𝑦 + 1)) ↔ ((2nd𝑇) ∈ ℕ ∧ (2nd𝑇) ≤ (𝑦 + 1))))
295294ad2antlr 763 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((2nd𝑇) ∈ (1...(𝑦 + 1)) ↔ ((2nd𝑇) ∈ ℕ ∧ (2nd𝑇) ≤ (𝑦 + 1))))
296284, 292, 295mpbir2and 977 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (2nd𝑇) ∈ (1...(𝑦 + 1)))
29750ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((2nd𝑇) + 1) ∈ ℕ)
298 1red 10093 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → 1 ∈ ℝ)
299285, 286, 298, 289leadd1dd 10679 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((2nd𝑇) + 1) ≤ (𝑦 + 1))
300 fznn 12446 . . . . . . . . . . . . . . . . . . . . . . 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 763 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (((2nd𝑇) + 1) ∈ (1...(𝑦 + 1)) ↔ (((2nd𝑇) + 1) ∈ ℕ ∧ ((2nd𝑇) + 1) ≤ (𝑦 + 1))))
303297, 299, 302mpbir2and 977 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((2nd𝑇) + 1) ∈ (1...(𝑦 + 1)))
304 prssi 4385 . . . . . . . . . . . . . . . . . . . 20 (((2nd𝑇) ∈ (1...(𝑦 + 1)) ∧ ((2nd𝑇) + 1) ∈ (1...(𝑦 + 1))) → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...(𝑦 + 1)))
305296, 303, 304syl2anc 694 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → {(2nd𝑇), ((2nd𝑇) + 1)} ⊆ (1...(𝑦 + 1)))
306 imass2 5536 . . . . . . . . . . . . . . . . . . 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 3673 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ⊆ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...(𝑦 + 1))))
309282, 308eqssd 3653 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...(𝑦 + 1))) = ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩})
310215ad2antrr 762 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ran {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} = {(2nd𝑇), ((2nd𝑇) + 1)})
311309, 310eqtrd 2685 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (1...(𝑦 + 1))) = {(2nd𝑇), ((2nd𝑇) + 1)})
312 undif 4082 . . . . . . . . . . . . . . . . . 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 5501 . . . . . . . . . . . . . . . 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 11751 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 − 1) ∈ (ℤ𝑦) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
317150, 316syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
318317adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑦 + 1)))
319149, 318eqeltrrd 2731 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘(𝑦 + 1)))
320 fzss2 12419 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ (ℤ‘(𝑦 + 1)) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
321319, 320syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (1...(𝑦 + 1)) ⊆ (1...𝑁))
322321ssdifd 3779 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
323322adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
324 resiima 5515 . . . . . . . . . . . . . . . . . . 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 3801 . . . . . . . . . . . . . . . . 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 5580 . . . . . . . . . . . . . . . . 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 3790 . . . . . . . . . . . . . . . . . 18 (∅ ∪ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) = (((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ∅)
329 un0 4000 . . . . . . . . . . . . . . . . . 18 (((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) ∪ ∅) = ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})
330328, 329eqtr2i 2674 . . . . . . . . . . . . . . . . 17 ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}) = (∅ ∪ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
331326, 327, 3303eqtr4g 2710 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ ({(2nd𝑇), ((2nd𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) = ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
332314, 331eqtr3d 2687 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (1...(𝑦 + 1))) = ((1...(𝑦 + 1)) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))
333311, 332uneq12d 3801 . . . . . . . . . . . . . 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 2697 . . . . . . . . . . . . 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 2685 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (1...(𝑦 + 1))) = (1...(𝑦 + 1)))
336335imaeq2d 5501 . . . . . . . . . . 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 2697 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (1...(𝑦 + 1))) = ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
338337xpeq1d 5172 . . . . . . . . 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 5678 . . . . . . . . . . 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 762 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → {⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} Fn {(2nd𝑇), ((2nd𝑇) + 1)})
341 incom 3838 . . . . . . . . . . . . . . . 16 ({(2nd𝑇), ((2nd𝑇) + 1)} ∩ (((𝑦 + 1) + 1)...𝑁)) = ((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)})
342126ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((2nd𝑇) + 1) ∈ ℝ)
343186peano2nnd 11075 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℕ)
344343nnred 11073 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℝ)
345344ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((𝑦 + 1) + 1) ∈ ℝ)
34619ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (2nd𝑇) < ((2nd𝑇) + 1))
347116ltp1d 10992 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 < (𝑦 + 1))
348347ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → 𝑦 < (𝑦 + 1))
349285, 286, 288, 289, 348lelttrd 10233 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (2nd𝑇) < (𝑦 + 1))
350285, 288, 298, 349ltadd1dd 10676 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((2nd𝑇) + 1) < ((𝑦 + 1) + 1))
351285, 342, 345, 346, 350lttrd 10236 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (2nd𝑇) < ((𝑦 + 1) + 1))
352 ltnle 10155 . . . . . . . . . . . . . . . . . . . . . . 23 (((2nd𝑇) ∈ ℝ ∧ ((𝑦 + 1) + 1) ∈ ℝ) → ((2nd𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2nd𝑇)))
35318, 344, 352syl2an 493 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → ((2nd𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2nd𝑇)))
354353adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((2nd𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2nd𝑇)))
355351, 354mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ¬ ((𝑦 + 1) + 1) ≤ (2nd𝑇))
356 elfzle1 12382 . . . . . . . . . . . . . . . . . . . 20 ((2nd𝑇) ∈ (((𝑦 + 1) + 1)...𝑁) → ((𝑦 + 1) + 1) ≤ (2nd𝑇))
357355, 356nsyl 135 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ¬ (2nd𝑇) ∈ (((𝑦 + 1) + 1)...𝑁))
358 disjsn 4278 . . . . . . . . . . . . . . . . . . 19 (((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇)}) = ∅ ↔ ¬ (2nd𝑇) ∈ (((𝑦 + 1) + 1)...𝑁))
359357, 358sylibr 224 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇)}) = ∅)
360 ltnle 10155 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑇) + 1) ∈ ℝ ∧ ((𝑦 + 1) + 1) ∈ ℝ) → (((2nd𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2nd𝑇) + 1)))
361126, 344, 360syl2an 493 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (((2nd𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2nd𝑇) + 1)))
362361adantr 480 . . . . . . . . . . . . . . . . . . . . 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 12382 . . . . . . . . . . . . . . . . . . . 20 (((2nd𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁) → ((𝑦 + 1) + 1) ≤ ((2nd𝑇) + 1))
365363, 364nsyl 135 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ¬ ((2nd𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁))
366 disjsn 4278 . . . . . . . . . . . . . . . . . . 19 (((((𝑦 + 1) + 1)...𝑁) ∩ {((2nd𝑇) + 1)}) = ∅ ↔ ¬ ((2nd𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁))
367365, 366sylibr 224 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {((2nd𝑇) + 1)}) = ∅)
368359, 367uneq12d 3801 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2nd𝑇) + 1)})) = (∅ ∪ ∅))
369140ineq2i 3844 . . . . . . . . . . . . . . . . . 18 ((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ((((𝑦 + 1) + 1)...𝑁) ∩ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)}))
370 indi 3906 . . . . . . . . . . . . . . . . . 18 ((((𝑦 + 1) + 1)...𝑁) ∩ ({(2nd𝑇)} ∪ {((2nd𝑇) + 1)})) = (((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2nd𝑇) + 1)}))
371369, 370eqtr2i 2674 . . . . . . . . . . . . . . . . 17 (((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2nd𝑇) + 1)})) = ((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)})
372368, 371, 1443eqtr3g 2708 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd𝑇), ((2nd𝑇) + 1)}) = ∅)
373341, 372syl5eq 2697 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ({(2nd𝑇), ((2nd𝑇) + 1)} ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅)
374 fnimadisj 6050 . . . . . . . . . . . . . . 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 694 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (((𝑦 + 1) + 1)...𝑁)) = ∅)
376343, 227syl6eleq 2740 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ (ℤ‘1))
377 fzss1 12418 . . . . . . . . . . . . . . . . . 18 (((𝑦 + 1) + 1) ∈ (ℤ‘1) → (((𝑦 + 1) + 1)...𝑁) ⊆ (1...𝑁))
378 reldisj 4053 . . . . . . . . . . . . . . . . . 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 763 . . . . . . . . . . . . . . . 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 5515 . . . . . . . . . . . . . . 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 3801 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} “ (((𝑦 + 1) + 1)...𝑁)) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})) “ (((𝑦 + 1) + 1)...𝑁))) = (∅ ∪ (((𝑦 + 1) + 1)...𝑁)))
385 imaundir 5581 . . . . . . . . . . . . 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 3790 . . . . . . . . . . . . . 14 (∅ ∪ (((𝑦 + 1) + 1)...𝑁)) = ((((𝑦 + 1) + 1)...𝑁) ∪ ∅)
387 un0 4000 . . . . . . . . . . . . . 14 ((((𝑦 + 1) + 1)...𝑁) ∪ ∅) = (((𝑦 + 1) + 1)...𝑁)
388386, 387eqtr2i 2674 . . . . . . . . . . . . 13 (((𝑦 + 1) + 1)...𝑁) = (∅ ∪ (((𝑦 + 1) + 1)...𝑁))
389384, 385, 3883eqtr4g 2710 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))) “ (((𝑦 + 1) + 1)...𝑁)) = (((𝑦 + 1) + 1)...𝑁))
390389imaeq2d 5501 . . . . . . . . . . 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 2697 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd𝑇) ≤ 𝑦) → (((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)})))) “ (((𝑦 + 1) + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
392391xpeq1d 5172 . . . . . . . . 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 3801 . . . . . . . 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 486 . . . . . . 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 6706 . . . . . 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 4128 . . . . . . . . 9 𝑦 < (2nd𝑇) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = (𝑦 + 1))
397396csbeq1d 3573 . . . . . . . 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 6718 . . . . . . . . 9 (𝑦 + 1) ∈ V
399 oveq2 6698 . . . . . . . . . . . . 13 (𝑗 = (𝑦 + 1) → (1...𝑗) = (1...(𝑦 + 1)))
400399imaeq2d 5501 . . . . . . . . . . . 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 5172 . . . . . . . . . . 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 6697 . . . . . . . . . . . . . 14 (𝑗 = (𝑦 + 1) → (𝑗 + 1) = ((𝑦 + 1) + 1))
403402oveq1d 6705 . . . . . . . . . . . . 13 (𝑗 = (𝑦 + 1) → ((𝑗 + 1)...𝑁) = (((𝑦 + 1) + 1)...𝑁))
404403imaeq2d 5501 . . . . . . . . . . . 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 5172 . . . . . . . . . . 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 3801 . . . . . . . . . 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 6706 . . . . . . . . 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 3592 . . . . . . . 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 2701 . . . . . . 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 481 . . . . . 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 3573 . . . . . . . 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 5501 . . . . . . . . . . . 12 (𝑗 = (𝑦 + 1) → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))))
413412xpeq1d 5172 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}))
414403imaeq2d 5501 . . . . . . . . . . . 12 (𝑗 = (𝑦 + 1) → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))
415414xpeq1d 5172 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))
416413, 415uneq12d 3801 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))
417416oveq2d 6706 . . . . . . . . 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 3592 . . . . . . . 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 2701 . . . . . . 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 481 . . . . . 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 2695 . . . . 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 849 . . . 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 4777 . . 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 2688 . 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 4962 . . . . . . 7 ⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩ ∈ V
426425, 22op1std 7220 . . . . . 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 7221 . . . . . 6 (𝑡 = ⟨⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩, (2nd𝑇)⟩ → (2nd𝑡) = (2nd𝑇))
428 breq2 4689 . . . . . . . . 9 ((2nd𝑡) = (2nd𝑇) → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
429428ifbid 4141 . . . . . . . 8 ((2nd𝑡) = (2nd𝑇) → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
430429csbeq1d 3573 . . . . . . 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 6239 . . . . . . . . . 10 (1st ‘(1st𝑇)) ∈ V
432431, 79op1std 7220 . . . . . . . . 9 ((1st𝑡) = ⟨(1st ‘(1st𝑇)), ((2nd ‘(1st𝑇)) ∘ ({⟨(2nd𝑇), ((2nd𝑇) + 1)⟩, ⟨((2nd𝑇) + 1), (2nd𝑇)⟩} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd𝑇), ((2nd𝑇) + 1)}))))⟩ → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
433431, 79op2ndd 7221 . . . . . . . . 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 5496 . . . . . . . . . . . 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 5172 . . . . . . . . . . 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 5496 . . . . . . . . . . . 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 5172 . . . . . . . . . . 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 3801 . . . . . . . . . 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 6709 . . . . . . . . 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 694 . . . . . . . 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 4025 . . . . . . 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 2707 . . . . . 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 694 . . . . 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 4778 . . . 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 2661 . . 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 3399 . 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 699 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 383   = wceq 1523   ∈ wcel 2030  {cab 2637   ≠ wne 2823  {crab 2945  Vcvv 3231  ⦋csb 3566   ∖ cdif 3604   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  ifcif 4119  {csn 4210  {cpr 4212  ⟨cop 4216   class class class wbr 4685   ↦ cmpt 4762   I cid 5052   × cxp 5141  ran crn 5144   ↾ cres 5145   “ cima 5146   ∘ ccom 5147   Fn wfn 5921  ⟶wf 5922  –onto→wfo 5924  –1-1-onto→wf1o 5925  ‘cfv 5926  (class class class)co 6690   ∘𝑓 cof 6937  1st c1st 7208  2nd c2nd 7209   ↑𝑚 cmap 7899  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   < clt 10112   ≤ cle 10113   − cmin 10304  ℕcn 11058  ℕ0cn0 11330  ℤcz 11415  ℤ≥cuz 11725  ...cfz 12364  ..^cfzo 12504 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365 This theorem is referenced by:  poimirlem22  33561
 Copyright terms: Public domain W3C validator