Proof of Theorem poimirlem17
Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | | poimirlem22.s |
. . . . 5
⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
3 | | poimirlem22.1 |
. . . . 5
⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) |
4 | | poimirlem22.2 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
5 | | poimirlem18.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) |
6 | | poimirlem18.4 |
. . . . 5
⊢ (𝜑 → (2nd
‘𝑇) =
0) |
7 | 1, 2, 3, 4, 5, 6 | poimirlem16 34789 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘f + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))))) |
8 | | elfznn0 12988 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ0) |
9 | 8 | nn0red 11944 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ) |
10 | 9 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ) |
11 | 1 | nnzd 12074 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℤ) |
12 | | peano2zm 12013 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
14 | 13 | zred 12075 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
15 | 14 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ) |
16 | 1 | nnred 11641 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℝ) |
17 | 16 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℝ) |
18 | | elfzle2 12899 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑁 − 1)) |
19 | 18 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ≤ (𝑁 − 1)) |
20 | 16 | ltm1d 11560 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 1) < 𝑁) |
21 | 20 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) < 𝑁) |
22 | 10, 15, 17, 19, 21 | lelttrd 10786 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁) |
23 | 22 | adantlr 711 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁) |
24 | | fveq2 6663 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 → (2nd ‘𝑡) = (2nd
‘〈〈(𝑛
∈ (1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉)) |
25 | | opex 5347 |
. . . . . . . . . . . . . . . 16
⊢
〈(𝑛 ∈
(1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉 ∈ V |
26 | | op2ndg 7691 |
. . . . . . . . . . . . . . . 16
⊢
((〈(𝑛 ∈
(1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉 ∈ V ∧ 𝑁 ∈ ℕ) →
(2nd ‘〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) = 𝑁) |
27 | 25, 1, 26 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2nd
‘〈〈(𝑛
∈ (1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) = 𝑁) |
28 | 24, 27 | sylan9eqr 2875 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → (2nd ‘𝑡) = 𝑁) |
29 | 28 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2nd
‘𝑡) = 𝑁) |
30 | 23, 29 | breqtrrd 5085 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < (2nd ‘𝑡)) |
31 | 30 | iftrued 4471 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = 𝑦) |
32 | 31 | csbeq1d 3884 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
33 | | vex 3495 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
34 | | oveq2 7153 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑦 → (1...𝑗) = (1...𝑦)) |
35 | 34 | imaeq2d 5922 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑦 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑡)) “
(1...𝑦))) |
36 | 35 | xpeq1d 5577 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑦 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑡)) “ (1...𝑦)) × {1})) |
37 | | oveq1 7152 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑦 → (𝑗 + 1) = (𝑦 + 1)) |
38 | 37 | oveq1d 7160 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑦 → ((𝑗 + 1)...𝑁) = ((𝑦 + 1)...𝑁)) |
39 | 38 | imaeq2d 5922 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑦 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑡)) “ ((𝑦 + 1)...𝑁))) |
40 | 39 | xpeq1d 5577 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑦 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑡)) “ ((𝑦 + 1)...𝑁)) × {0})) |
41 | 36, 40 | uneq12d 4137 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑦 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑡)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑦 + 1)...𝑁)) × {0}))) |
42 | 41 | oveq2d 7161 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑦 → ((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑦 + 1)...𝑁)) × {0})))) |
43 | 33, 42 | csbie 3915 |
. . . . . . . . . . . 12
⊢
⦋𝑦 /
𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑦 + 1)...𝑁)) × {0}))) |
44 | | 2fveq3 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘〈〈(𝑛
∈ (1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉))) |
45 | | op1stg 7690 |
. . . . . . . . . . . . . . . . 17
⊢
((〈(𝑛 ∈
(1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉 ∈ V ∧ 𝑁 ∈ ℕ) →
(1st ‘〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) = 〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉) |
46 | 25, 1, 45 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1st
‘〈〈(𝑛
∈ (1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) = 〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉) |
47 | 46 | fveq2d 6667 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1st
‘(1st ‘〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉)) = (1st
‘〈(𝑛 ∈
(1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉)) |
48 | | ovex 7178 |
. . . . . . . . . . . . . . . . 17
⊢
(1...𝑁) ∈
V |
49 | 48 | mptex 6977 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∈ V |
50 | | fvex 6676 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘(1st ‘𝑇)) ∈ V |
51 | 48 | mptex 6977 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∈ V |
52 | 50, 51 | coex 7624 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) ∈ V |
53 | 49, 52 | op1st 7686 |
. . . . . . . . . . . . . . 15
⊢
(1st ‘〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉) = (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) |
54 | 47, 53 | syl6eq 2869 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1st
‘(1st ‘〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉)) = (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0)))) |
55 | 44, 54 | sylan9eqr 2875 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → (1st
‘(1st ‘𝑡)) = (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0)))) |
56 | | fveq2 6663 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 → (1st ‘𝑡) = (1st
‘〈〈(𝑛
∈ (1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉)) |
57 | 56, 46 | sylan9eqr 2875 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → (1st ‘𝑡) = 〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉) |
58 | 57 | fveq2d 6667 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → (2nd
‘(1st ‘𝑡)) = (2nd ‘〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉)) |
59 | 49, 52 | op2nd 7687 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉) = ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) |
60 | 58, 59 | syl6eq 2869 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → (2nd
‘(1st ‘𝑡)) = ((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))) |
61 | 60 | imaeq1d 5921 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → ((2nd
‘(1st ‘𝑡)) “ (1...𝑦)) = (((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦))) |
62 | 61 | xpeq1d 5577 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → (((2nd
‘(1st ‘𝑡)) “ (1...𝑦)) × {1}) = ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1})) |
63 | 60 | imaeq1d 5921 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → ((2nd
‘(1st ‘𝑡)) “ ((𝑦 + 1)...𝑁)) = (((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁))) |
64 | 63 | xpeq1d 5577 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → (((2nd
‘(1st ‘𝑡)) “ ((𝑦 + 1)...𝑁)) × {0}) = ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})) |
65 | 62, 64 | uneq12d 4137 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑦 + 1)...𝑁)) × {0})) = (((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))) |
66 | 55, 65 | oveq12d 7163 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → ((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑦 + 1)...𝑁)) × {0}))) = ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘f + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))) |
67 | 43, 66 | syl5eq 2865 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → ⦋𝑦 / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘f + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))) |
68 | 67 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋𝑦 / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘f + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))) |
69 | 32, 68 | eqtrd 2853 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘f + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))) |
70 | 69 | mpteq2dva 5152 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘f + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))))) |
71 | 70 | eqeq2d 2829 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘f + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))))) |
72 | 71 | ex 413 |
. . . . . 6
⊢ (𝜑 → (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘f + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))))))) |
73 | 72 | alrimiv 1919 |
. . . . 5
⊢ (𝜑 → ∀𝑡(𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘f + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))))))) |
74 | | oveq2 7153 |
. . . . . . . . . . 11
⊢ (1 =
if(𝑛 = ((2nd
‘(1st ‘𝑇))‘1), 1, 0) → (((1st
‘(1st ‘𝑇))‘𝑛) + 1) = (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) |
75 | 74 | eleq1d 2894 |
. . . . . . . . . 10
⊢ (1 =
if(𝑛 = ((2nd
‘(1st ‘𝑇))‘1), 1, 0) → ((((1st
‘(1st ‘𝑇))‘𝑛) + 1) ∈ (0..^𝐾) ↔ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1, 0))
∈ (0..^𝐾))) |
76 | | oveq2 7153 |
. . . . . . . . . . 11
⊢ (0 =
if(𝑛 = ((2nd
‘(1st ‘𝑇))‘1), 1, 0) → (((1st
‘(1st ‘𝑇))‘𝑛) + 0) = (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) |
77 | 76 | eleq1d 2894 |
. . . . . . . . . 10
⊢ (0 =
if(𝑛 = ((2nd
‘(1st ‘𝑇))‘1), 1, 0) → ((((1st
‘(1st ‘𝑇))‘𝑛) + 0) ∈ (0..^𝐾) ↔ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1, 0))
∈ (0..^𝐾))) |
78 | | fveq2 6663 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → ((1st
‘(1st ‘𝑇))‘𝑛) = ((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1))) |
79 | 78 | oveq1d 7160 |
. . . . . . . . . . . . 13
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → (((1st
‘(1st ‘𝑇))‘𝑛) + 1) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) |
80 | 79 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 = ((2nd ‘(1st
‘𝑇))‘1)) →
(((1st ‘(1st ‘𝑇))‘𝑛) + 1) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) |
81 | | elrabi 3672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑇 ∈ {𝑡 ∈ ((((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...𝑁))) |
82 | 81, 2 | eleq2s 2928 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
83 | | xp1st 7710 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
84 | 4, 82, 83 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1st
‘𝑇) ∈
(((0..^𝐾)
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
85 | | xp1st 7710 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
86 | | elmapi 8417 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
87 | 84, 85, 86 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
88 | 4, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
89 | | xp2nd 7711 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
90 | 88, 83, 89 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
91 | | f1oeq1 6597 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
92 | 50, 91 | elab 3664 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
93 | 90, 92 | sylib 219 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
94 | | f1of 6608 |
. . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)⟶(1...𝑁)) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)⟶(1...𝑁)) |
96 | | nnuz 12269 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℕ =
(ℤ≥‘1) |
97 | 1, 96 | eleqtrdi 2920 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
98 | | eluzfz1 12902 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑁)) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈ (1...𝑁)) |
100 | 95, 99 | ffvelrnd 6844 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) |
101 | 87, 100 | ffvelrnd 6844 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ (0..^𝐾)) |
102 | | elfzonn0 13070 |
. . . . . . . . . . . . . . 15
⊢
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈
ℕ0) |
103 | | peano2nn0 11925 |
. . . . . . . . . . . . . . 15
⊢
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ ℕ0
→ (((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈
ℕ0) |
104 | 101, 102,
103 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈
ℕ0) |
105 | | elfzo0 13066 |
. . . . . . . . . . . . . . . 16
⊢
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ (0..^𝐾) ↔ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ ℕ0
∧ 𝐾 ∈ ℕ
∧ ((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) < 𝐾)) |
106 | 101, 105 | sylib 219 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ ℕ0
∧ 𝐾 ∈ ℕ
∧ ((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) < 𝐾)) |
107 | 106 | simp2d 1135 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ ℕ) |
108 | | elfzolt2 13035 |
. . . . . . . . . . . . . . . . 17
⊢
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) < 𝐾) |
109 | 101, 108 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) < 𝐾) |
110 | 101, 102 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈
ℕ0) |
111 | 110 | nn0zd 12073 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈
ℤ) |
112 | 107 | nnzd 12074 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈ ℤ) |
113 | | zltp1le 12020 |
. . . . . . . . . . . . . . . . 17
⊢
((((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ ℤ ∧ 𝐾 ∈ ℤ) →
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) < 𝐾 ↔ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ≤ 𝐾)) |
114 | 111, 112,
113 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) < 𝐾 ↔ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ≤ 𝐾)) |
115 | 109, 114 | mpbid 233 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ≤ 𝐾) |
116 | | fvex 6676 |
. . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇))‘1) ∈ V |
117 | | eleq1 2897 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → (𝑛 ∈ (1...𝑁) ↔ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁))) |
118 | 117 | anbi2d 628 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ↔ (𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)))) |
119 | | fveq2 6663 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → (𝑝‘𝑛) = (𝑝‘((2nd
‘(1st ‘𝑇))‘1))) |
120 | 119 | neeq1d 3072 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → ((𝑝‘𝑛) ≠ 𝐾 ↔ (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾)) |
121 | 120 | rexbidv 3294 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → (∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾 ↔ ∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾)) |
122 | 118, 121 | imbi12d 346 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) ↔ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾))) |
123 | 116, 122,
5 | vtocl 3557 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾) |
124 | 100, 123 | mpdan 683 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾) |
125 | | fveq1 6662 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘1))) |
126 | 87 | ffnd 6508 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
127 | 126 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
128 | | 1ex 10625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 ∈
V |
129 | | fnconstg 6560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (1 ∈
V → (((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1)))) |
130 | 128, 129 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) |
131 | | c0ex 10623 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 0 ∈
V |
132 | | fnconstg 6560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (0 ∈
V → (((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) |
133 | 131, 132 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) |
134 | 130, 133 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∧ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) |
135 | | dff1o3 6614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡(2nd ‘(1st
‘𝑇)))) |
136 | 135 | simprbi 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡(2nd ‘(1st
‘𝑇))) |
137 | 93, 136 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → Fun ◡(2nd ‘(1st
‘𝑇))) |
138 | | imain 6432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Fun
◡(2nd ‘(1st
‘𝑇)) →
((2nd ‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))) |
139 | 137, 138 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))) |
140 | | nn0p1nn 11924 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ ℕ0
→ (𝑦 + 1) ∈
ℕ) |
141 | 8, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℕ) |
142 | 141 | nnred 11641 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℝ) |
143 | 142 | ltp1d 11558 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) < ((𝑦 + 1) + 1)) |
144 | | fzdisj 12922 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑦 + 1) < ((𝑦 + 1) + 1) → ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅) |
145 | 144 | imaeq2d 5922 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑦 + 1) < ((𝑦 + 1) + 1) → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ((2nd
‘(1st ‘𝑇)) “ ∅)) |
146 | | ima0 5938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((2nd ‘(1st ‘𝑇)) “ ∅) =
∅ |
147 | 145, 146 | syl6eq 2869 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 + 1) < ((𝑦 + 1) + 1) → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ∅) |
148 | 143, 147 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ∅) |
149 | 139, 148 | sylan9req 2874 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅) |
150 | | fnun 6456 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∧ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) ∧ (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅) → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))) |
151 | 134, 149,
150 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))) |
152 | | imaundi 6001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((2nd ‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) |
153 | 141 | peano2nnd 11643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℕ) |
154 | 153, 96 | eleqtrdi 2920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈
(ℤ≥‘1)) |
155 | 154 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1) + 1) ∈
(ℤ≥‘1)) |
156 | 1 | nncnd 11642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝑁 ∈ ℂ) |
157 | | npcan1 11053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
158 | 156, 157 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
159 | 158 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁) |
160 | | elfzuz3 12893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑦)) |
161 | | eluzp1p1 12258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 − 1) ∈
(ℤ≥‘𝑦) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑦 + 1))) |
162 | 160, 161 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑦 + 1))) |
163 | 162 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑦 + 1))) |
164 | 159, 163 | eqeltrrd 2911 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ≥‘(𝑦 + 1))) |
165 | | fzsplit2 12920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑦 + 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑦 + 1))) → (1...𝑁) = ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) |
166 | 155, 164,
165 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) = ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) |
167 | 166 | imaeq2d 5922 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = ((2nd ‘(1st
‘𝑇)) “
((1...(𝑦 + 1)) ∪
(((𝑦 + 1) + 1)...𝑁)))) |
168 | | f1ofo 6615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) |
169 | | foima 6588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
170 | 93, 168, 169 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
171 | 170 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
172 | 167, 171 | eqtr3d 2855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (1...𝑁)) |
173 | 152, 172 | syl5eqr 2867 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = (1...𝑁)) |
174 | 173 | fneq2d 6440 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) ↔ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))) |
175 | 151, 174 | mpbid 233 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
176 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) ∈ V) |
177 | | inidm 4192 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
178 | | eqidd 2819 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) = ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1))) |
179 | | f1ofn 6609 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)) Fn (1...𝑁)) |
180 | 93, 179 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) Fn (1...𝑁)) |
181 | 180 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2nd
‘(1st ‘𝑇)) Fn (1...𝑁)) |
182 | | fzss2 12935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈
(ℤ≥‘(𝑦 + 1)) → (1...(𝑦 + 1)) ⊆ (1...𝑁)) |
183 | 164, 182 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...(𝑦 + 1)) ⊆ (1...𝑁)) |
184 | 141, 96 | eleqtrdi 2920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈
(ℤ≥‘1)) |
185 | | eluzfz1 12902 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑦 + 1) ∈
(ℤ≥‘1) → 1 ∈ (1...(𝑦 + 1))) |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 1 ∈ (1...(𝑦 + 1))) |
187 | 186 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 1 ∈ (1...(𝑦 + 1))) |
188 | | fnfvima 6986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((2nd ‘(1st ‘𝑇)) Fn (1...𝑁) ∧ (1...(𝑦 + 1)) ⊆ (1...𝑁) ∧ 1 ∈ (1...(𝑦 + 1))) → ((2nd
‘(1st ‘𝑇))‘1) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1)))) |
189 | 181, 183,
187, 188 | syl3anc 1363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑇))‘1) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1)))) |
190 | | fvun1 6747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∧ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) ∧ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅ ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))))) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘1)) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd
‘(1st ‘𝑇))‘1))) |
191 | 130, 133,
190 | mp3an12 1442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅ ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1)))) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘1)) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd
‘(1st ‘𝑇))‘1))) |
192 | 149, 189,
191 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘1)) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd
‘(1st ‘𝑇))‘1))) |
193 | 128 | fvconst2 6958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((2nd ‘(1st ‘𝑇))‘1) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd
‘(1st ‘𝑇))‘1)) = 1) |
194 | 189, 193 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd
‘(1st ‘𝑇))‘1)) = 1) |
195 | 192, 194 | eqtrd 2853 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘1)) = 1) |
196 | 195 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘1)) = 1) |
197 | 127, 175,
176, 176, 177, 178, 196 | ofval 7407 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) |
198 | 100, 197 | mpidan 685 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) |
199 | 125, 198 | sylan9eqr 2875 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑝 = ((1st ‘(1st
‘𝑇))
∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) |
200 | 199 | adantllr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑝 ∈ ran 𝐹) ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑝 = ((1st ‘(1st
‘𝑇))
∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) |
201 | | fveq2 6663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
202 | 201 | breq2d 5069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) |
203 | 202 | ifbid 4485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) |
204 | 203 | csbeq1d 3884 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑡 = 𝑇 → ⦋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})))) |
205 | | 2fveq3 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
206 | | 2fveq3 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) |
207 | 206 | imaeq1d 5921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑗))) |
208 | 207 | xpeq1d 5577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1})) |
209 | 206 | imaeq1d 5921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
210 | 209 | xpeq1d 5577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
211 | 208, 210 | uneq12d 4137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑡 = 𝑇 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
212 | 205, 211 | oveq12d 7163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
213 | 212 | csbeq2dv 3887 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑡 = 𝑇 → ⦋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})))) |
214 | 204, 213 | eqtrd 2853 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑡 = 𝑇 → ⦋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})))) |
215 | 214 | mpteq2dv 5153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑡 = 𝑇 → (𝑦 ∈ (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}))))) |
216 | 215 | eqeq2d 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (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})))))) |
217 | 216, 2 | elrab2 3680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((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})))))) |
218 | 217 | simprbi 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
219 | 4, 218 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
220 | 219 | rneqd 5801 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ran 𝐹 = ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
221 | 220 | eleq2d 2895 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑝 ∈ ran 𝐹 ↔ 𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
222 | | eqid 2818 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ (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})))) |
223 | | ovex 7178 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((1st ‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V |
224 | 223 | csbex 5206 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
⦋if(𝑦
< (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V |
225 | 222, 224 | elrnmpti 5825 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑝 ∈ ran (𝑦 ∈ (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})))) |
226 | 221, 225 | syl6bb 288 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑝 ∈ ran 𝐹 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
227 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2nd
‘𝑇) =
0) |
228 | | elfzle1 12898 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 0 ≤ 𝑦) |
229 | 228 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 0 ≤ 𝑦) |
230 | 227, 229 | eqbrtrd 5079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2nd
‘𝑇) ≤ 𝑦) |
231 | | 0re 10631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 0 ∈
ℝ |
232 | 6, 231 | syl6eqel 2918 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (2nd
‘𝑇) ∈
ℝ) |
233 | | lenlt 10707 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((2nd ‘𝑇) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((2nd
‘𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd ‘𝑇))) |
234 | 232, 9, 233 | syl2an 595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd ‘𝑇))) |
235 | 230, 234 | mpbid 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ¬ 𝑦 < (2nd
‘𝑇)) |
236 | 235 | iffalsed 4474 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = (𝑦 + 1)) |
237 | 236 | csbeq1d 3884 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑦 + 1) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
238 | | ovex 7178 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 + 1) ∈ V |
239 | | oveq2 7153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑗 = (𝑦 + 1) → (1...𝑗) = (1...(𝑦 + 1))) |
240 | 239 | imaeq2d 5922 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 = (𝑦 + 1) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...(𝑦 +
1)))) |
241 | 240 | xpeq1d 5577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 = (𝑦 + 1) → (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1})) |
242 | | oveq1 7152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 = (𝑦 + 1) → (𝑗 + 1) = ((𝑦 + 1) + 1)) |
243 | 242 | oveq1d 7160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑗 = (𝑦 + 1) → ((𝑗 + 1)...𝑁) = (((𝑦 + 1) + 1)...𝑁)) |
244 | 243 | imaeq2d 5922 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 = (𝑦 + 1) → ((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) |
245 | 244 | xpeq1d 5577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 = (𝑦 + 1) → (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) |
246 | 241, 245 | uneq12d 4137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 = (𝑦 + 1) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) |
247 | 246 | oveq2d 7161 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑗 = (𝑦 + 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})))) |
248 | 238, 247 | csbie 3915 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
⦋(𝑦 +
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}))) |
249 | 237, 248 | syl6eq 2869 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) |
250 | 249 | eqeq2d 2829 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑝 = ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) ↔ 𝑝 = ((1st ‘(1st
‘𝑇))
∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))) |
251 | 250 | rexbidva 3293 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ((1st ‘(1st
‘𝑇))
∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))) |
252 | 226, 251 | bitrd 280 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑝 ∈ ran 𝐹 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ((1st ‘(1st
‘𝑇))
∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))) |
253 | 252 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ((1st ‘(1st
‘𝑇))
∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) |
254 | 200, 253 | r19.29a 3286 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) |
255 | | eqtr3 2840 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∧ 𝐾 = (((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = 𝐾) |
256 | 255 | ex 413 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) → (𝐾 = (((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = 𝐾)) |
257 | 254, 256 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → (𝐾 = (((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = 𝐾)) |
258 | 257 | necon3d 3034 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → ((𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾 → 𝐾 ≠ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1))) |
259 | 258 | rexlimdva 3281 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾 → 𝐾 ≠ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1))) |
260 | 124, 259 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ≠ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) |
261 | 104 | nn0red 11944 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈
ℝ) |
262 | 107 | nnred 11641 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ ℝ) |
263 | 261, 262 | ltlend 10773 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) < 𝐾 ↔ ((((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ≤ 𝐾 ∧ 𝐾 ≠ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)))) |
264 | 115, 260,
263 | mpbir2and 709 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) < 𝐾) |
265 | | elfzo0 13066 |
. . . . . . . . . . . . . 14
⊢
((((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈ (0..^𝐾) ↔ ((((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈ ℕ0
∧ 𝐾 ∈ ℕ
∧ (((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) < 𝐾)) |
266 | 104, 107,
264, 265 | syl3anbrc 1335 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈ (0..^𝐾)) |
267 | 266 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 = ((2nd ‘(1st
‘𝑇))‘1)) →
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈ (0..^𝐾)) |
268 | 80, 267 | eqeltrd 2910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 = ((2nd ‘(1st
‘𝑇))‘1)) →
(((1st ‘(1st ‘𝑇))‘𝑛) + 1) ∈ (0..^𝐾)) |
269 | 268 | adantlr 711 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 = ((2nd ‘(1st
‘𝑇))‘1)) →
(((1st ‘(1st ‘𝑇))‘𝑛) + 1) ∈ (0..^𝐾)) |
270 | 87 | ffvelrnda 6843 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈ (0..^𝐾)) |
271 | | elfzonn0 13070 |
. . . . . . . . . . . . . . 15
⊢
(((1st ‘(1st ‘𝑇))‘𝑛) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈
ℕ0) |
272 | 270, 271 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈
ℕ0) |
273 | 272 | nn0cnd 11945 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈ ℂ) |
274 | 273 | addid1d 10828 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) + 0) = ((1st
‘(1st ‘𝑇))‘𝑛)) |
275 | 274, 270 | eqeltrd 2910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) + 0) ∈ (0..^𝐾)) |
276 | 275 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2nd ‘(1st
‘𝑇))‘1)) →
(((1st ‘(1st ‘𝑇))‘𝑛) + 0) ∈ (0..^𝐾)) |
277 | 75, 77, 269, 276 | ifbothda 4500 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1, 0))
∈ (0..^𝐾)) |
278 | 277 | fmpttd 6871 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))):(1...𝑁)⟶(0..^𝐾)) |
279 | | ovex 7178 |
. . . . . . . . 9
⊢
(0..^𝐾) ∈
V |
280 | 279, 48 | elmap 8424 |
. . . . . . . 8
⊢ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∈ ((0..^𝐾)
↑m (1...𝑁))
↔ (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))):(1...𝑁)⟶(0..^𝐾)) |
281 | 278, 280 | sylibr 235 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∈ ((0..^𝐾)
↑m (1...𝑁))) |
282 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → 𝑛 ∈ (1...(𝑁 − 1))) |
283 | | 1z 12000 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℤ |
284 | 13, 283 | jctil 520 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 ∈ ℤ ∧
(𝑁 − 1) ∈
ℤ)) |
285 | | elfzelz 12896 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℤ) |
286 | 285, 283 | jctir 521 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (1...(𝑁 − 1)) → (𝑛 ∈ ℤ ∧ 1 ∈
ℤ)) |
287 | | fzaddel 12929 |
. . . . . . . . . . . . . . . 16
⊢ (((1
∈ ℤ ∧ (𝑁
− 1) ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
→ (𝑛 ∈
(1...(𝑁 − 1)) ↔
(𝑛 + 1) ∈ ((1 +
1)...((𝑁 − 1) +
1)))) |
288 | 284, 286,
287 | syl2an 595 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 ∈ (1...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1)))) |
289 | 282, 288 | mpbid 233 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1))) |
290 | 158 | oveq2d 7161 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 +
1)...𝑁)) |
291 | 290 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 +
1)...𝑁)) |
292 | 289, 291 | eleqtrd 2912 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 + 1) ∈ ((1 + 1)...𝑁)) |
293 | 292 | ralrimiva 3179 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑛 + 1) ∈ ((1 + 1)...𝑁)) |
294 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → 𝑦 ∈ ((1 + 1)...𝑁)) |
295 | | peano2z 12011 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 ∈
ℤ → (1 + 1) ∈ ℤ) |
296 | 283, 295 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 + 1)
∈ ℤ |
297 | 11, 296 | jctil 520 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1 + 1) ∈ ℤ
∧ 𝑁 ∈
ℤ)) |
298 | | elfzelz 12896 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ((1 + 1)...𝑁) → 𝑦 ∈ ℤ) |
299 | 298, 283 | jctir 521 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ((1 + 1)...𝑁) → (𝑦 ∈ ℤ ∧ 1 ∈
ℤ)) |
300 | | fzsubel 12931 |
. . . . . . . . . . . . . . . . 17
⊢ ((((1 +
1) ∈ ℤ ∧ 𝑁
∈ ℤ) ∧ (𝑦
∈ ℤ ∧ 1 ∈ ℤ)) → (𝑦 ∈ ((1 + 1)...𝑁) ↔ (𝑦 − 1) ∈ (((1 + 1) −
1)...(𝑁 −
1)))) |
301 | 297, 299,
300 | syl2an 595 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 ∈ ((1 + 1)...𝑁) ↔ (𝑦 − 1) ∈ (((1 + 1) −
1)...(𝑁 −
1)))) |
302 | 294, 301 | mpbid 233 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 − 1) ∈ (((1 + 1) −
1)...(𝑁 −
1))) |
303 | | ax-1cn 10583 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
304 | 303, 303 | pncan3oi 10890 |
. . . . . . . . . . . . . . . 16
⊢ ((1 + 1)
− 1) = 1 |
305 | 304 | oveq1i 7155 |
. . . . . . . . . . . . . . 15
⊢ (((1 + 1)
− 1)...(𝑁 − 1))
= (1...(𝑁 −
1)) |
306 | 302, 305 | eleqtrdi 2920 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 − 1) ∈ (1...(𝑁 − 1))) |
307 | 298 | zcnd 12076 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ((1 + 1)...𝑁) → 𝑦 ∈ ℂ) |
308 | | elfznn 12924 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℕ) |
309 | 308 | nncnd 11642 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℂ) |
310 | | subadd2 10878 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℂ ∧ 1 ∈
ℂ ∧ 𝑛 ∈
ℂ) → ((𝑦 −
1) = 𝑛 ↔ (𝑛 + 1) = 𝑦)) |
311 | 303, 310 | mp3an2 1440 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑦 − 1) = 𝑛 ↔ (𝑛 + 1) = 𝑦)) |
312 | 311 | bicomd 224 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑛 + 1) = 𝑦 ↔ (𝑦 − 1) = 𝑛)) |
313 | | eqcom 2825 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (𝑛 + 1) ↔ (𝑛 + 1) = 𝑦) |
314 | | eqcom 2825 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = (𝑦 − 1) ↔ (𝑦 − 1) = 𝑛) |
315 | 312, 313,
314 | 3bitr4g 315 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) |
316 | 307, 309,
315 | syl2an 595 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ((1 + 1)...𝑁) ∧ 𝑛 ∈ (1...(𝑁 − 1))) → (𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) |
317 | 316 | ralrimiva 3179 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ((1 + 1)...𝑁) → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) |
318 | 317 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) |
319 | | reu6i 3716 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 − 1) ∈ (1...(𝑁 − 1)) ∧ ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) → ∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1)) |
320 | 306, 318,
319 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → ∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1)) |
321 | 320 | ralrimiva 3179 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑦 ∈ ((1 + 1)...𝑁)∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1)) |
322 | | eqid 2818 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) = (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) |
323 | 322 | f1ompt 6867 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 +
1)...𝑁) ↔
(∀𝑛 ∈
(1...(𝑁 − 1))(𝑛 + 1) ∈ ((1 + 1)...𝑁) ∧ ∀𝑦 ∈ ((1 + 1)...𝑁)∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1))) |
324 | 293, 321,
323 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 +
1)...𝑁)) |
325 | | f1osng 6648 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 1 ∈
V) → {〈𝑁,
1〉}:{𝑁}–1-1-onto→{1}) |
326 | 1, 128, 325 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝜑 → {〈𝑁, 1〉}:{𝑁}–1-1-onto→{1}) |
327 | 14, 16 | ltnled 10775 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1))) |
328 | 20, 327 | mpbid 233 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1)) |
329 | | elfzle2 12899 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1)) |
330 | 328, 329 | nsyl 142 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1))) |
331 | | disjsn 4639 |
. . . . . . . . . . . 12
⊢
(((1...(𝑁 −
1)) ∩ {𝑁}) = ∅
↔ ¬ 𝑁 ∈
(1...(𝑁 −
1))) |
332 | 330, 331 | sylibr 235 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅) |
333 | | 1re 10629 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
334 | 333 | ltp1i 11532 |
. . . . . . . . . . . . . . 15
⊢ 1 < (1
+ 1) |
335 | 296 | zrei 11975 |
. . . . . . . . . . . . . . . 16
⊢ (1 + 1)
∈ ℝ |
336 | 333, 335 | ltnlei 10749 |
. . . . . . . . . . . . . . 15
⊢ (1 <
(1 + 1) ↔ ¬ (1 + 1) ≤ 1) |
337 | 334, 336 | mpbi 231 |
. . . . . . . . . . . . . 14
⊢ ¬ (1
+ 1) ≤ 1 |
338 | | elfzle1 12898 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
((1 + 1)...𝑁) → (1 +
1) ≤ 1) |
339 | 337, 338 | mto 198 |
. . . . . . . . . . . . 13
⊢ ¬ 1
∈ ((1 + 1)...𝑁) |
340 | | disjsn 4639 |
. . . . . . . . . . . . 13
⊢ ((((1 +
1)...𝑁) ∩ {1}) =
∅ ↔ ¬ 1 ∈ ((1 + 1)...𝑁)) |
341 | 339, 340 | mpbir 232 |
. . . . . . . . . . . 12
⊢ (((1 +
1)...𝑁) ∩ {1}) =
∅ |
342 | 341 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (((1 + 1)...𝑁) ∩ {1}) =
∅) |
343 | | f1oun 6627 |
. . . . . . . . . . 11
⊢ ((((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 +
1)...𝑁) ∧ {〈𝑁, 1〉}:{𝑁}–1-1-onto→{1})
∧ (((1...(𝑁 − 1))
∩ {𝑁}) = ∅ ∧
(((1 + 1)...𝑁) ∩ {1}) =
∅)) → ((𝑛 ∈
(1...(𝑁 − 1)) ↦
(𝑛 + 1)) ∪ {〈𝑁, 1〉}):((1...(𝑁 − 1)) ∪ {𝑁})–1-1-onto→(((1
+ 1)...𝑁) ∪
{1})) |
344 | 324, 326,
332, 342, 343 | syl22anc 834 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {〈𝑁, 1〉}):((1...(𝑁 − 1)) ∪ {𝑁})–1-1-onto→(((1
+ 1)...𝑁) ∪
{1})) |
345 | | elex 3510 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ V) |
346 | 1, 345 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ V) |
347 | 128 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
V) |
348 | 158, 97 | eqeltrd 2910 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘1)) |
349 | | uzid 12246 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
350 | | peano2uz 12289 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
351 | 13, 349, 350 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
352 | 158, 351 | eqeltrrd 2911 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
353 | | fzsplit2 12920 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
354 | 348, 352,
353 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
355 | 158 | oveq1d 7160 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁)) |
356 | | fzsn 12937 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁}) |
357 | 11, 356 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁...𝑁) = {𝑁}) |
358 | 355, 357 | eqtrd 2853 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁}) |
359 | 358 | uneq2d 4136 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
360 | 354, 359 | eqtr2d 2854 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁)) |
361 | | iftrue 4469 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑁 → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = 1) |
362 | 361 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = 1) |
363 | 346, 347,
360, 362 | fmptapd 6925 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∪ {〈𝑁, 1〉}) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) |
364 | | eleq1 2897 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑁 → (𝑛 ∈ (1...(𝑁 − 1)) ↔ 𝑁 ∈ (1...(𝑁 − 1)))) |
365 | 364 | notbid 319 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑁 → (¬ 𝑛 ∈ (1...(𝑁 − 1)) ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1)))) |
366 | 330, 365 | syl5ibrcom 248 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑛 = 𝑁 → ¬ 𝑛 ∈ (1...(𝑁 − 1)))) |
367 | 366 | necon2ad 3028 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ≠ 𝑁)) |
368 | 367 | imp 407 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → 𝑛 ≠ 𝑁) |
369 | | ifnefalse 4475 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ≠ 𝑁 → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1)) |
370 | 368, 369 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1)) |
371 | 370 | mpteq2dva 5152 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1))) |
372 | 371 | uneq1d 4135 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∪ {〈𝑁, 1〉}) = ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {〈𝑁, 1〉})) |
373 | 363, 372 | eqtr3d 2855 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {〈𝑁, 1〉})) |
374 | 354, 359 | eqtrd 2853 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
375 | | uzid 12246 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℤ → 1 ∈ (ℤ≥‘1)) |
376 | | peano2uz 12289 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
(ℤ≥‘1) → (1 + 1) ∈
(ℤ≥‘1)) |
377 | 283, 375,
376 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ (1 + 1)
∈ (ℤ≥‘1) |
378 | | fzsplit2 12920 |
. . . . . . . . . . . . 13
⊢ (((1 + 1)
∈ (ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘1))
→ (1...𝑁) = ((1...1)
∪ ((1 + 1)...𝑁))) |
379 | 377, 97, 378 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝑁) = ((1...1) ∪ ((1 + 1)...𝑁))) |
380 | | fzsn 12937 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℤ → (1...1) = {1}) |
381 | 283, 380 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (1...1) =
{1} |
382 | 381 | uneq1i 4132 |
. . . . . . . . . . . . 13
⊢ ((1...1)
∪ ((1 + 1)...𝑁)) = ({1}
∪ ((1 + 1)...𝑁)) |
383 | 382 | equncomi 4128 |
. . . . . . . . . . . 12
⊢ ((1...1)
∪ ((1 + 1)...𝑁)) = (((1
+ 1)...𝑁) ∪
{1}) |
384 | 379, 383 | syl6eq 2869 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...𝑁) = (((1 + 1)...𝑁) ∪ {1})) |
385 | 373, 374,
384 | f1oeq123d 6603 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {〈𝑁, 1〉}):((1...(𝑁 − 1)) ∪ {𝑁})–1-1-onto→(((1
+ 1)...𝑁) ∪
{1}))) |
386 | 344, 385 | mpbird 258 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁)) |
387 | | f1oco 6630 |
. . . . . . . . 9
⊢
(((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ∧ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁)) → ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁)) |
388 | 93, 386, 387 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁)) |
389 | | f1oeq1 6597 |
. . . . . . . . 9
⊢ (𝑓 = ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁))) |
390 | 52, 389 | elab 3664 |
. . . . . . . 8
⊢
(((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁)) |
391 | 388, 390 | sylibr 235 |
. . . . . . 7
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
392 | | opelxpi 5585 |
. . . . . . 7
⊢ (((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∈ ((0..^𝐾)
↑m (1...𝑁))
∧ ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → 〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
393 | 281, 391,
392 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → 〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
394 | 1 | nnnn0d 11943 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
395 | | nn0fz0 12993 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈ (0...𝑁)) |
396 | 394, 395 | sylib 219 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (0...𝑁)) |
397 | | opelxpi 5585 |
. . . . . 6
⊢
((〈(𝑛 ∈
(1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑁 ∈ (0...𝑁)) → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
398 | 393, 396,
397 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
399 | | elrab3t 3676 |
. . . . 5
⊢
((∀𝑡(𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘f + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))))) ∧
〈〈(𝑛 ∈
(1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ∈ {𝑡 ∈ ((((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...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘f + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))))) |
400 | 73, 398, 399 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ∈ {𝑡 ∈ ((((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...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘f + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))))) |
401 | 7, 400 | mpbird 258 |
. . 3
⊢ (𝜑 → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ∈ {𝑡 ∈ ((((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}))))}) |
402 | 401, 2 | eleqtrrdi 2921 |
. 2
⊢ (𝜑 → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ∈ 𝑆) |
403 | | fveqeq2 6672 |
. . . . . 6
⊢
(〈〈(𝑛
∈ (1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 = 𝑇 → ((2nd
‘〈〈(𝑛
∈ (1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) = 𝑁 ↔ (2nd ‘𝑇) = 𝑁)) |
404 | 27, 403 | syl5ibcom 246 |
. . . . 5
⊢ (𝜑 → (〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 = 𝑇 → (2nd ‘𝑇) = 𝑁)) |
405 | 1 | nnne0d 11675 |
. . . . . 6
⊢ (𝜑 → 𝑁 ≠ 0) |
406 | | neeq1 3075 |
. . . . . 6
⊢
((2nd ‘𝑇) = 𝑁 → ((2nd ‘𝑇) ≠ 0 ↔ 𝑁 ≠ 0)) |
407 | 405, 406 | syl5ibrcom 248 |
. . . . 5
⊢ (𝜑 → ((2nd
‘𝑇) = 𝑁 → (2nd
‘𝑇) ≠
0)) |
408 | 404, 407 | syld 47 |
. . . 4
⊢ (𝜑 → (〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 = 𝑇 → (2nd ‘𝑇) ≠ 0)) |
409 | 408 | necon2d 3036 |
. . 3
⊢ (𝜑 → ((2nd
‘𝑇) = 0 →
〈〈(𝑛 ∈
(1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ≠ 𝑇)) |
410 | 6, 409 | mpd 15 |
. 2
⊢ (𝜑 → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ≠ 𝑇) |
411 | | neeq1 3075 |
. . 3
⊢ (𝑧 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 → (𝑧 ≠ 𝑇 ↔ 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ≠ 𝑇)) |
412 | 411 | rspcev 3620 |
. 2
⊢
((〈〈(𝑛
∈ (1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ∈ 𝑆 ∧ 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ≠ 𝑇) → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
413 | 402, 410,
412 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |