Proof of Theorem poimirlem17
Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | | poimirlem22.s |
. . . . 5
⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
3 | | poimirlem22.1 |
. . . . 5
⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (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 33425 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))))) |
8 | | elfznn0 12433 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ0) |
9 | 8 | nn0red 11352 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ) |
10 | 9 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ) |
11 | 1 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℤ) |
12 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
14 | 13 | zred 11482 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
15 | 14 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ) |
16 | 1 | nnred 11035 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℝ) |
17 | 16 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℝ) |
18 | | elfzle2 12345 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑁 − 1)) |
19 | 18 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ≤ (𝑁 − 1)) |
20 | 16 | ltm1d 10956 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 1) < 𝑁) |
21 | 20 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) < 𝑁) |
22 | 10, 15, 17, 19, 21 | lelttrd 10195 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁) |
23 | 22 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁) |
24 | | fveq2 6191 |
. . . . . . . . . . . . . . 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 4932 |
. . . . . . . . . . . . . . . 16
⊢
〈(𝑛 ∈
(1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉 ∈ V |
26 | | op2ndg 7181 |
. . . . . . . . . . . . . . . 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 695 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2nd
‘〈〈(𝑛
∈ (1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) = 𝑁) |
28 | 24, 27 | sylan9eqr 2678 |
. . . . . . . . . . . . . 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 4681 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < (2nd ‘𝑡)) |
31 | 30 | iftrued 4094 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = 𝑦) |
32 | 31 | csbeq1d 3540 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
33 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
34 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑦 → (1...𝑗) = (1...𝑦)) |
35 | 34 | imaeq2d 5466 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑦 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑡)) “
(1...𝑦))) |
36 | 35 | xpeq1d 5138 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑦 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑡)) “ (1...𝑦)) × {1})) |
37 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑦 → (𝑗 + 1) = (𝑦 + 1)) |
38 | 37 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑦 → ((𝑗 + 1)...𝑁) = ((𝑦 + 1)...𝑁)) |
39 | 38 | imaeq2d 5466 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑦 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑡)) “ ((𝑦 + 1)...𝑁))) |
40 | 39 | xpeq1d 5138 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑦 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑡)) “ ((𝑦 + 1)...𝑁)) × {0})) |
41 | 36, 40 | uneq12d 3768 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑦 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑡)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑦 + 1)...𝑁)) × {0}))) |
42 | 41 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑦 → ((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑦 + 1)...𝑁)) × {0})))) |
43 | 33, 42 | csbie 3559 |
. . . . . . . . . . . 12
⊢
⦋𝑦 /
𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑦 + 1)...𝑁)) × {0}))) |
44 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 〈〈(𝑛 ∈ (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))))〉, 𝑁〉)) |
45 | 44 | fveq2d 6195 |
. . . . . . . . . . . . . 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))))〉, 𝑁〉))) |
46 | | op1stg 7180 |
. . . . . . . . . . . . . . . . 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))))〉) |
47 | 25, 1, 46 | sylancr 695 |
. . . . . . . . . . . . . . . 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))))〉) |
48 | 47 | fveq2d 6195 |
. . . . . . . . . . . . . . 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))))〉)) |
49 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
⊢
(1...𝑁) ∈
V |
50 | 49 | mptex 6486 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∈ V |
51 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘(1st ‘𝑇)) ∈ V |
52 | 49 | mptex 6486 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∈ V |
53 | 51, 52 | coex 7118 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) ∈ V |
54 | 50, 53 | op1st 7176 |
. . . . . . . . . . . . . . 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))) |
55 | 48, 54 | syl6eq 2672 |
. . . . . . . . . . . . . 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)))) |
56 | 45, 55 | sylan9eqr 2678 |
. . . . . . . . . . . . 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)))) |
57 | 44, 47 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . 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 6195 |
. . . . . . . . . . . . . . . . 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 | 50, 53 | op2nd 7177 |
. . . . . . . . . . . . . . . . 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 2672 |
. . . . . . . . . . . . . . . 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 5465 |
. . . . . . . . . . . . . . 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 5138 |
. . . . . . . . . . . . . 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 5465 |
. . . . . . . . . . . . . . 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 5138 |
. . . . . . . . . . . . . 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 3768 |
. . . . . . . . . . . . 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 | 56, 65 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → ((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑦 + 1)...𝑁)) × {0}))) = ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))) |
67 | 43, 66 | syl5eq 2668 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → ⦋𝑦 / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘𝑓 + (((((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 ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))) |
69 | 32, 68 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))) |
70 | 69 | mpteq2dva 4744 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))))) |
71 | 70 | eqeq2d 2632 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))))) |
72 | 71 | ex 450 |
. . . . . 6
⊢ (𝜑 → (𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))))))) |
73 | 72 | alrimiv 1855 |
. . . . 5
⊢ (𝜑 → ∀𝑡(𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0}))))))) |
74 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (1 =
if(𝑛 = ((2nd
‘(1st ‘𝑇))‘1), 1, 0) → (((1st
‘(1st ‘𝑇))‘𝑛) + 1) = (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) |
75 | 74 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (1 =
if(𝑛 = ((2nd
‘(1st ‘𝑇))‘1), 1, 0) → ((((1st
‘(1st ‘𝑇))‘𝑛) + 1) ∈ (0..^𝐾) ↔ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1, 0))
∈ (0..^𝐾))) |
76 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (0 =
if(𝑛 = ((2nd
‘(1st ‘𝑇))‘1), 1, 0) → (((1st
‘(1st ‘𝑇))‘𝑛) + 0) = (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) |
77 | 76 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (0 =
if(𝑛 = ((2nd
‘(1st ‘𝑇))‘1), 1, 0) → ((((1st
‘(1st ‘𝑇))‘𝑛) + 0) ∈ (0..^𝐾) ↔ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1, 0))
∈ (0..^𝐾))) |
78 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → ((1st
‘(1st ‘𝑇))‘𝑛) = ((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1))) |
79 | 78 | oveq1d 6665 |
. . . . . . . . . . . . 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 3359 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
82 | 81, 2 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
83 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
84 | 4, 82, 83 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1st
‘𝑇) ∈
(((0..^𝐾)
↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
85 | | xp1st 7198 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
86 | | elmapi 7879 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
87 | 84, 85, 86 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
88 | 4, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
89 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚 (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 6127 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
92 | 51, 91 | elab 3350 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
93 | 90, 92 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
94 | | f1of 6137 |
. . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)⟶(1...𝑁)) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)⟶(1...𝑁)) |
96 | | nnuz 11723 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℕ =
(ℤ≥‘1) |
97 | 1, 96 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
98 | | eluzfz1 12348 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑁)) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈ (1...𝑁)) |
100 | 95, 99 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) |
101 | 87, 100 | ffvelrnd 6360 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ (0..^𝐾)) |
102 | | elfzonn0 12512 |
. . . . . . . . . . . . . . 15
⊢
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈
ℕ0) |
103 | | peano2nn0 11333 |
. . . . . . . . . . . . . . 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 12508 |
. . . . . . . . . . . . . . . 16
⊢
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ (0..^𝐾) ↔ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ ℕ0
∧ 𝐾 ∈ ℕ
∧ ((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) < 𝐾)) |
106 | 101, 105 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ ℕ0
∧ 𝐾 ∈ ℕ
∧ ((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) < 𝐾)) |
107 | 106 | simp2d 1074 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ ℕ) |
108 | | elfzolt2 12479 |
. . . . . . . . . . . . . . . . 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 11480 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈
ℤ) |
112 | 107 | nnzd 11481 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈ ℤ) |
113 | | zltp1le 11427 |
. . . . . . . . . . . . . . . . 17
⊢
((((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ ℤ ∧ 𝐾 ∈ ℤ) →
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) < 𝐾 ↔ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ≤ 𝐾)) |
114 | 111, 112,
113 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) < 𝐾 ↔ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ≤ 𝐾)) |
115 | 109, 114 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ≤ 𝐾) |
116 | | fvex 6201 |
. . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇))‘1) ∈ V |
117 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → (𝑛 ∈ (1...𝑁) ↔ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁))) |
118 | 117 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ↔ (𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)))) |
119 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → (𝑝‘𝑛) = (𝑝‘((2nd
‘(1st ‘𝑇))‘1))) |
120 | 119 | neeq1d 2853 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → ((𝑝‘𝑛) ≠ 𝐾 ↔ (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾)) |
121 | 120 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → (∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾 ↔ ∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾)) |
122 | 118, 121 | imbi12d 334 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) ↔ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾))) |
123 | 116, 122,
5 | vtocl 3259 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾) |
124 | 100, 123 | mpdan 702 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾) |
125 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘1))) |
126 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((1st ‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾) → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
127 | 87, 126 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
128 | 127 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
129 | | 1ex 10035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 ∈
V |
130 | | fnconstg 6093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (1 ∈
V → (((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1)))) |
131 | 129, 130 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) |
132 | | c0ex 10034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 0 ∈
V |
133 | | fnconstg 6093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (0 ∈
V → (((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) |
134 | 132, 133 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) |
135 | 131, 134 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∧ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) |
136 | | dff1o3 6143 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡(2nd ‘(1st
‘𝑇)))) |
137 | 136 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡(2nd ‘(1st
‘𝑇))) |
138 | 93, 137 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → Fun ◡(2nd ‘(1st
‘𝑇))) |
139 | | imain 5974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Fun
◡(2nd ‘(1st
‘𝑇)) →
((2nd ‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))) |
140 | 138, 139 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))) |
141 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ ℕ0
→ (𝑦 + 1) ∈
ℕ) |
142 | 8, 141 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℕ) |
143 | 142 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℝ) |
144 | 143 | ltp1d 10954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) < ((𝑦 + 1) + 1)) |
145 | | fzdisj 12368 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑦 + 1) < ((𝑦 + 1) + 1) → ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅) |
146 | 145 | imaeq2d 5466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑦 + 1) < ((𝑦 + 1) + 1) → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ((2nd
‘(1st ‘𝑇)) “ ∅)) |
147 | | ima0 5481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((2nd ‘(1st ‘𝑇)) “ ∅) =
∅ |
148 | 146, 147 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 + 1) < ((𝑦 + 1) + 1) → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ∅) |
149 | 144, 148 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ∅) |
150 | 140, 149 | sylan9req 2677 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅) |
151 | | fnun 5997 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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)...𝑁)))) |
152 | 135, 150,
151 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))) |
153 | | imaundi 5545 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((2nd ‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) |
154 | 142 | peano2nnd 11037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℕ) |
155 | 154, 96 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈
(ℤ≥‘1)) |
156 | 155 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑦 + 1) + 1) ∈
(ℤ≥‘1)) |
157 | 1 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝑁 ∈ ℂ) |
158 | | npcan1 10455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
159 | 157, 158 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
160 | 159 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁) |
161 | | elfzuz3 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑦)) |
162 | | eluzp1p1 11713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 − 1) ∈
(ℤ≥‘𝑦) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑦 + 1))) |
163 | 161, 162 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑦 + 1))) |
164 | 163 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑦 + 1))) |
165 | 160, 164 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ≥‘(𝑦 + 1))) |
166 | | fzsplit2 12366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑦 + 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑦 + 1))) → (1...𝑁) = ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) |
167 | 156, 165,
166 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) = ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) |
168 | 167 | imaeq2d 5466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = ((2nd ‘(1st
‘𝑇)) “
((1...(𝑦 + 1)) ∪
(((𝑦 + 1) + 1)...𝑁)))) |
169 | | f1ofo 6144 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) |
170 | | foima 6120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
171 | 93, 169, 170 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
172 | 171 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
173 | 168, 172 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (1...𝑁)) |
174 | 153, 173 | syl5eqr 2670 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = (1...𝑁)) |
175 | 174 | fneq2d 5982 |
. . . . . . . . . . . . . . . . . . . . . . . . 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...𝑁))) |
176 | 152, 175 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
177 | 49 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) ∈ V) |
178 | | inidm 3822 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
179 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) = ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1))) |
180 | | f1ofn 6138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)) Fn (1...𝑁)) |
181 | 93, 180 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) Fn (1...𝑁)) |
182 | 181 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2nd
‘(1st ‘𝑇)) Fn (1...𝑁)) |
183 | | fzss2 12381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈
(ℤ≥‘(𝑦 + 1)) → (1...(𝑦 + 1)) ⊆ (1...𝑁)) |
184 | 165, 183 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...(𝑦 + 1)) ⊆ (1...𝑁)) |
185 | 142, 96 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈
(ℤ≥‘1)) |
186 | | eluzfz1 12348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑦 + 1) ∈
(ℤ≥‘1) → 1 ∈ (1...(𝑦 + 1))) |
187 | 185, 186 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 1 ∈ (1...(𝑦 + 1))) |
188 | 187 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 1 ∈ (1...(𝑦 + 1))) |
189 | | fnfvima 6496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((2nd ‘(1st ‘𝑇)) Fn (1...𝑁) ∧ (1...(𝑦 + 1)) ⊆ (1...𝑁) ∧ 1 ∈ (1...(𝑦 + 1))) → ((2nd
‘(1st ‘𝑇))‘1) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1)))) |
190 | 182, 184,
188, 189 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑇))‘1) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1)))) |
191 | | fvun1 6269 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 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))) |
192 | 131, 134,
191 | mp3an12 1414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 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))) |
193 | 150, 190,
192 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘1)) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd
‘(1st ‘𝑇))‘1))) |
194 | 129 | fvconst2 6469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((2nd ‘(1st ‘𝑇))‘1) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd
‘(1st ‘𝑇))‘1)) = 1) |
195 | 190, 194 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1})‘((2nd
‘(1st ‘𝑇))‘1)) = 1) |
196 | 193, 195 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘1)) = 1) |
197 | 196 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘1)) = 1) |
198 | 128, 176,
177, 177, 178, 179, 197 | ofval 6906 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) |
199 | 100, 198 | mpidan 704 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) |
200 | 125, 199 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑝 = ((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...(𝑦 + 1))) × {1})
∪ (((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) |
201 | 200 | adantllr 755 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑝 ∈ ran 𝐹) ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑝 = ((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...(𝑦 + 1))) × {1})
∪ (((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) |
202 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
203 | 202 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) |
204 | 203 | ifbid 4108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) |
205 | 204 | csbeq1d 3540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
206 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑡 = 𝑇 → (1st ‘𝑡) = (1st ‘𝑇)) |
207 | 206 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
208 | 206 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) |
209 | 208 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑗))) |
210 | 209 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1})) |
211 | 208 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
212 | 211 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
213 | 210, 212 | uneq12d 3768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑡 = 𝑇 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
214 | 207, 213 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
215 | 214 | csbeq2dv 3992 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
216 | 205, 215 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
217 | 216 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
218 | 217 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
219 | 218, 2 | elrab2 3366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
220 | 219 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
221 | 4, 220 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
222 | 221 | rneqd 5353 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ran 𝐹 = ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
223 | 222 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑝 ∈ ran 𝐹 ↔ 𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
224 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
225 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((1st ‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V |
226 | 225 | csbex 4793 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
⦋if(𝑦
< (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V |
227 | 224, 226 | elrnmpti 5376 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
228 | 223, 227 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑝 ∈ ran 𝐹 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
229 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2nd
‘𝑇) =
0) |
230 | | elfzle1 12344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 0 ≤ 𝑦) |
231 | 230 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 0 ≤ 𝑦) |
232 | 229, 231 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2nd
‘𝑇) ≤ 𝑦) |
233 | | 0re 10040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 0 ∈
ℝ |
234 | 6, 233 | syl6eqel 2709 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (2nd
‘𝑇) ∈
ℝ) |
235 | | lenlt 10116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((2nd ‘𝑇) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((2nd
‘𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd ‘𝑇))) |
236 | 234, 9, 235 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd ‘𝑇))) |
237 | 232, 236 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ¬ 𝑦 < (2nd
‘𝑇)) |
238 | 237 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = (𝑦 + 1)) |
239 | 238 | csbeq1d 3540 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑦 + 1) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
240 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 + 1) ∈ V |
241 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑗 = (𝑦 + 1) → (1...𝑗) = (1...(𝑦 + 1))) |
242 | 241 | imaeq2d 5466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 = (𝑦 + 1) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...(𝑦 +
1)))) |
243 | 242 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 = (𝑦 + 1) → (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1})) |
244 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 = (𝑦 + 1) → (𝑗 + 1) = ((𝑦 + 1) + 1)) |
245 | 244 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑗 = (𝑦 + 1) → ((𝑗 + 1)...𝑁) = (((𝑦 + 1) + 1)...𝑁)) |
246 | 245 | imaeq2d 5466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 = (𝑦 + 1) → ((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) |
247 | 246 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 = (𝑦 + 1) → (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) |
248 | 243, 247 | uneq12d 3768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 = (𝑦 + 1) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) |
249 | 248 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑗 = (𝑦 + 1) → ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) |
250 | 240, 249 | csbie 3559 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
⦋(𝑦 +
1) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) |
251 | 239, 250 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) |
252 | 251 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑝 = ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) ↔ 𝑝 = ((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...(𝑦 + 1))) × {1})
∪ (((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))) |
253 | 252 | rexbidva 3049 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...(𝑦 + 1))) × {1})
∪ (((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))) |
254 | 228, 253 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑝 ∈ ran 𝐹 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...(𝑦 + 1))) × {1})
∪ (((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))) |
255 | 254 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...(𝑦 + 1))) × {1})
∪ (((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) |
256 | 201, 255 | r19.29a 3078 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) |
257 | | eqtr3 2643 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∧ 𝐾 = (((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = 𝐾) |
258 | 257 | ex 450 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) → (𝐾 = (((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = 𝐾)) |
259 | 256, 258 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → (𝐾 = (((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = 𝐾)) |
260 | 259 | necon3d 2815 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → ((𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾 → 𝐾 ≠ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1))) |
261 | 260 | rexlimdva 3031 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾 → 𝐾 ≠ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1))) |
262 | 124, 261 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ≠ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) |
263 | 104 | nn0red 11352 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈
ℝ) |
264 | 107 | nnred 11035 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ ℝ) |
265 | 263, 264 | ltlend 10182 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) < 𝐾 ↔ ((((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ≤ 𝐾 ∧ 𝐾 ≠ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)))) |
266 | 115, 262,
265 | mpbir2and 957 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) < 𝐾) |
267 | | elfzo0 12508 |
. . . . . . . . . . . . . 14
⊢
((((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈ (0..^𝐾) ↔ ((((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈ ℕ0
∧ 𝐾 ∈ ℕ
∧ (((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) < 𝐾)) |
268 | 104, 107,
266, 267 | syl3anbrc 1246 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈ (0..^𝐾)) |
269 | 268 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 = ((2nd ‘(1st
‘𝑇))‘1)) →
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈ (0..^𝐾)) |
270 | 80, 269 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 = ((2nd ‘(1st
‘𝑇))‘1)) →
(((1st ‘(1st ‘𝑇))‘𝑛) + 1) ∈ (0..^𝐾)) |
271 | 270 | adantlr 751 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 = ((2nd ‘(1st
‘𝑇))‘1)) →
(((1st ‘(1st ‘𝑇))‘𝑛) + 1) ∈ (0..^𝐾)) |
272 | 87 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈ (0..^𝐾)) |
273 | | elfzonn0 12512 |
. . . . . . . . . . . . . . 15
⊢
(((1st ‘(1st ‘𝑇))‘𝑛) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈
ℕ0) |
274 | 272, 273 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈
ℕ0) |
275 | 274 | nn0cnd 11353 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈ ℂ) |
276 | 275 | addid1d 10236 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) + 0) = ((1st
‘(1st ‘𝑇))‘𝑛)) |
277 | 276, 272 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) + 0) ∈ (0..^𝐾)) |
278 | 277 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2nd ‘(1st
‘𝑇))‘1)) →
(((1st ‘(1st ‘𝑇))‘𝑛) + 0) ∈ (0..^𝐾)) |
279 | 75, 77, 271, 278 | ifbothda 4123 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1, 0))
∈ (0..^𝐾)) |
280 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) = (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) |
281 | 279, 280 | fmptd 6385 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))):(1...𝑁)⟶(0..^𝐾)) |
282 | | ovex 6678 |
. . . . . . . . 9
⊢
(0..^𝐾) ∈
V |
283 | 282, 49 | elmap 7886 |
. . . . . . . 8
⊢ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∈ ((0..^𝐾)
↑𝑚 (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))):(1...𝑁)⟶(0..^𝐾)) |
284 | 281, 283 | sylibr 224 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∈ ((0..^𝐾)
↑𝑚 (1...𝑁))) |
285 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → 𝑛 ∈ (1...(𝑁 − 1))) |
286 | | 1z 11407 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℤ |
287 | 13, 286 | jctil 560 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 ∈ ℤ ∧
(𝑁 − 1) ∈
ℤ)) |
288 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℤ) |
289 | 288, 286 | jctir 561 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (1...(𝑁 − 1)) → (𝑛 ∈ ℤ ∧ 1 ∈
ℤ)) |
290 | | fzaddel 12375 |
. . . . . . . . . . . . . . . 16
⊢ (((1
∈ ℤ ∧ (𝑁
− 1) ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
→ (𝑛 ∈
(1...(𝑁 − 1)) ↔
(𝑛 + 1) ∈ ((1 +
1)...((𝑁 − 1) +
1)))) |
291 | 287, 289,
290 | syl2an 494 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 ∈ (1...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1)))) |
292 | 285, 291 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1))) |
293 | 159 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 +
1)...𝑁)) |
294 | 293 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 +
1)...𝑁)) |
295 | 292, 294 | eleqtrd 2703 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 + 1) ∈ ((1 + 1)...𝑁)) |
296 | 295 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑛 + 1) ∈ ((1 + 1)...𝑁)) |
297 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → 𝑦 ∈ ((1 + 1)...𝑁)) |
298 | | peano2z 11418 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 ∈
ℤ → (1 + 1) ∈ ℤ) |
299 | 286, 298 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 + 1)
∈ ℤ |
300 | 11, 299 | jctil 560 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1 + 1) ∈ ℤ
∧ 𝑁 ∈
ℤ)) |
301 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ((1 + 1)...𝑁) → 𝑦 ∈ ℤ) |
302 | 301, 286 | jctir 561 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ((1 + 1)...𝑁) → (𝑦 ∈ ℤ ∧ 1 ∈
ℤ)) |
303 | | fzsubel 12377 |
. . . . . . . . . . . . . . . . 17
⊢ ((((1 +
1) ∈ ℤ ∧ 𝑁
∈ ℤ) ∧ (𝑦
∈ ℤ ∧ 1 ∈ ℤ)) → (𝑦 ∈ ((1 + 1)...𝑁) ↔ (𝑦 − 1) ∈ (((1 + 1) −
1)...(𝑁 −
1)))) |
304 | 300, 302,
303 | syl2an 494 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 ∈ ((1 + 1)...𝑁) ↔ (𝑦 − 1) ∈ (((1 + 1) −
1)...(𝑁 −
1)))) |
305 | 297, 304 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 − 1) ∈ (((1 + 1) −
1)...(𝑁 −
1))) |
306 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
307 | 306, 306 | pncan3oi 10297 |
. . . . . . . . . . . . . . . 16
⊢ ((1 + 1)
− 1) = 1 |
308 | 307 | oveq1i 6660 |
. . . . . . . . . . . . . . 15
⊢ (((1 + 1)
− 1)...(𝑁 − 1))
= (1...(𝑁 −
1)) |
309 | 305, 308 | syl6eleq 2711 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 − 1) ∈ (1...(𝑁 − 1))) |
310 | 301 | zcnd 11483 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ((1 + 1)...𝑁) → 𝑦 ∈ ℂ) |
311 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℕ) |
312 | 311 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℂ) |
313 | | subadd2 10285 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℂ ∧ 1 ∈
ℂ ∧ 𝑛 ∈
ℂ) → ((𝑦 −
1) = 𝑛 ↔ (𝑛 + 1) = 𝑦)) |
314 | 306, 313 | mp3an2 1412 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑦 − 1) = 𝑛 ↔ (𝑛 + 1) = 𝑦)) |
315 | 314 | bicomd 213 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑛 + 1) = 𝑦 ↔ (𝑦 − 1) = 𝑛)) |
316 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (𝑛 + 1) ↔ (𝑛 + 1) = 𝑦) |
317 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = (𝑦 − 1) ↔ (𝑦 − 1) = 𝑛) |
318 | 315, 316,
317 | 3bitr4g 303 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) |
319 | 310, 312,
318 | syl2an 494 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ((1 + 1)...𝑁) ∧ 𝑛 ∈ (1...(𝑁 − 1))) → (𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) |
320 | 319 | ralrimiva 2966 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ((1 + 1)...𝑁) → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) |
321 | 320 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) |
322 | | reu6i 3397 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 − 1) ∈ (1...(𝑁 − 1)) ∧ ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) → ∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1)) |
323 | 309, 321,
322 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → ∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1)) |
324 | 323 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑦 ∈ ((1 + 1)...𝑁)∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1)) |
325 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) = (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) |
326 | 325 | f1ompt 6382 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 +
1)...𝑁) ↔
(∀𝑛 ∈
(1...(𝑁 − 1))(𝑛 + 1) ∈ ((1 + 1)...𝑁) ∧ ∀𝑦 ∈ ((1 + 1)...𝑁)∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1))) |
327 | 296, 324,
326 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 +
1)...𝑁)) |
328 | | f1osng 6177 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 1 ∈
V) → {〈𝑁,
1〉}:{𝑁}–1-1-onto→{1}) |
329 | 1, 129, 328 | sylancl 694 |
. . . . . . . . . . 11
⊢ (𝜑 → {〈𝑁, 1〉}:{𝑁}–1-1-onto→{1}) |
330 | 14, 16 | ltnled 10184 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1))) |
331 | 20, 330 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1)) |
332 | | elfzle2 12345 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1)) |
333 | 331, 332 | nsyl 135 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1))) |
334 | | disjsn 4246 |
. . . . . . . . . . . 12
⊢
(((1...(𝑁 −
1)) ∩ {𝑁}) = ∅
↔ ¬ 𝑁 ∈
(1...(𝑁 −
1))) |
335 | 333, 334 | sylibr 224 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅) |
336 | | 1re 10039 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
337 | 336 | ltp1i 10927 |
. . . . . . . . . . . . . . 15
⊢ 1 < (1
+ 1) |
338 | 299 | zrei 11383 |
. . . . . . . . . . . . . . . 16
⊢ (1 + 1)
∈ ℝ |
339 | 336, 338 | ltnlei 10158 |
. . . . . . . . . . . . . . 15
⊢ (1 <
(1 + 1) ↔ ¬ (1 + 1) ≤ 1) |
340 | 337, 339 | mpbi 220 |
. . . . . . . . . . . . . 14
⊢ ¬ (1
+ 1) ≤ 1 |
341 | | elfzle1 12344 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
((1 + 1)...𝑁) → (1 +
1) ≤ 1) |
342 | 340, 341 | mto 188 |
. . . . . . . . . . . . 13
⊢ ¬ 1
∈ ((1 + 1)...𝑁) |
343 | | disjsn 4246 |
. . . . . . . . . . . . 13
⊢ ((((1 +
1)...𝑁) ∩ {1}) =
∅ ↔ ¬ 1 ∈ ((1 + 1)...𝑁)) |
344 | 342, 343 | mpbir 221 |
. . . . . . . . . . . 12
⊢ (((1 +
1)...𝑁) ∩ {1}) =
∅ |
345 | 344 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (((1 + 1)...𝑁) ∩ {1}) =
∅) |
346 | | f1oun 6156 |
. . . . . . . . . . 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})) |
347 | 327, 329,
335, 345, 346 | syl22anc 1327 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {〈𝑁, 1〉}):((1...(𝑁 − 1)) ∪ {𝑁})–1-1-onto→(((1
+ 1)...𝑁) ∪
{1})) |
348 | | elex 3212 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ V) |
349 | 1, 348 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ V) |
350 | 129 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
V) |
351 | 159, 97 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘1)) |
352 | | uzid 11702 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
353 | | peano2uz 11741 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
354 | 13, 352, 353 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
355 | 159, 354 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
356 | | fzsplit2 12366 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
357 | 351, 355,
356 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
358 | 159 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁)) |
359 | | fzsn 12383 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁}) |
360 | 11, 359 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁...𝑁) = {𝑁}) |
361 | 358, 360 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁}) |
362 | 361 | uneq2d 3767 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
363 | 357, 362 | eqtr2d 2657 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁)) |
364 | | iftrue 4092 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑁 → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = 1) |
365 | 364 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = 1) |
366 | 349, 350,
363, 365 | fmptapd 6437 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∪ {〈𝑁, 1〉}) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) |
367 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑁 → (𝑛 ∈ (1...(𝑁 − 1)) ↔ 𝑁 ∈ (1...(𝑁 − 1)))) |
368 | 367 | notbid 308 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑁 → (¬ 𝑛 ∈ (1...(𝑁 − 1)) ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1)))) |
369 | 333, 368 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑛 = 𝑁 → ¬ 𝑛 ∈ (1...(𝑁 − 1)))) |
370 | 369 | necon2ad 2809 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ≠ 𝑁)) |
371 | 370 | imp 445 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → 𝑛 ≠ 𝑁) |
372 | | ifnefalse 4098 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ≠ 𝑁 → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1)) |
373 | 371, 372 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1)) |
374 | 373 | mpteq2dva 4744 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1))) |
375 | 374 | uneq1d 3766 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∪ {〈𝑁, 1〉}) = ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {〈𝑁, 1〉})) |
376 | 366, 375 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {〈𝑁, 1〉})) |
377 | 357, 362 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
378 | | uzid 11702 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℤ → 1 ∈ (ℤ≥‘1)) |
379 | | peano2uz 11741 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
(ℤ≥‘1) → (1 + 1) ∈
(ℤ≥‘1)) |
380 | 286, 378,
379 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ (1 + 1)
∈ (ℤ≥‘1) |
381 | | fzsplit2 12366 |
. . . . . . . . . . . . 13
⊢ (((1 + 1)
∈ (ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘1))
→ (1...𝑁) = ((1...1)
∪ ((1 + 1)...𝑁))) |
382 | 380, 97, 381 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝑁) = ((1...1) ∪ ((1 + 1)...𝑁))) |
383 | | fzsn 12383 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℤ → (1...1) = {1}) |
384 | 286, 383 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (1...1) =
{1} |
385 | 384 | uneq1i 3763 |
. . . . . . . . . . . . 13
⊢ ((1...1)
∪ ((1 + 1)...𝑁)) = ({1}
∪ ((1 + 1)...𝑁)) |
386 | 385 | equncomi 3759 |
. . . . . . . . . . . 12
⊢ ((1...1)
∪ ((1 + 1)...𝑁)) = (((1
+ 1)...𝑁) ∪
{1}) |
387 | 382, 386 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...𝑁) = (((1 + 1)...𝑁) ∪ {1})) |
388 | 376, 377,
387 | f1oeq123d 6133 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {〈𝑁, 1〉}):((1...(𝑁 − 1)) ∪ {𝑁})–1-1-onto→(((1
+ 1)...𝑁) ∪
{1}))) |
389 | 347, 388 | mpbird 247 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁)) |
390 | | f1oco 6159 |
. . . . . . . . 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...𝑁)) |
391 | 93, 389, 390 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁)) |
392 | | f1oeq1 6127 |
. . . . . . . . 9
⊢ (𝑓 = ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁))) |
393 | 53, 392 | elab 3350 |
. . . . . . . 8
⊢
(((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁)) |
394 | 391, 393 | sylibr 224 |
. . . . . . 7
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
395 | | opelxpi 5148 |
. . . . . . 7
⊢ (((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∈ ((0..^𝐾)
↑𝑚 (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..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
396 | 284, 394,
395 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → 〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉 ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
397 | 1 | nnnn0d 11351 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
398 | | nn0fz0 12437 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈ (0...𝑁)) |
399 | 397, 398 | sylib 208 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (0...𝑁)) |
400 | | opelxpi 5148 |
. . . . . 6
⊢
((〈(𝑛 ∈
(1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉 ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ 𝑁 ∈ (0...𝑁)) → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
401 | 396, 399,
400 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
402 | | elrab3t 3362 |
. . . . 5
⊢
((∀𝑡(𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘𝑓 + (((((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..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ∈ {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))))) |
403 | 73, 401, 402 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ∈ {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∘𝑓 + (((((2nd ‘(1st
‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ (1...𝑦)) × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) “ ((𝑦 + 1)...𝑁)) × {0})))))) |
404 | 7, 403 | mpbird 247 |
. . 3
⊢ (𝜑 → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ∈ {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}) |
405 | 404, 2 | syl6eleqr 2712 |
. 2
⊢ (𝜑 → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ∈ 𝑆) |
406 | | fveq2 6191 |
. . . . . . 7
⊢
(〈〈(𝑛
∈ (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 ‘𝑇)) |
407 | 406 | eqeq1d 2624 |
. . . . . 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 ‘𝑇) = 𝑁)) |
408 | 27, 407 | syl5ibcom 235 |
. . . . 5
⊢ (𝜑 → (〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 = 𝑇 → (2nd ‘𝑇) = 𝑁)) |
409 | 1 | nnne0d 11065 |
. . . . . 6
⊢ (𝜑 → 𝑁 ≠ 0) |
410 | | neeq1 2856 |
. . . . . 6
⊢
((2nd ‘𝑇) = 𝑁 → ((2nd ‘𝑇) ≠ 0 ↔ 𝑁 ≠ 0)) |
411 | 409, 410 | syl5ibrcom 237 |
. . . . 5
⊢ (𝜑 → ((2nd
‘𝑇) = 𝑁 → (2nd
‘𝑇) ≠
0)) |
412 | 408, 411 | syld 47 |
. . . 4
⊢ (𝜑 → (〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 = 𝑇 → (2nd ‘𝑇) ≠ 0)) |
413 | 412 | necon2d 2817 |
. . 3
⊢ (𝜑 → ((2nd
‘𝑇) = 0 →
〈〈(𝑛 ∈
(1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ≠ 𝑇)) |
414 | 6, 413 | mpd 15 |
. 2
⊢ (𝜑 → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ≠ 𝑇) |
415 | | neeq1 2856 |
. . 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))))〉, 𝑁〉 ≠ 𝑇)) |
416 | 415 | rspcev 3309 |
. 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))))〉, 𝑁〉 ≠ 𝑇) → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
417 | 405, 414,
416 | syl2anc 693 |
1
⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |