Proof of Theorem poimirlem15
Step | Hyp | Ref
| Expression |
1 | | poimirlem22.2 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
2 | | elrabi 3596 |
. . . . . . 7
⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
3 | | poimirlem22.s |
. . . . . . 7
⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
4 | 2, 3 | eleq2s 2856 |
. . . . . 6
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
5 | 1, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
6 | | xp1st 7793 |
. . . . 5
⊢ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
7 | | xp1st 7793 |
. . . . 5
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
8 | 5, 6, 7 | 3syl 18 |
. . . 4
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
9 | | xp2nd 7794 |
. . . . . . . 8
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
10 | 5, 6, 9 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
11 | | fvex 6730 |
. . . . . . . 8
⊢
(2nd ‘(1st ‘𝑇)) ∈ V |
12 | | f1oeq1 6649 |
. . . . . . . 8
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
13 | 11, 12 | elab 3587 |
. . . . . . 7
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
14 | 10, 13 | sylib 221 |
. . . . . 6
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
15 | | poimirlem15.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2nd
‘𝑇) ∈
(1...(𝑁 −
1))) |
16 | | elfznn 13141 |
. . . . . . . . . . . . 13
⊢
((2nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑇) ∈
ℕ) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2nd
‘𝑇) ∈
ℕ) |
18 | 17 | nnred 11845 |
. . . . . . . . . . 11
⊢ (𝜑 → (2nd
‘𝑇) ∈
ℝ) |
19 | 18 | ltp1d 11762 |
. . . . . . . . . . 11
⊢ (𝜑 → (2nd
‘𝑇) <
((2nd ‘𝑇)
+ 1)) |
20 | 18, 19 | ltned 10968 |
. . . . . . . . . 10
⊢ (𝜑 → (2nd
‘𝑇) ≠
((2nd ‘𝑇)
+ 1)) |
21 | 20 | necomd 2996 |
. . . . . . . . . 10
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ≠
(2nd ‘𝑇)) |
22 | | fvex 6730 |
. . . . . . . . . . 11
⊢
(2nd ‘𝑇) ∈ V |
23 | | ovex 7246 |
. . . . . . . . . . 11
⊢
((2nd ‘𝑇) + 1) ∈ V |
24 | | f1oprg 6705 |
. . . . . . . . . . 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 ‘𝑇)})) |
25 | 22, 23, 23, 22, 24 | mp4an 693 |
. . . . . . . . . 10
⊢
(((2nd ‘𝑇) ≠ ((2nd ‘𝑇) + 1) ∧ ((2nd
‘𝑇) + 1) ≠
(2nd ‘𝑇))
→ {〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–1-1-onto→{((2nd ‘𝑇) + 1), (2nd ‘𝑇)}) |
26 | 20, 21, 25 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{((2nd ‘𝑇) + 1), (2nd ‘𝑇)}) |
27 | | prcom 4648 |
. . . . . . . . . 10
⊢
{((2nd ‘𝑇) + 1), (2nd ‘𝑇)} = {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)} |
28 | | f1oeq3 6651 |
. . . . . . . . . 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)})) |
29 | 27, 28 | ax-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)}) |
30 | 26, 29 | sylib 221 |
. . . . . . . 8
⊢ (𝜑 → {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}:{(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}–1-1-onto→{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) |
31 | | f1oi 6698 |
. . . . . . . 8
⊢ ( I
↾ ((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})):((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})–1-1-onto→((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) |
32 | | disjdif 4386 |
. . . . . . . . 9
⊢
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) =
∅ |
33 | | f1oun 6680 |
. . . . . . . . 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)}))) |
34 | 32, 32, 33 | mpanr12 705 |
. . . . . . . 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)}))) |
35 | 30, 31, 34 | sylancl 589 |
. . . . . . 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
⊢ (𝜑 → 𝑁 ∈ ℕ) |
37 | 36 | nncnd 11846 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℂ) |
38 | | npcan1 11257 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
40 | 36 | nnzd 12281 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℤ) |
41 | | peano2zm 12220 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
43 | | uzid 12453 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
44 | | peano2uz 12497 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
45 | 42, 43, 44 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
46 | 39, 45 | eqeltrrd 2839 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
47 | | fzss2 13152 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
49 | 48, 15 | sseldd 3902 |
. . . . . . . . . 10
⊢ (𝜑 → (2nd
‘𝑇) ∈ (1...𝑁)) |
50 | 17 | peano2nnd 11847 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ∈
ℕ) |
51 | 42 | zred 12282 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
52 | 36 | nnred 11845 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℝ) |
53 | | elfzle2 13116 |
. . . . . . . . . . . . . 14
⊢
((2nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑇) ≤ (𝑁 − 1)) |
54 | 15, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2nd
‘𝑇) ≤ (𝑁 − 1)) |
55 | 52 | ltm1d 11764 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 1) < 𝑁) |
56 | 18, 51, 52, 54, 55 | lelttrd 10990 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2nd
‘𝑇) < 𝑁) |
57 | 17 | nnzd 12281 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2nd
‘𝑇) ∈
ℤ) |
58 | | zltp1le 12227 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘𝑇) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((2nd
‘𝑇) < 𝑁 ↔ ((2nd
‘𝑇) + 1) ≤ 𝑁)) |
59 | 57, 40, 58 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2nd
‘𝑇) < 𝑁 ↔ ((2nd
‘𝑇) + 1) ≤ 𝑁)) |
60 | 56, 59 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ≤ 𝑁) |
61 | | fznn 13180 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ →
(((2nd ‘𝑇)
+ 1) ∈ (1...𝑁) ↔
(((2nd ‘𝑇)
+ 1) ∈ ℕ ∧ ((2nd ‘𝑇) + 1) ≤ 𝑁))) |
62 | 40, 61 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2nd
‘𝑇) + 1) ∈
(1...𝑁) ↔
(((2nd ‘𝑇)
+ 1) ∈ ℕ ∧ ((2nd ‘𝑇) + 1) ≤ 𝑁))) |
63 | 50, 60, 62 | mpbir2and 713 |
. . . . . . . . . 10
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ∈
(1...𝑁)) |
64 | | prssi 4734 |
. . . . . . . . . 10
⊢
(((2nd ‘𝑇) ∈ (1...𝑁) ∧ ((2nd ‘𝑇) + 1) ∈ (1...𝑁)) → {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ⊆
(1...𝑁)) |
65 | 49, 63, 64 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ⊆
(1...𝑁)) |
66 | | undif 4396 |
. . . . . . . . 9
⊢
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ⊆ (1...𝑁) ↔ ({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)})) =
(1...𝑁)) |
67 | 65, 66 | sylib 221 |
. . . . . . . 8
⊢ (𝜑 → ({(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ∪
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) = (1...𝑁)) |
68 | | f1oeq23 6652 |
. . . . . . . 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...𝑁))) |
69 | 67, 67, 68 | syl2anc 587 |
. . . . . . 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...𝑁))) |
70 | 35, 69 | mpbid 235 |
. . . . . 6
⊢ (𝜑 → ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))):(1...𝑁)–1-1-onto→(1...𝑁)) |
71 | | f1oco 6683 |
. . . . . 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...𝑁)) |
72 | 14, 70, 71 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))):(1...𝑁)–1-1-onto→(1...𝑁)) |
73 | | prex 5325 |
. . . . . . . 8
⊢
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∈ V |
74 | | ovex 7246 |
. . . . . . . . 9
⊢
(1...𝑁) ∈
V |
75 | | difexg 5220 |
. . . . . . . . 9
⊢
((1...𝑁) ∈ V
→ ((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) ∈ V) |
76 | | resiexg 7692 |
. . . . . . . . 9
⊢
(((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) ∈ V → ( I ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) ∈
V) |
77 | 74, 75, 76 | mp2b 10 |
. . . . . . . 8
⊢ ( I
↾ ((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) ∈ V |
78 | 73, 77 | unex 7531 |
. . . . . . 7
⊢
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))) ∈
V |
79 | 11, 78 | coex 7708 |
. . . . . 6
⊢
((2nd ‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))) ∈ V |
80 | | f1oeq1 6649 |
. . . . . 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...𝑁))) |
81 | 79, 80 | elab 3587 |
. . . . 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...𝑁)) |
82 | 72, 81 | sylibr 237 |
. . . 4
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))) ∈ {𝑓 ∣
𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
83 | | opelxpi 5588 |
. . . 4
⊢
(((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (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..^𝐾)
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
84 | 8, 82, 83 | syl2anc 587 |
. . 3
⊢ (𝜑 → 〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉
∈ (((0..^𝐾)
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
85 | | fz1ssfz0 13208 |
. . . . 5
⊢
(1...𝑁) ⊆
(0...𝑁) |
86 | 48, 85 | sstrdi 3913 |
. . . 4
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (0...𝑁)) |
87 | 86, 15 | sseldd 3902 |
. . 3
⊢ (𝜑 → (2nd
‘𝑇) ∈ (0...𝑁)) |
88 | | opelxpi 5588 |
. . 3
⊢
((〈(1st ‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉
∈ (((0..^𝐾)
↑m (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..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
89 | 84, 87, 88 | syl2anc 587 |
. 2
⊢ (𝜑 →
〈〈(1st ‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉,
(2nd ‘𝑇)〉 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
90 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
91 | 90 | breq2d 5065 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) |
92 | 91 | ifbid 4462 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) |
93 | 92 | csbeq1d 3815 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
94 | | 2fveq3 6722 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
95 | | 2fveq3 6722 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) |
96 | 95 | imaeq1d 5928 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑗))) |
97 | 96 | xpeq1d 5580 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1})) |
98 | 95 | imaeq1d 5928 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
99 | 98 | xpeq1d 5580 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
100 | 97, 99 | uneq12d 4078 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
101 | 94, 100 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
102 | 101 | csbeq2dv 3818 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
103 | 93, 102 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
104 | 103 | mpteq2dv 5151 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
105 | 104 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
106 | 105, 3 | elrab2 3605 |
. . . . 5
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
107 | 106 | simprbi 500 |
. . . 4
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
108 | 1, 107 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
109 | | imaco 6115 |
. . . . . . . . . 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...𝑦))) |
110 | | f1ofn 6662 |
. . . . . . . . . . . . . . . 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)}) |
111 | 26, 110 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} Fn {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}) |
112 | 111 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} Fn {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}) |
113 | | incom 4115 |
. . . . . . . . . . . . . . 15
⊢
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∩ (1...𝑦)) = ((1...𝑦) ∩ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) |
114 | | elfznn0 13205 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ0) |
115 | 114 | nn0red 12151 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ) |
116 | | ltnle 10912 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℝ ∧
(2nd ‘𝑇)
∈ ℝ) → (𝑦
< (2nd ‘𝑇) ↔ ¬ (2nd ‘𝑇) ≤ 𝑦)) |
117 | 115, 18, 116 | syl2anr 600 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2nd ‘𝑇) ↔ ¬ (2nd
‘𝑇) ≤ 𝑦)) |
118 | 117 | biimpa 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ¬ (2nd
‘𝑇) ≤ 𝑦) |
119 | | elfzle2 13116 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘𝑇) ∈ (1...𝑦) → (2nd ‘𝑇) ≤ 𝑦) |
120 | 118, 119 | nsyl 142 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ¬ (2nd
‘𝑇) ∈ (1...𝑦)) |
121 | | disjsn 4627 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1...𝑦) ∩
{(2nd ‘𝑇)}) = ∅ ↔ ¬ (2nd
‘𝑇) ∈ (1...𝑦)) |
122 | 120, 121 | sylibr 237 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ((1...𝑦) ∩ {(2nd
‘𝑇)}) =
∅) |
123 | 115 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → 𝑦 ∈ ℝ) |
124 | 18 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (2nd
‘𝑇) ∈
ℝ) |
125 | 50 | nnred 11845 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ∈
ℝ) |
126 | 125 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ((2nd
‘𝑇) + 1) ∈
ℝ) |
127 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → 𝑦 < (2nd ‘𝑇)) |
128 | 19 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (2nd
‘𝑇) <
((2nd ‘𝑇)
+ 1)) |
129 | 123, 124,
126, 127, 128 | lttrd 10993 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → 𝑦 < ((2nd ‘𝑇) + 1)) |
130 | | ltnle 10912 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℝ ∧
((2nd ‘𝑇)
+ 1) ∈ ℝ) → (𝑦 < ((2nd ‘𝑇) + 1) ↔ ¬
((2nd ‘𝑇)
+ 1) ≤ 𝑦)) |
131 | 115, 125,
130 | syl2anr 600 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < ((2nd ‘𝑇) + 1) ↔ ¬
((2nd ‘𝑇)
+ 1) ≤ 𝑦)) |
132 | 131 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (𝑦 < ((2nd ‘𝑇) + 1) ↔ ¬
((2nd ‘𝑇)
+ 1) ≤ 𝑦)) |
133 | 129, 132 | mpbid 235 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ¬ ((2nd
‘𝑇) + 1) ≤ 𝑦) |
134 | | elfzle2 13116 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((2nd ‘𝑇) + 1) ∈ (1...𝑦) → ((2nd ‘𝑇) + 1) ≤ 𝑦) |
135 | 133, 134 | nsyl 142 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ¬ ((2nd
‘𝑇) + 1) ∈
(1...𝑦)) |
136 | | disjsn 4627 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1...𝑦) ∩
{((2nd ‘𝑇)
+ 1)}) = ∅ ↔ ¬ ((2nd ‘𝑇) + 1) ∈ (1...𝑦)) |
137 | 135, 136 | sylibr 237 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ((1...𝑦) ∩ {((2nd
‘𝑇) + 1)}) =
∅) |
138 | 122, 137 | uneq12d 4078 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (((1...𝑦) ∩ {(2nd
‘𝑇)}) ∪
((1...𝑦) ∩
{((2nd ‘𝑇)
+ 1)})) = (∅ ∪ ∅)) |
139 | | df-pr 4544 |
. . . . . . . . . . . . . . . . . 18
⊢
{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} = ({(2nd ‘𝑇)} ∪ {((2nd
‘𝑇) +
1)}) |
140 | 139 | ineq2i 4124 |
. . . . . . . . . . . . . . . . 17
⊢
((1...𝑦) ∩
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) = ((1...𝑦) ∩
({(2nd ‘𝑇)} ∪ {((2nd ‘𝑇) + 1)})) |
141 | | indi 4188 |
. . . . . . . . . . . . . . . . 17
⊢
((1...𝑦) ∩
({(2nd ‘𝑇)} ∪ {((2nd ‘𝑇) + 1)})) = (((1...𝑦) ∩ {(2nd
‘𝑇)}) ∪
((1...𝑦) ∩
{((2nd ‘𝑇)
+ 1)})) |
142 | 140, 141 | eqtr2i 2766 |
. . . . . . . . . . . . . . . 16
⊢
(((1...𝑦) ∩
{(2nd ‘𝑇)}) ∪ ((1...𝑦) ∩ {((2nd ‘𝑇) + 1)})) = ((1...𝑦) ∩ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}) |
143 | | un0 4305 |
. . . . . . . . . . . . . . . 16
⊢ (∅
∪ ∅) = ∅ |
144 | 138, 142,
143 | 3eqtr3g 2801 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ((1...𝑦) ∩ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}) =
∅) |
145 | 113, 144 | syl5eq 2790 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ({(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ∩
(1...𝑦)) =
∅) |
146 | | fnimadisj 6510 |
. . . . . . . . . . . . . 14
⊢
(({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} Fn {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∧ ({(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ∩
(1...𝑦)) = ∅) →
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ (1...𝑦)) = ∅) |
147 | 112, 145,
146 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) →
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ (1...𝑦)) = ∅) |
148 | 39 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁) |
149 | | elfzuz3 13109 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑦)) |
150 | | peano2uz 12497 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 − 1) ∈
(ℤ≥‘𝑦) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘𝑦)) |
151 | 149, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘𝑦)) |
152 | 151 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘𝑦)) |
153 | 148, 152 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ≥‘𝑦)) |
154 | | fzss2 13152 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘𝑦) → (1...𝑦) ⊆ (1...𝑁)) |
155 | | reldisj 4366 |
. . . . . . . . . . . . . . . . 17
⊢
((1...𝑦) ⊆
(1...𝑁) → (((1...𝑦) ∩ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}) = ∅
↔ (1...𝑦) ⊆
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))) |
156 | 153, 154,
155 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((1...𝑦) ∩ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}) = ∅
↔ (1...𝑦) ⊆
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))) |
157 | 156 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (((1...𝑦) ∩ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}) = ∅
↔ (1...𝑦) ⊆
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))) |
158 | 144, 157 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (1...𝑦) ⊆ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)})) |
159 | | resiima 5944 |
. . . . . . . . . . . . . 14
⊢
((1...𝑦) ⊆
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) → (( I ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) “ (1...𝑦)) = (1...𝑦)) |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ (1...𝑦)) =
(1...𝑦)) |
161 | 147, 160 | uneq12d 4078 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) →
(({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ (1...𝑦)) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) “ (1...𝑦))) = (∅ ∪ (1...𝑦))) |
162 | | imaundir 6014 |
. . . . . . . . . . . 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...𝑦))) |
163 | | uncom 4067 |
. . . . . . . . . . . . 13
⊢ (∅
∪ (1...𝑦)) =
((1...𝑦) ∪
∅) |
164 | | un0 4305 |
. . . . . . . . . . . . 13
⊢
((1...𝑦) ∪
∅) = (1...𝑦) |
165 | 163, 164 | eqtr2i 2766 |
. . . . . . . . . . . 12
⊢
(1...𝑦) = (∅
∪ (1...𝑦)) |
166 | 161, 162,
165 | 3eqtr4g 2803 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) →
(({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))) “
(1...𝑦)) = (1...𝑦)) |
167 | 166 | imaeq2d 5929 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ((2nd
‘(1st ‘𝑇)) “ (({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))) “ (1...𝑦)))
= ((2nd ‘(1st ‘𝑇)) “ (1...𝑦))) |
168 | 109, 167 | syl5eq 2790 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))) “ (1...𝑦))
= ((2nd ‘(1st ‘𝑇)) “ (1...𝑦))) |
169 | 168 | xpeq1d 5580 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ((((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))) “ (1...𝑦))
× {1}) = (((2nd ‘(1st ‘𝑇)) “ (1...𝑦)) ×
{1})) |
170 | | imaco 6115 |
. . . . . . . . . 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)...𝑁))) |
171 | | imaundir 6014 |
. . . . . . . . . . . . 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)...𝑁))) |
172 | | imassrn 5940 |
. . . . . . . . . . . . . . . . 17
⊢
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ ((𝑦 + 1)...𝑁)) ⊆ ran {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} |
173 | 172 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) →
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ ((𝑦 + 1)...𝑁)) ⊆ ran {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) |
174 | | fnima 6508 |
. . . . . . . . . . . . . . . . . . 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 ‘𝑇)〉}) |
175 | 26, 110, 174 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} “
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) = ran {〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}) |
176 | 175 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) →
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}) = ran
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}) |
177 | | elfzelz 13112 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ) |
178 | | zltp1le 12227 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℤ ∧
(2nd ‘𝑇)
∈ ℤ) → (𝑦
< (2nd ‘𝑇) ↔ (𝑦 + 1) ≤ (2nd ‘𝑇))) |
179 | 177, 57, 178 | syl2anr 600 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2nd ‘𝑇) ↔ (𝑦 + 1) ≤ (2nd ‘𝑇))) |
180 | 179 | biimpa 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (𝑦 + 1) ≤ (2nd ‘𝑇)) |
181 | 18, 52, 56 | ltled 10980 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (2nd
‘𝑇) ≤ 𝑁) |
182 | 181 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (2nd
‘𝑇) ≤ 𝑁) |
183 | 57 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2nd
‘𝑇) ∈
ℤ) |
184 | | nn0p1nn 12129 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ℕ0
→ (𝑦 + 1) ∈
ℕ) |
185 | 114, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℕ) |
186 | 185 | nnzd 12281 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℤ) |
187 | 186 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ ℤ) |
188 | 40 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℤ) |
189 | | elfz 13101 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((2nd ‘𝑇) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((2nd
‘𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2nd ‘𝑇) ∧ (2nd
‘𝑇) ≤ 𝑁))) |
190 | 183, 187,
188, 189 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2nd ‘𝑇) ∧ (2nd
‘𝑇) ≤ 𝑁))) |
191 | 190 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ((2nd
‘𝑇) ∈ ((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ (2nd ‘𝑇) ∧ (2nd
‘𝑇) ≤ 𝑁))) |
192 | 180, 182,
191 | mpbir2and 713 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (2nd
‘𝑇) ∈ ((𝑦 + 1)...𝑁)) |
193 | | 1red 10834 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → 1 ∈
ℝ) |
194 | | ltle 10921 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℝ ∧
(2nd ‘𝑇)
∈ ℝ) → (𝑦
< (2nd ‘𝑇) → 𝑦 ≤ (2nd ‘𝑇))) |
195 | 115, 18, 194 | syl2anr 600 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 < (2nd ‘𝑇) → 𝑦 ≤ (2nd ‘𝑇))) |
196 | 195 | imp 410 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → 𝑦 ≤ (2nd ‘𝑇)) |
197 | 123, 124,
193, 196 | leadd1dd 11446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (𝑦 + 1) ≤ ((2nd ‘𝑇) + 1)) |
198 | 60 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ((2nd
‘𝑇) + 1) ≤ 𝑁) |
199 | 57 | peano2zd 12285 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ∈
ℤ) |
200 | 199 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘𝑇) + 1) ∈
ℤ) |
201 | | elfz 13101 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((2nd ‘𝑇) + 1) ∈ ℤ ∧ (𝑦 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(((2nd ‘𝑇)
+ 1) ∈ ((𝑦 +
1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2nd
‘𝑇) + 1) ∧
((2nd ‘𝑇)
+ 1) ≤ 𝑁))) |
202 | 200, 187,
188, 201 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2nd
‘𝑇) + 1) ∈
((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2nd ‘𝑇) + 1) ∧ ((2nd
‘𝑇) + 1) ≤ 𝑁))) |
203 | 202 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (((2nd
‘𝑇) + 1) ∈
((𝑦 + 1)...𝑁) ↔ ((𝑦 + 1) ≤ ((2nd ‘𝑇) + 1) ∧ ((2nd
‘𝑇) + 1) ≤ 𝑁))) |
204 | 197, 198,
203 | mpbir2and 713 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ((2nd
‘𝑇) + 1) ∈
((𝑦 + 1)...𝑁)) |
205 | | prssi 4734 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((2nd ‘𝑇) ∈ ((𝑦 + 1)...𝑁) ∧ ((2nd ‘𝑇) + 1) ∈ ((𝑦 + 1)...𝑁)) → {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁)) |
206 | 192, 204,
205 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ⊆
((𝑦 + 1)...𝑁)) |
207 | | imass2 5970 |
. . . . . . . . . . . . . . . . . 18
⊢
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁) → ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} “
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) ⊆ ({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ ((𝑦 + 1)...𝑁))) |
208 | 206, 207 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) →
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}) ⊆
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ ((𝑦 + 1)...𝑁))) |
209 | 176, 208 | eqsstrrd 3940 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ran
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ⊆ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} “ ((𝑦 + 1)...𝑁))) |
210 | 173, 209 | eqssd 3918 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) →
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ ((𝑦 + 1)...𝑁)) = ran {〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}) |
211 | | f1ofo 6668 |
. . . . . . . . . . . . . . . . . 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
‘𝑇)}) |
212 | | forn 6636 |
. . . . . . . . . . . . . . . . . 18
⊢
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}–onto→{((2nd ‘𝑇) + 1), (2nd ‘𝑇)} → ran
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} = {((2nd ‘𝑇) + 1), (2nd
‘𝑇)}) |
213 | 26, 211, 212 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ran {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} = {((2nd
‘𝑇) + 1),
(2nd ‘𝑇)}) |
214 | 213, 27 | eqtrdi 2794 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ran {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} = {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}) |
215 | 214 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ran
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} = {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) |
216 | 210, 215 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) →
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ ((𝑦 + 1)...𝑁)) = {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) |
217 | | undif 4396 |
. . . . . . . . . . . . . . . . 17
⊢
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ⊆ ((𝑦 + 1)...𝑁) ↔ ({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = ((𝑦 + 1)...𝑁)) |
218 | 206, 217 | sylib 221 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ({(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ∪
(((𝑦 + 1)...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)})) = ((𝑦 + 1)...𝑁)) |
219 | 218 | imaeq2d 5929 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ ({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = (( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ ((𝑦 +
1)...𝑁))) |
220 | | fnresi 6506 |
. . . . . . . . . . . . . . . . . . 19
⊢ ( I
↾ ((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) Fn ((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) |
221 | | disjdifr 4387 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) ∩ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = ∅ |
222 | | fnimadisj 6510 |
. . . . . . . . . . . . . . . . . . 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)}) = ∅) |
223 | 220, 221,
222 | mp2an 692 |
. . . . . . . . . . . . . . . . . 18
⊢ (( I
↾ ((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = ∅ |
224 | 223 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = ∅) |
225 | | nnuz 12477 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℕ =
(ℤ≥‘1) |
226 | 185, 225 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈
(ℤ≥‘1)) |
227 | | fzss1 13151 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 + 1) ∈
(ℤ≥‘1) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁)) |
228 | 226, 227 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1)...𝑁) ⊆ (1...𝑁)) |
229 | 228 | ssdifd 4055 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (((𝑦 + 1)...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)})) |
230 | | resiima 5944 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑦 + 1)...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ⊆ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}) → ((
I ↾ ((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ (((𝑦 +
1)...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) = (((𝑦 + 1)...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)})) |
231 | 229, 230 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)})) “
(((𝑦 + 1)...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)})) =
(((𝑦 + 1)...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)})) |
232 | 231 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ (((𝑦 +
1)...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) = (((𝑦 + 1)...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)})) |
233 | 224, 232 | uneq12d 4078 |
. . . . . . . . . . . . . . . 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)}))) |
234 | | imaundi 6013 |
. . . . . . . . . . . . . . . 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)}))) |
235 | | uncom 4067 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
∪ (((𝑦 + 1)...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)})) =
((((𝑦 + 1)...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}) ∪
∅) |
236 | | un0 4305 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 + 1)...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∪ ∅) =
(((𝑦 + 1)...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}) |
237 | 235, 236 | eqtr2i 2766 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 + 1)...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = (∅ ∪
(((𝑦 + 1)...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)})) |
238 | 233, 234,
237 | 3eqtr4g 2803 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ ({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ (((𝑦 + 1)...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = (((𝑦 + 1)...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) |
239 | 219, 238 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ ((𝑦 +
1)...𝑁)) = (((𝑦 + 1)...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) |
240 | 216, 239 | uneq12d 4078 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) →
(({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ ((𝑦 + 1)...𝑁)) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)})) “
((𝑦 + 1)...𝑁))) = ({(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ∪
(((𝑦 + 1)...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}))) |
241 | 171, 240 | syl5eq 2790 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) →
(({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))) “
((𝑦 + 1)...𝑁)) = ({(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ∪
(((𝑦 + 1)...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}))) |
242 | 241, 218 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) →
(({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))) “
((𝑦 + 1)...𝑁)) = ((𝑦 + 1)...𝑁)) |
243 | 242 | imaeq2d 5929 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ((2nd
‘(1st ‘𝑇)) “ (({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))) “ ((𝑦 +
1)...𝑁))) =
((2nd ‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) |
244 | 170, 243 | syl5eq 2790 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → (((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))) “ ((𝑦 +
1)...𝑁)) = ((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁))) |
245 | 244 | xpeq1d 5580 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ((((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))) “ ((𝑦 +
1)...𝑁)) × {0}) =
(((2nd ‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) |
246 | 169, 245 | uneq12d 4078 |
. . . . . . 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}))) |
247 | 246 | oveq2d 7229 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) → ((1st
‘(1st ‘𝑇)) ∘f + (((((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 ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) |
248 | | iftrue 4445 |
. . . . . . . . 9
⊢ (𝑦 < (2nd
‘𝑇) → if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) = 𝑦) |
249 | 248 | csbeq1d 3815 |
. . . . . . . 8
⊢ (𝑦 < (2nd
‘𝑇) →
⦋if(𝑦 <
(2nd ‘𝑇),
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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 ‘𝑇)) ∘f + (((((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})))) |
250 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
251 | | oveq2 7221 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑦 → (1...𝑗) = (1...𝑦)) |
252 | 251 | imaeq2d 5929 |
. . . . . . . . . . . 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...𝑦))) |
253 | 252 | xpeq1d 5580 |
. . . . . . . . . . 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})) |
254 | | oveq1 7220 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑦 → (𝑗 + 1) = (𝑦 + 1)) |
255 | 254 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑦 → ((𝑗 + 1)...𝑁) = ((𝑦 + 1)...𝑁)) |
256 | 255 | imaeq2d 5929 |
. . . . . . . . . . . 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)...𝑁))) |
257 | 256 | xpeq1d 5580 |
. . . . . . . . . . 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})) |
258 | 253, 257 | uneq12d 4078 |
. . . . . . . . . 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}))) |
259 | 258 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝑗 = 𝑦 → ((1st
‘(1st ‘𝑇)) ∘f + (((((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 ‘𝑇)) ∘f + (((((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})))) |
260 | 250, 259 | csbie 3847 |
. . . . . . . 8
⊢
⦋𝑦 /
𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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 ‘𝑇)) ∘f + (((((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}))) |
261 | 249, 260 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑦 < (2nd
‘𝑇) →
⦋if(𝑦 <
(2nd ‘𝑇),
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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 ‘𝑇)) ∘f + (((((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})))) |
262 | 261 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) →
⦋if(𝑦 <
(2nd ‘𝑇),
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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 ‘𝑇)) ∘f + (((((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})))) |
263 | 248 | csbeq1d 3815 |
. . . . . . . 8
⊢ (𝑦 < (2nd
‘𝑇) →
⦋if(𝑦 <
(2nd ‘𝑇),
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
264 | 251 | imaeq2d 5929 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑦 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑦))) |
265 | 264 | xpeq1d 5580 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑦 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1})) |
266 | 255 | imaeq2d 5929 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑦 → ((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑦 + 1)...𝑁))) |
267 | 266 | xpeq1d 5580 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑦 → (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})) |
268 | 265, 267 | uneq12d 4078 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑦 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))) |
269 | 268 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝑗 = 𝑦 → ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) |
270 | 250, 269 | csbie 3847 |
. . . . . . . 8
⊢
⦋𝑦 /
𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0}))) |
271 | 263, 270 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑦 < (2nd
‘𝑇) →
⦋if(𝑦 <
(2nd ‘𝑇),
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) |
272 | 271 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) →
⦋if(𝑦 <
(2nd ‘𝑇),
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑦 + 1)...𝑁)) × {0})))) |
273 | 247, 262,
272 | 3eqtr4d 2787 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < (2nd ‘𝑇)) →
⦋if(𝑦 <
(2nd ‘𝑇),
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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 ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
274 | | lenlt 10911 |
. . . . . . . . . 10
⊢
(((2nd ‘𝑇) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((2nd
‘𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd ‘𝑇))) |
275 | 18, 115, 274 | syl2an 599 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd ‘𝑇))) |
276 | 275 | biimpar 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2nd ‘𝑇)) → (2nd
‘𝑇) ≤ 𝑦) |
277 | | imaco 6115 |
. . . . . . . . . . 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)))) |
278 | | imaundir 6014 |
. . . . . . . . . . . . . 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)))) |
279 | | imassrn 5940 |
. . . . . . . . . . . . . . . . . 18
⊢
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ (1...(𝑦 + 1))) ⊆ ran {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} |
280 | 279 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} “ (1...(𝑦 + 1))) ⊆ ran
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}) |
281 | 175 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} “
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) = ran {〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}) |
282 | 17 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (2nd
‘𝑇) ∈
ℕ) |
283 | 18 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (2nd
‘𝑇) ∈
ℝ) |
284 | 115 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → 𝑦 ∈ ℝ) |
285 | 185 | nnred 11845 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℝ) |
286 | 285 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (𝑦 + 1) ∈ ℝ) |
287 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (2nd
‘𝑇) ≤ 𝑦) |
288 | 115 | lep1d 11763 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑦 + 1)) |
289 | 288 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → 𝑦 ≤ (𝑦 + 1)) |
290 | 283, 284,
286, 287, 289 | letrd 10989 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (2nd
‘𝑇) ≤ (𝑦 + 1)) |
291 | | fznn 13180 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 + 1) ∈ ℤ →
((2nd ‘𝑇)
∈ (1...(𝑦 + 1)) ↔
((2nd ‘𝑇)
∈ ℕ ∧ (2nd ‘𝑇) ≤ (𝑦 + 1)))) |
292 | 186, 291 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd
‘𝑇) ∈
(1...(𝑦 + 1)) ↔
((2nd ‘𝑇)
∈ ℕ ∧ (2nd ‘𝑇) ≤ (𝑦 + 1)))) |
293 | 292 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ((2nd
‘𝑇) ∈
(1...(𝑦 + 1)) ↔
((2nd ‘𝑇)
∈ ℕ ∧ (2nd ‘𝑇) ≤ (𝑦 + 1)))) |
294 | 282, 290,
293 | mpbir2and 713 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (2nd
‘𝑇) ∈
(1...(𝑦 +
1))) |
295 | 50 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ((2nd
‘𝑇) + 1) ∈
ℕ) |
296 | | 1red 10834 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → 1 ∈
ℝ) |
297 | 283, 284,
296, 287 | leadd1dd 11446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ((2nd
‘𝑇) + 1) ≤ (𝑦 + 1)) |
298 | | fznn 13180 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 + 1) ∈ ℤ →
(((2nd ‘𝑇)
+ 1) ∈ (1...(𝑦 + 1))
↔ (((2nd ‘𝑇) + 1) ∈ ℕ ∧ ((2nd
‘𝑇) + 1) ≤ (𝑦 + 1)))) |
299 | 186, 298 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (((2nd
‘𝑇) + 1) ∈
(1...(𝑦 + 1)) ↔
(((2nd ‘𝑇)
+ 1) ∈ ℕ ∧ ((2nd ‘𝑇) + 1) ≤ (𝑦 + 1)))) |
300 | 299 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (((2nd
‘𝑇) + 1) ∈
(1...(𝑦 + 1)) ↔
(((2nd ‘𝑇)
+ 1) ∈ ℕ ∧ ((2nd ‘𝑇) + 1) ≤ (𝑦 + 1)))) |
301 | 295, 297,
300 | mpbir2and 713 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ((2nd
‘𝑇) + 1) ∈
(1...(𝑦 +
1))) |
302 | | prssi 4734 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((2nd ‘𝑇) ∈ (1...(𝑦 + 1)) ∧ ((2nd ‘𝑇) + 1) ∈ (1...(𝑦 + 1))) → {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ⊆
(1...(𝑦 +
1))) |
303 | 294, 301,
302 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ⊆
(1...(𝑦 +
1))) |
304 | | imass2 5970 |
. . . . . . . . . . . . . . . . . . 19
⊢
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ⊆ (1...(𝑦 + 1)) → ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} “
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) ⊆ ({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ (1...(𝑦 + 1)))) |
305 | 303, 304 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} “
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) ⊆ ({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ (1...(𝑦 + 1)))) |
306 | 281, 305 | eqsstrrd 3940 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ran
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ⊆ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} “ (1...(𝑦 + 1)))) |
307 | 280, 306 | eqssd 3918 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} “ (1...(𝑦 + 1))) = ran
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}) |
308 | 214 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ran
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} = {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) |
309 | 307, 308 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} “ (1...(𝑦 + 1))) = {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}) |
310 | | undif 4396 |
. . . . . . . . . . . . . . . . . 18
⊢
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ⊆ (1...(𝑦 + 1)) ↔ ({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)})) =
(1...(𝑦 +
1))) |
311 | 303, 310 | sylib 221 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ({(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ∪
((1...(𝑦 + 1)) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) = (1...(𝑦 +
1))) |
312 | 311 | imaeq2d 5929 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ ({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = (( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ (1...(𝑦 +
1)))) |
313 | 223 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = ∅) |
314 | | eluzp1p1 12466 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 − 1) ∈
(ℤ≥‘𝑦) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑦 + 1))) |
315 | 149, 314 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑦 + 1))) |
316 | 315 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑦 + 1))) |
317 | 148, 316 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ≥‘(𝑦 + 1))) |
318 | | fzss2 13152 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘(𝑦 + 1)) → (1...(𝑦 + 1)) ⊆ (1...𝑁)) |
319 | 317, 318 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...(𝑦 + 1)) ⊆ (1...𝑁)) |
320 | 319 | ssdifd 4055 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((1...(𝑦 + 1)) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}) ⊆
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) |
321 | 320 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ((1...(𝑦 + 1)) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}) ⊆
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) |
322 | | resiima 5944 |
. . . . . . . . . . . . . . . . . . 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)})) |
323 | 321, 322 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ ((1...(𝑦 +
1)) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = ((1...(𝑦 + 1)) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) |
324 | 313, 323 | uneq12d 4078 |
. . . . . . . . . . . . . . . . 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)}))) |
325 | | imaundi 6013 |
. . . . . . . . . . . . . . . . 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)}))) |
326 | | uncom 4067 |
. . . . . . . . . . . . . . . . . 18
⊢ (∅
∪ ((1...(𝑦 + 1))
∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = (((1...(𝑦 + 1)) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∪
∅) |
327 | | un0 4305 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1...(𝑦 + 1))
∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) ∪ ∅) = ((1...(𝑦 + 1)) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}) |
328 | 326, 327 | eqtr2i 2766 |
. . . . . . . . . . . . . . . . 17
⊢
((1...(𝑦 + 1))
∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = (∅ ∪ ((1...(𝑦 + 1)) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)})) |
329 | 324, 325,
328 | 3eqtr4g 2803 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ ({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...(𝑦 + 1)) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) = ((1...(𝑦 + 1)) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)})) |
330 | 312, 329 | eqtr3d 2779 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ (1...(𝑦 +
1))) = ((1...(𝑦 + 1))
∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) |
331 | 309, 330 | uneq12d 4078 |
. . . . . . . . . . . . . 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)}))) |
332 | 278, 331 | syl5eq 2790 |
. . . . . . . . . . . . 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)}))) |
333 | 332, 311 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) →
(({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))) “
(1...(𝑦 + 1))) =
(1...(𝑦 +
1))) |
334 | 333 | imaeq2d 5929 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ((2nd
‘(1st ‘𝑇)) “ (({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))) “ (1...(𝑦 +
1)))) = ((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1)))) |
335 | 277, 334 | syl5eq 2790 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))) “ (1...(𝑦 +
1))) = ((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1)))) |
336 | 335 | xpeq1d 5580 |
. . . . . . . . 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})) |
337 | | imaco 6115 |
. . . . . . . . . . 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)...𝑁))) |
338 | 111 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → {〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} Fn {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}) |
339 | | incom 4115 |
. . . . . . . . . . . . . . . 16
⊢
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∩ (((𝑦 + 1) + 1)...𝑁)) = ((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) |
340 | 125 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ((2nd
‘𝑇) + 1) ∈
ℝ) |
341 | 185 | peano2nnd 11847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℕ) |
342 | 341 | nnred 11845 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℝ) |
343 | 342 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ((𝑦 + 1) + 1) ∈ ℝ) |
344 | 19 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (2nd
‘𝑇) <
((2nd ‘𝑇)
+ 1)) |
345 | 115 | ltp1d 11762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 < (𝑦 + 1)) |
346 | 345 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → 𝑦 < (𝑦 + 1)) |
347 | 283, 284,
286, 287, 346 | lelttrd 10990 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (2nd
‘𝑇) < (𝑦 + 1)) |
348 | 283, 286,
296, 347 | ltadd1dd 11443 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ((2nd
‘𝑇) + 1) < ((𝑦 + 1) + 1)) |
349 | 283, 340,
343, 344, 348 | lttrd 10993 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (2nd
‘𝑇) < ((𝑦 + 1) + 1)) |
350 | | ltnle 10912 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((2nd ‘𝑇) ∈ ℝ ∧ ((𝑦 + 1) + 1) ∈ ℝ) →
((2nd ‘𝑇)
< ((𝑦 + 1) + 1) ↔
¬ ((𝑦 + 1) + 1) ≤
(2nd ‘𝑇))) |
351 | 18, 342, 350 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2nd
‘𝑇))) |
352 | 351 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ((2nd
‘𝑇) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ (2nd
‘𝑇))) |
353 | 349, 352 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ¬ ((𝑦 + 1) + 1) ≤ (2nd
‘𝑇)) |
354 | | elfzle1 13115 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2nd ‘𝑇) ∈ (((𝑦 + 1) + 1)...𝑁) → ((𝑦 + 1) + 1) ≤ (2nd ‘𝑇)) |
355 | 353, 354 | nsyl 142 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ¬ (2nd
‘𝑇) ∈ (((𝑦 + 1) + 1)...𝑁)) |
356 | | disjsn 4627 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑦 + 1) +
1)...𝑁) ∩
{(2nd ‘𝑇)}) = ∅ ↔ ¬ (2nd
‘𝑇) ∈ (((𝑦 + 1) + 1)...𝑁)) |
357 | 355, 356 | sylibr 237 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd ‘𝑇)}) = ∅) |
358 | | ltnle 10912 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((2nd ‘𝑇) + 1) ∈ ℝ ∧ ((𝑦 + 1) + 1) ∈ ℝ)
→ (((2nd ‘𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2nd ‘𝑇) + 1))) |
359 | 125, 342,
358 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2nd
‘𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2nd
‘𝑇) +
1))) |
360 | 359 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (((2nd
‘𝑇) + 1) < ((𝑦 + 1) + 1) ↔ ¬ ((𝑦 + 1) + 1) ≤ ((2nd
‘𝑇) +
1))) |
361 | 348, 360 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ¬ ((𝑦 + 1) + 1) ≤ ((2nd
‘𝑇) +
1)) |
362 | | elfzle1 13115 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((2nd ‘𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁) → ((𝑦 + 1) + 1) ≤ ((2nd ‘𝑇) + 1)) |
363 | 361, 362 | nsyl 142 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ¬ ((2nd
‘𝑇) + 1) ∈
(((𝑦 + 1) + 1)...𝑁)) |
364 | | disjsn 4627 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑦 + 1) +
1)...𝑁) ∩
{((2nd ‘𝑇)
+ 1)}) = ∅ ↔ ¬ ((2nd ‘𝑇) + 1) ∈ (((𝑦 + 1) + 1)...𝑁)) |
365 | 363, 364 | sylibr 237 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {((2nd ‘𝑇) + 1)}) =
∅) |
366 | 357, 365 | uneq12d 4078 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd ‘𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2nd ‘𝑇) + 1)})) = (∅ ∪
∅)) |
367 | 139 | ineq2i 4124 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = ((((𝑦 + 1) + 1)...𝑁) ∩ ({(2nd ‘𝑇)} ∪ {((2nd
‘𝑇) +
1)})) |
368 | | indi 4188 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 + 1) + 1)...𝑁) ∩ ({(2nd ‘𝑇)} ∪ {((2nd
‘𝑇) + 1)})) =
(((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd
‘𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2nd ‘𝑇) + 1)})) |
369 | 367, 368 | eqtr2i 2766 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑦 + 1) +
1)...𝑁) ∩
{(2nd ‘𝑇)}) ∪ ((((𝑦 + 1) + 1)...𝑁) ∩ {((2nd ‘𝑇) + 1)})) = ((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) |
370 | 366, 369,
143 | 3eqtr3g 2801 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) =
∅) |
371 | 339, 370 | syl5eq 2790 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ({(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ∩
(((𝑦 + 1) + 1)...𝑁)) = ∅) |
372 | | fnimadisj 6510 |
. . . . . . . . . . . . . . 15
⊢
(({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} Fn {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∧ ({(2nd
‘𝑇), ((2nd
‘𝑇) + 1)} ∩
(((𝑦 + 1) + 1)...𝑁)) = ∅) →
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ (((𝑦 + 1) + 1)...𝑁)) = ∅) |
373 | 338, 371,
372 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} “ (((𝑦 + 1) + 1)...𝑁)) = ∅) |
374 | 341, 225 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈
(ℤ≥‘1)) |
375 | | fzss1 13151 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 + 1) + 1) ∈
(ℤ≥‘1) → (((𝑦 + 1) + 1)...𝑁) ⊆ (1...𝑁)) |
376 | | reldisj 4366 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 + 1) + 1)...𝑁) ⊆ (1...𝑁) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = ∅ ↔
(((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}))) |
377 | 374, 375,
376 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = ∅ ↔
(((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}))) |
378 | 377 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (((((𝑦 + 1) + 1)...𝑁) ∩ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) = ∅ ↔
(((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}))) |
379 | 370, 378 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) |
380 | | resiima 5944 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 + 1) + 1)...𝑁) ⊆ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) → (( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ (((𝑦 + 1) +
1)...𝑁)) = (((𝑦 + 1) + 1)...𝑁)) |
381 | 379, 380 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) “ (((𝑦 + 1) +
1)...𝑁)) = (((𝑦 + 1) + 1)...𝑁)) |
382 | 373, 381 | uneq12d 4078 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) →
(({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} “ (((𝑦 + 1) + 1)...𝑁)) ∪ (( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)})) “
(((𝑦 + 1) + 1)...𝑁))) = (∅ ∪ (((𝑦 + 1) + 1)...𝑁))) |
383 | | imaundir 6014 |
. . . . . . . . . . . . 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)...𝑁))) |
384 | | uncom 4067 |
. . . . . . . . . . . . . 14
⊢ (∅
∪ (((𝑦 + 1) +
1)...𝑁)) = ((((𝑦 + 1) + 1)...𝑁) ∪ ∅) |
385 | | un0 4305 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 + 1) + 1)...𝑁) ∪ ∅) = (((𝑦 + 1) + 1)...𝑁) |
386 | 384, 385 | eqtr2i 2766 |
. . . . . . . . . . . . 13
⊢ (((𝑦 + 1) + 1)...𝑁) = (∅ ∪ (((𝑦 + 1) + 1)...𝑁)) |
387 | 382, 383,
386 | 3eqtr4g 2803 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) →
(({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))) “
(((𝑦 + 1) + 1)...𝑁)) = (((𝑦 + 1) + 1)...𝑁)) |
388 | 387 | imaeq2d 5929 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → ((2nd
‘(1st ‘𝑇)) “ (({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))) “ (((𝑦 + 1)
+ 1)...𝑁))) =
((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) |
389 | 337, 388 | syl5eq 2790 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ (2nd
‘𝑇) ≤ 𝑦) → (((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))) “ (((𝑦 + 1)
+ 1)...𝑁)) =
((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) |
390 | 389 | xpeq1d 5580 |
. . . . . . . . 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})) |
391 | 336, 390 | uneq12d 4078 |
. . . . . . . 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}))) |
392 | 276, 391 | syldan 594 |
. . . . . . 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}))) |
393 | 392 | oveq2d 7229 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2nd ‘𝑇)) → ((1st
‘(1st ‘𝑇)) ∘f + (((((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 ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) |
394 | | iffalse 4448 |
. . . . . . . . 9
⊢ (¬
𝑦 < (2nd
‘𝑇) → if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) = (𝑦 + 1)) |
395 | 394 | csbeq1d 3815 |
. . . . . . . 8
⊢ (¬
𝑦 < (2nd
‘𝑇) →
⦋if(𝑦 <
(2nd ‘𝑇),
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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 ‘𝑇)) ∘f + (((((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})))) |
396 | | ovex 7246 |
. . . . . . . . 9
⊢ (𝑦 + 1) ∈ V |
397 | | oveq2 7221 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑦 + 1) → (1...𝑗) = (1...(𝑦 + 1))) |
398 | 397 | imaeq2d 5929 |
. . . . . . . . . . . 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)))) |
399 | 398 | xpeq1d 5580 |
. . . . . . . . . . 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})) |
400 | | oveq1 7220 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑦 + 1) → (𝑗 + 1) = ((𝑦 + 1) + 1)) |
401 | 400 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑦 + 1) → ((𝑗 + 1)...𝑁) = (((𝑦 + 1) + 1)...𝑁)) |
402 | 401 | imaeq2d 5929 |
. . . . . . . . . . . 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)...𝑁))) |
403 | 402 | xpeq1d 5580 |
. . . . . . . . . . 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})) |
404 | 399, 403 | uneq12d 4078 |
. . . . . . . . . 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}))) |
405 | 404 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝑗 = (𝑦 + 1) → ((1st
‘(1st ‘𝑇)) ∘f + (((((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 ‘𝑇)) ∘f + (((((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})))) |
406 | 396, 405 | csbie 3847 |
. . . . . . . 8
⊢
⦋(𝑦 +
1) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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 ‘𝑇)) ∘f + (((((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}))) |
407 | 395, 406 | eqtrdi 2794 |
. . . . . . 7
⊢ (¬
𝑦 < (2nd
‘𝑇) →
⦋if(𝑦 <
(2nd ‘𝑇),
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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 ‘𝑇)) ∘f + (((((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})))) |
408 | 407 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2nd ‘𝑇)) →
⦋if(𝑦 <
(2nd ‘𝑇),
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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 ‘𝑇)) ∘f + (((((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})))) |
409 | 394 | csbeq1d 3815 |
. . . . . . . 8
⊢ (¬
𝑦 < (2nd
‘𝑇) →
⦋if(𝑦 <
(2nd ‘𝑇),
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑦 + 1) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
410 | 397 | imaeq2d 5929 |
. . . . . . . . . . . 12
⊢ (𝑗 = (𝑦 + 1) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...(𝑦 +
1)))) |
411 | 410 | xpeq1d 5580 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑦 + 1) → (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1})) |
412 | 401 | imaeq2d 5929 |
. . . . . . . . . . . 12
⊢ (𝑗 = (𝑦 + 1) → ((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) |
413 | 412 | xpeq1d 5580 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑦 + 1) → (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) |
414 | 411, 413 | uneq12d 4078 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑦 + 1) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) |
415 | 414 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝑗 = (𝑦 + 1) → ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) |
416 | 396, 415 | csbie 3847 |
. . . . . . . 8
⊢
⦋(𝑦 +
1) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) |
417 | 409, 416 | eqtrdi 2794 |
. . . . . . 7
⊢ (¬
𝑦 < (2nd
‘𝑇) →
⦋if(𝑦 <
(2nd ‘𝑇),
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) |
418 | 417 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2nd ‘𝑇)) →
⦋if(𝑦 <
(2nd ‘𝑇),
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) |
419 | 393, 408,
418 | 3eqtr4d 2787 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < (2nd ‘𝑇)) →
⦋if(𝑦 <
(2nd ‘𝑇),
𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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 ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
420 | 273, 419 | pm2.61dan 813 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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 ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
421 | 420 | mpteq2dva 5150 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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 ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
422 | 108, 421 | eqtr4d 2780 |
. 2
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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}))))) |
423 | | opex 5348 |
. . . . . . 7
⊢
〈(1st ‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉
∈ V |
424 | 423, 22 | op1std 7771 |
. . . . . 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)}))))〉) |
425 | 423, 22 | op2ndd 7772 |
. . . . . 6
⊢ (𝑡 = 〈〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉,
(2nd ‘𝑇)〉 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
426 | | breq2 5057 |
. . . . . . . . 9
⊢
((2nd ‘𝑡) = (2nd ‘𝑇) → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) |
427 | 426 | ifbid 4462 |
. . . . . . . 8
⊢
((2nd ‘𝑡) = (2nd ‘𝑇) → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) |
428 | 427 | csbeq1d 3815 |
. . . . . . 7
⊢
((2nd ‘𝑡) = (2nd ‘𝑇) → ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
429 | | fvex 6730 |
. . . . . . . . . 10
⊢
(1st ‘(1st ‘𝑇)) ∈ V |
430 | 429, 79 | op1std 7771 |
. . . . . . . . 9
⊢
((1st ‘𝑡) = 〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉
→ (1st ‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
431 | 429, 79 | op2ndd 7772 |
. . . . . . . . 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)}))))) |
432 | | id 22 |
. . . . . . . . . 10
⊢
((1st ‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇)) →
(1st ‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
433 | | imaeq1 5924 |
. . . . . . . . . . . 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...𝑗))) |
434 | 433 | xpeq1d 5580 |
. . . . . . . . . . 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})) |
435 | | imaeq1 5924 |
. . . . . . . . . . . 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)...𝑁))) |
436 | 435 | xpeq1d 5580 |
. . . . . . . . . . 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})) |
437 | 434, 436 | uneq12d 4078 |
. . . . . . . . . 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}))) |
438 | 432, 437 | oveqan12d 7232 |
. . . . . . . . 9
⊢
(((1st ‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇)) ∧
(2nd ‘(1st ‘𝑡)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))) →
((1st ‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + (((((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})))) |
439 | 430, 431,
438 | syl2anc 587 |
. . . . . . . 8
⊢
((1st ‘𝑡) = 〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉
→ ((1st ‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + (((((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})))) |
440 | 439 | csbeq2dv 3818 |
. . . . . . 7
⊢
((1st ‘𝑡) = 〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉
→ ⦋if(𝑦
< (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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})))) |
441 | 428, 440 | sylan9eqr 2800 |
. . . . . 6
⊢
(((1st ‘𝑡) = 〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉
∧ (2nd ‘𝑡) = (2nd ‘𝑇)) → ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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})))) |
442 | 424, 425,
441 | syl2anc 587 |
. . . . 5
⊢ (𝑡 = 〈〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉,
(2nd ‘𝑇)〉 → ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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})))) |
443 | 442 | mpteq2dv 5151 |
. . . 4
⊢ (𝑡 = 〈〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉,
(2nd ‘𝑇)〉 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((2nd
‘(1st ‘𝑇)) ∘ ({〈(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}))))) |
444 | 443 | eqeq2d 2748 |
. . 3
⊢ (𝑡 = 〈〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉,
(2nd ‘𝑇)〉 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((2nd
‘(1st ‘𝑇)) ∘ ({〈(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})))))) |
445 | 444, 3 | elrab2 3605 |
. 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..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + (((((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})))))) |
446 | 89, 422, 445 | sylanbrc 586 |
1
⊢ (𝜑 →
〈〈(1st ‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉,
(2nd ‘𝑇)〉 ∈ 𝑆) |