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 37644 | . . . 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 13661 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℕ0) | 
| 9 | 8 | nn0red 12590 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ) | 
| 10 | 9 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ) | 
| 11 | 1 | nnzd 12642 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 12 |  | peano2zm 12662 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) | 
| 13 | 11, 12 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) | 
| 14 | 13 | zred 12724 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) | 
| 15 | 14 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ) | 
| 16 | 1 | nnred 12282 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 17 | 16 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℝ) | 
| 18 |  | elfzle2 13569 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑁 − 1)) | 
| 19 | 18 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ≤ (𝑁 − 1)) | 
| 20 | 16 | ltm1d 12201 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 1) < 𝑁) | 
| 21 | 20 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) < 𝑁) | 
| 22 | 10, 15, 17, 19, 21 | lelttrd 11420 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁) | 
| 23 | 22 | adantlr 715 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁) | 
| 24 |  | fveq2 6905 | . . . . . . . . . . . . . . 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 5468 | . . . . . . . . . . . . . . . 16
⊢
〈(𝑛 ∈
(1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉 ∈ V | 
| 26 |  | op2ndg 8028 | . . . . . . . . . . . . . . . 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 2798 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) → (2nd ‘𝑡) = 𝑁) | 
| 29 | 28 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2nd
‘𝑡) = 𝑁) | 
| 30 | 23, 29 | breqtrrd 5170 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < (2nd ‘𝑡)) | 
| 31 | 30 | iftrued 4532 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 = 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = 𝑦) | 
| 32 | 31 | csbeq1d 3902 | . . . . . . . . . 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 3483 | . . . . . . . . . . . . 13
⊢ 𝑦 ∈ V | 
| 34 |  | oveq2 7440 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑦 → (1...𝑗) = (1...𝑦)) | 
| 35 | 34 | imaeq2d 6077 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑦 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑡)) “
(1...𝑦))) | 
| 36 | 35 | xpeq1d 5713 | . . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑦 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑡)) “ (1...𝑦)) × {1})) | 
| 37 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑦 → (𝑗 + 1) = (𝑦 + 1)) | 
| 38 | 37 | oveq1d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑦 → ((𝑗 + 1)...𝑁) = ((𝑦 + 1)...𝑁)) | 
| 39 | 38 | imaeq2d 6077 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑦 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑡)) “ ((𝑦 + 1)...𝑁))) | 
| 40 | 39 | xpeq1d 5713 | . . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑦 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑡)) “ ((𝑦 + 1)...𝑁)) × {0})) | 
| 41 | 36, 40 | uneq12d 4168 | . . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑦 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑡)) “ (1...𝑦)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑦 + 1)...𝑁)) × {0}))) | 
| 42 | 41 | oveq2d 7448 | . . . . . . . . . . . . 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 3933 | . . . . . . . . . . . 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 6910 | . . . . . . . . . . . . . 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 8027 | . . . . . . . . . . . . . . . . 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 6909 | . . . . . . . . . . . . . . 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 7465 | . . . . . . . . . . . . . . . . 17
⊢
(1...𝑁) ∈
V | 
| 49 | 48 | mptex 7244 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∈ V | 
| 50 |  | fvex 6918 | . . . . . . . . . . . . . . . . 17
⊢
(2nd ‘(1st ‘𝑇)) ∈ V | 
| 51 | 48 | mptex 7244 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∈ V | 
| 52 | 50, 51 | coex 7953 | . . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) ∈ V | 
| 53 | 49, 52 | op1st 8023 | . . . . . . . . . . . . . . 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 | eqtrdi 2792 | . . . . . . . . . . . . . 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 2798 | . . . . . . . . . . . . 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 6905 | . . . . . . . . . . . . . . . . . . 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 2798 | . . . . . . . . . . . . . . . . . 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 6909 | . . . . . . . . . . . . . . . . 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 8024 | . . . . . . . . . . . . . . . . 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 | eqtrdi 2792 | . . . . . . . . . . . . . . . 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 6076 | . . . . . . . . . . . . . . 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 5713 | . . . . . . . . . . . . . 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 6076 | . . . . . . . . . . . . . . 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 5713 | . . . . . . . . . . . . . 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 4168 | . . . . . . . . . . . . 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 7450 | . . . . . . . . . . . 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 | eqtrid 2788 | . . . . . . . . . . 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 480 | . . . . . . . . . 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 2776 | . . . . . . . . 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 5241 | . . . . . . . 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 2747 | . . . . . . 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 412 | . . . . . 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 1926 | . . . . 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 7440 | . . . . . . . . . . 11
⊢ (1 =
if(𝑛 = ((2nd
‘(1st ‘𝑇))‘1), 1, 0) → (((1st
‘(1st ‘𝑇))‘𝑛) + 1) = (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) | 
| 75 | 74 | eleq1d 2825 | . . . . . . . . . 10
⊢ (1 =
if(𝑛 = ((2nd
‘(1st ‘𝑇))‘1), 1, 0) → ((((1st
‘(1st ‘𝑇))‘𝑛) + 1) ∈ (0..^𝐾) ↔ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1, 0))
∈ (0..^𝐾))) | 
| 76 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (0 =
if(𝑛 = ((2nd
‘(1st ‘𝑇))‘1), 1, 0) → (((1st
‘(1st ‘𝑇))‘𝑛) + 0) = (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) | 
| 77 | 76 | eleq1d 2825 | . . . . . . . . . 10
⊢ (0 =
if(𝑛 = ((2nd
‘(1st ‘𝑇))‘1), 1, 0) → ((((1st
‘(1st ‘𝑇))‘𝑛) + 0) ∈ (0..^𝐾) ↔ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1, 0))
∈ (0..^𝐾))) | 
| 78 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → ((1st
‘(1st ‘𝑇))‘𝑛) = ((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1))) | 
| 79 | 78 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → (((1st
‘(1st ‘𝑇))‘𝑛) + 1) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) | 
| 80 | 79 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 = ((2nd ‘(1st
‘𝑇))‘1)) →
(((1st ‘(1st ‘𝑇))‘𝑛) + 1) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) | 
| 81 |  | elrabi 3686 | . . . . . . . . . . . . . . . . . . 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 2858 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) | 
| 83 |  | xp1st 8047 | . . . . . . . . . . . . . . . . . 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 8047 | . . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁))) | 
| 86 |  | elmapi 8890 | . . . . . . . . . . . . . . . . 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 8048 | . . . . . . . . . . . . . . . . . . . 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 6835 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) | 
| 92 | 50, 91 | elab 3678 | . . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) | 
| 93 | 90, 92 | sylib 218 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) | 
| 94 |  | f1of 6847 | . . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)⟶(1...𝑁)) | 
| 95 | 93, 94 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)⟶(1...𝑁)) | 
| 96 |  | nnuz 12922 | . . . . . . . . . . . . . . . . . . 19
⊢ ℕ =
(ℤ≥‘1) | 
| 97 | 1, 96 | eleqtrdi 2850 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) | 
| 98 |  | eluzfz1 13572 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑁)) | 
| 99 | 97, 98 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈ (1...𝑁)) | 
| 100 | 95, 99 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) | 
| 101 | 87, 100 | ffvelcdmd 7104 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ (0..^𝐾)) | 
| 102 |  | elfzonn0 13748 | . . . . . . . . . . . . . . 15
⊢
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈
ℕ0) | 
| 103 |  | peano2nn0 12568 | . . . . . . . . . . . . . . 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 13741 | . . . . . . . . . . . . . . . 16
⊢
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ (0..^𝐾) ↔ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ ℕ0
∧ 𝐾 ∈ ℕ
∧ ((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) < 𝐾)) | 
| 106 | 101, 105 | sylib 218 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ ℕ0
∧ 𝐾 ∈ ℕ
∧ ((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) < 𝐾)) | 
| 107 | 106 | simp2d 1143 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ ℕ) | 
| 108 | 104 | nn0red 12590 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈
ℝ) | 
| 109 | 107 | nnred 12282 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ∈ ℝ) | 
| 110 |  | elfzolt2 13709 | . . . . . . . . . . . . . . . . 17
⊢
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) < 𝐾) | 
| 111 | 101, 110 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) < 𝐾) | 
| 112 | 101, 102 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈
ℕ0) | 
| 113 | 112 | nn0zd 12641 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈
ℤ) | 
| 114 | 107 | nnzd 12642 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈ ℤ) | 
| 115 |  | zltp1le 12669 | . . . . . . . . . . . . . . . . 17
⊢
((((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) ∈ ℤ ∧ 𝐾 ∈ ℤ) →
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) < 𝐾 ↔ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ≤ 𝐾)) | 
| 116 | 113, 114,
115 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) < 𝐾 ↔ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ≤ 𝐾)) | 
| 117 | 111, 116 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ≤ 𝐾) | 
| 118 |  | fvex 6918 | . . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇))‘1) ∈ V | 
| 119 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → (𝑛 ∈ (1...𝑁) ↔ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁))) | 
| 120 | 119 | anbi2d 630 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ↔ (𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)))) | 
| 121 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → (𝑝‘𝑛) = (𝑝‘((2nd
‘(1st ‘𝑇))‘1))) | 
| 122 | 121 | neeq1d 2999 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → ((𝑝‘𝑛) ≠ 𝐾 ↔ (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾)) | 
| 123 | 122 | rexbidv 3178 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → (∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾 ↔ ∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾)) | 
| 124 | 120, 123 | imbi12d 344 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘1) → (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) ↔ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾))) | 
| 125 | 118, 124,
5 | vtocl 3557 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾) | 
| 126 | 100, 125 | mpdan 687 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾) | 
| 127 |  | fveq1 6904 | . . . . . . . . . . . . . . . . . . . . . 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))) | 
| 128 | 87 | ffnd 6736 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) | 
| 129 | 128 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) | 
| 130 |  | 1ex 11258 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 ∈
V | 
| 131 |  | fnconstg 6795 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (1 ∈
V → (((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1)))) | 
| 132 | 130, 131 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) | 
| 133 |  | c0ex 11256 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 0 ∈
V | 
| 134 |  | fnconstg 6795 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (0 ∈
V → (((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) | 
| 135 | 133, 134 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) | 
| 136 | 132, 135 | pm3.2i 470 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∧ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) | 
| 137 |  | dff1o3 6853 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡(2nd ‘(1st
‘𝑇)))) | 
| 138 | 137 | simprbi 496 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡(2nd ‘(1st
‘𝑇))) | 
| 139 |  | imain 6650 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Fun
◡(2nd ‘(1st
‘𝑇)) →
((2nd ‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))) | 
| 140 | 93, 138, 139 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))) | 
| 141 |  | nn0p1nn 12567 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ ℕ0
→ (𝑦 + 1) ∈
ℕ) | 
| 142 | 8, 141 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℕ) | 
| 143 | 142 | nnred 12282 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ ℝ) | 
| 144 | 143 | ltp1d 12199 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) < ((𝑦 + 1) + 1)) | 
| 145 |  | fzdisj 13592 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑦 + 1) < ((𝑦 + 1) + 1) → ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁)) = ∅) | 
| 146 | 145 | imaeq2d 6077 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑦 + 1) < ((𝑦 + 1) + 1) → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∩ (((𝑦 + 1) + 1)...𝑁))) = ((2nd
‘(1st ‘𝑇)) “ ∅)) | 
| 147 |  | ima0 6094 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((2nd ‘(1st ‘𝑇)) “ ∅) =
∅ | 
| 148 | 146, 147 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2797 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = ∅) | 
| 151 |  | fnun 6681 | . . . . . . . . . . . . . . . . . . . . . . . . . 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 | 136, 150,
151 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)))) | 
| 153 |  | imaundi 6168 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((2nd ‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) | 
| 154 | 142 | peano2nnd 12284 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈ ℕ) | 
| 155 | 154, 96 | eleqtrdi 2850 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑦 + 1) + 1) ∈
(ℤ≥‘1)) | 
| 156 | 1 | nncnd 12283 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 157 |  | npcan1 11689 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) | 
| 158 | 156, 157 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) | 
| 159 | 158 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁) | 
| 160 |  | elfzuz3 13562 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑦)) | 
| 161 |  | eluzp1p1 12907 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 − 1) ∈
(ℤ≥‘𝑦) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑦 + 1))) | 
| 162 | 160, 161 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑦 + 1))) | 
| 163 | 162 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑦 + 1))) | 
| 164 | 159, 163 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ≥‘(𝑦 + 1))) | 
| 165 |  | fzsplit2 13590 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑦 + 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑦 + 1))) → (1...𝑁) = ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) | 
| 166 | 155, 164,
165 | syl2an2 686 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...𝑁) = ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) | 
| 167 | 166 | imaeq2d 6077 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = ((2nd ‘(1st
‘𝑇)) “
((1...(𝑦 + 1)) ∪
(((𝑦 + 1) + 1)...𝑁)))) | 
| 168 |  | f1ofo 6854 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) | 
| 169 |  | foima 6824 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) | 
| 170 | 93, 168, 169 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) | 
| 171 | 170 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) | 
| 172 | 167, 171 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑦 + 1)) ∪ (((𝑦 + 1) + 1)...𝑁))) = (1...𝑁)) | 
| 173 | 153, 172 | eqtr3id 2790 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) = (1...𝑁)) | 
| 174 | 173 | fneq2d 6661 | . . . . . . . . . . . . . . . . . . . . . . . . 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 | 152, 174 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . . . 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 4226 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) | 
| 178 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) = ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1))) | 
| 179 |  | f1ofn 6848 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2nd
‘(1st ‘𝑇)) Fn (1...𝑁)) | 
| 182 |  | fzss2 13605 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈
(ℤ≥‘(𝑦 + 1)) → (1...(𝑦 + 1)) ⊆ (1...𝑁)) | 
| 183 | 164, 182 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (1...(𝑦 + 1)) ⊆ (1...𝑁)) | 
| 184 | 142, 96 | eleqtrdi 2850 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈
(ℤ≥‘1)) | 
| 185 |  | eluzfz1 13572 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑦 + 1) ∈
(ℤ≥‘1) → 1 ∈ (1...(𝑦 + 1))) | 
| 186 | 184, 185 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 1 ∈ (1...(𝑦 + 1))) | 
| 187 | 186 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 1 ∈ (1...(𝑦 + 1))) | 
| 188 |  | fnfvima 7254 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((2nd ‘(1st ‘𝑇)) Fn (1...𝑁) ∧ (1...(𝑦 + 1)) ⊆ (1...𝑁) ∧ 1 ∈ (1...(𝑦 + 1))) → ((2nd
‘(1st ‘𝑇))‘1) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1)))) | 
| 189 | 181, 183,
187, 188 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑇))‘1) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1)))) | 
| 190 |  | fvun1 6999 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 | 132, 135,
190 | mp3an12 1452 | . . . . . . . . . . . . . . . . . . . . . . . . . . 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 | 150, 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 | 130 | fvconst2 7225 | . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2776 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘1)) = 1) | 
| 196 | 195 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ ((2nd
‘(1st ‘𝑇))‘1) ∈ (1...𝑁)) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘1)) = 1) | 
| 197 | 129, 175,
176, 176, 177, 178, 196 | ofval 7709 | . . . . . . . . . . . . . . . . . . . . . . 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 689 | . . . . . . . . . . . . . . . . . . . . . 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 | 127, 198 | sylan9eqr 2798 | . . . . . . . . . . . . . . . . . . . . 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 719 | . . . . . . . . . . . . . . . . . . . 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 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) | 
| 202 | 201 | breq2d 5154 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) | 
| 203 | 202 | ifbid 4548 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) | 
| 204 |  | 2fveq3 6910 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) | 
| 205 |  | 2fveq3 6910 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) | 
| 206 | 205 | imaeq1d 6076 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑗))) | 
| 207 | 206 | xpeq1d 5713 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1})) | 
| 208 | 205 | imaeq1d 6076 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑗 + 1)...𝑁))) | 
| 209 | 208 | xpeq1d 5713 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) | 
| 210 | 207, 209 | uneq12d 4168 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑡 = 𝑇 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) | 
| 211 | 204, 210 | oveq12d 7450 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) | 
| 212 | 203, 211 | csbeq12dv 3907 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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})))) | 
| 213 | 212 | mpteq2dv 5243 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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}))))) | 
| 214 | 213 | eqeq2d 2747 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 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})))))) | 
| 215 | 214, 2 | elrab2 3694 | . . . . . . . . . . . . . . . . . . . . . . . . . . 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})))))) | 
| 216 | 215 | simprbi 496 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) | 
| 217 | 4, 216 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) | 
| 218 | 217 | rneqd 5948 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ran 𝐹 = ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) | 
| 219 | 218 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑝 ∈ ran 𝐹 ↔ 𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) | 
| 220 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . . 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})))) | 
| 221 |  | ovex 7465 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((1st ‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V | 
| 222 | 221 | csbex 5310 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
⦋if(𝑦
< (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V | 
| 223 | 220, 222 | elrnmpti 5972 | . . . . . . . . . . . . . . . . . . . . . . 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})))) | 
| 224 | 219, 223 | bitrdi 287 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑝 ∈ ran 𝐹 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) | 
| 225 | 6 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2nd
‘𝑇) =
0) | 
| 226 |  | elfzle1 13568 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 0 ≤ 𝑦) | 
| 227 | 226 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 0 ≤ 𝑦) | 
| 228 | 225, 227 | eqbrtrd 5164 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (2nd
‘𝑇) ≤ 𝑦) | 
| 229 |  | 0re 11264 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 0 ∈
ℝ | 
| 230 | 6, 229 | eqeltrdi 2848 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (2nd
‘𝑇) ∈
ℝ) | 
| 231 |  | lenlt 11340 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((2nd ‘𝑇) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((2nd
‘𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd ‘𝑇))) | 
| 232 | 230, 9, 231 | syl2an 596 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((2nd
‘𝑇) ≤ 𝑦 ↔ ¬ 𝑦 < (2nd ‘𝑇))) | 
| 233 | 228, 232 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ¬ 𝑦 < (2nd
‘𝑇)) | 
| 234 | 233 | iffalsed 4535 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = (𝑦 + 1)) | 
| 235 | 234 | csbeq1d 3902 | . . . . . . . . . . . . . . . . . . . . . . . . 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})))) | 
| 236 |  | ovex 7465 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 + 1) ∈ V | 
| 237 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑗 = (𝑦 + 1) → (1...𝑗) = (1...(𝑦 + 1))) | 
| 238 | 237 | imaeq2d 6077 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 = (𝑦 + 1) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...(𝑦 +
1)))) | 
| 239 | 238 | xpeq1d 5713 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 = (𝑦 + 1) → (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1})) | 
| 240 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 = (𝑦 + 1) → (𝑗 + 1) = ((𝑦 + 1) + 1)) | 
| 241 | 240 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑗 = (𝑦 + 1) → ((𝑗 + 1)...𝑁) = (((𝑦 + 1) + 1)...𝑁)) | 
| 242 | 241 | imaeq2d 6077 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 = (𝑦 + 1) → ((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁))) | 
| 243 | 242 | xpeq1d 5713 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 = (𝑦 + 1) → (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})) | 
| 244 | 239, 243 | uneq12d 4168 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 = (𝑦 + 1) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))) | 
| 245 | 244 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . . . . . 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})))) | 
| 246 | 236, 245 | csbie 3933 | . . . . . . . . . . . . . . . . . . . . . . . . 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}))) | 
| 247 | 235, 246 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . . . 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})))) | 
| 248 | 247 | eqeq2d 2747 | . . . . . . . . . . . . . . . . . . . . . . 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}))))) | 
| 249 | 248 | rexbidva 3176 | . . . . . . . . . . . . . . . . . . . . . 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}))))) | 
| 250 | 224, 249 | bitrd 279 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑝 ∈ ran 𝐹 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ((1st ‘(1st
‘𝑇))
∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0}))))) | 
| 251 | 250 | biimpa 476 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → ∃𝑦 ∈ (0...(𝑁 − 1))𝑝 = ((1st ‘(1st
‘𝑇))
∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...(𝑦 + 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (((𝑦 + 1) + 1)...𝑁)) × {0})))) | 
| 252 | 200, 251 | r19.29a 3161 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) | 
| 253 |  | eqtr3 2762 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∧ 𝐾 = (((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = 𝐾) | 
| 254 | 253 | ex 412 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) → (𝐾 = (((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = 𝐾)) | 
| 255 | 252, 254 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → (𝐾 = (((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) → (𝑝‘((2nd
‘(1st ‘𝑇))‘1)) = 𝐾)) | 
| 256 | 255 | necon3d 2960 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ ran 𝐹) → ((𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾 → 𝐾 ≠ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1))) | 
| 257 | 256 | rexlimdva 3154 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∃𝑝 ∈ ran 𝐹(𝑝‘((2nd
‘(1st ‘𝑇))‘1)) ≠ 𝐾 → 𝐾 ≠ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1))) | 
| 258 | 126, 257 | mpd 15 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ≠ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1)) | 
| 259 | 108, 109,
117, 258 | leneltd 11416 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) < 𝐾) | 
| 260 |  | elfzo0 13741 | . . . . . . . . . . . . . 14
⊢
((((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈ (0..^𝐾) ↔ ((((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈ ℕ0
∧ 𝐾 ∈ ℕ
∧ (((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) < 𝐾)) | 
| 261 | 104, 107,
259, 260 | syl3anbrc 1343 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈ (0..^𝐾)) | 
| 262 | 261 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 = ((2nd ‘(1st
‘𝑇))‘1)) →
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘1)) + 1) ∈ (0..^𝐾)) | 
| 263 | 80, 262 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 = ((2nd ‘(1st
‘𝑇))‘1)) →
(((1st ‘(1st ‘𝑇))‘𝑛) + 1) ∈ (0..^𝐾)) | 
| 264 | 263 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 = ((2nd ‘(1st
‘𝑇))‘1)) →
(((1st ‘(1st ‘𝑇))‘𝑛) + 1) ∈ (0..^𝐾)) | 
| 265 | 87 | ffvelcdmda 7103 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈ (0..^𝐾)) | 
| 266 |  | elfzonn0 13748 | . . . . . . . . . . . . . . 15
⊢
(((1st ‘(1st ‘𝑇))‘𝑛) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈
ℕ0) | 
| 267 | 265, 266 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈
ℕ0) | 
| 268 | 267 | nn0cnd 12591 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈ ℂ) | 
| 269 | 268 | addridd 11462 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) + 0) = ((1st
‘(1st ‘𝑇))‘𝑛)) | 
| 270 | 269, 265 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) + 0) ∈ (0..^𝐾)) | 
| 271 | 270 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ ¬ 𝑛 = ((2nd ‘(1st
‘𝑇))‘1)) →
(((1st ‘(1st ‘𝑇))‘𝑛) + 0) ∈ (0..^𝐾)) | 
| 272 | 75, 77, 264, 271 | ifbothda 4563 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1, 0))
∈ (0..^𝐾)) | 
| 273 | 272 | fmpttd 7134 | . . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))):(1...𝑁)⟶(0..^𝐾)) | 
| 274 |  | ovex 7465 | . . . . . . . . 9
⊢
(0..^𝐾) ∈
V | 
| 275 | 274, 48 | elmap 8912 | . . . . . . . 8
⊢ ((𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∈ ((0..^𝐾)
↑m (1...𝑁))
↔ (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))):(1...𝑁)⟶(0..^𝐾)) | 
| 276 | 273, 275 | sylibr 234 | . . . . . . 7
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))) ∈ ((0..^𝐾)
↑m (1...𝑁))) | 
| 277 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → 𝑛 ∈ (1...(𝑁 − 1))) | 
| 278 |  | 1z 12649 | . . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℤ | 
| 279 | 13, 278 | jctil 519 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 ∈ ℤ ∧
(𝑁 − 1) ∈
ℤ)) | 
| 280 |  | elfzelz 13565 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℤ) | 
| 281 | 280, 278 | jctir 520 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (1...(𝑁 − 1)) → (𝑛 ∈ ℤ ∧ 1 ∈
ℤ)) | 
| 282 |  | fzaddel 13599 | . . . . . . . . . . . . . . . 16
⊢ (((1
∈ ℤ ∧ (𝑁
− 1) ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 1 ∈ ℤ))
→ (𝑛 ∈
(1...(𝑁 − 1)) ↔
(𝑛 + 1) ∈ ((1 +
1)...((𝑁 − 1) +
1)))) | 
| 283 | 279, 281,
282 | syl2an 596 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 ∈ (1...(𝑁 − 1)) ↔ (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1)))) | 
| 284 | 277, 283 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 + 1) ∈ ((1 + 1)...((𝑁 − 1) + 1))) | 
| 285 | 158 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 +
1)...𝑁)) | 
| 286 | 285 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → ((1 + 1)...((𝑁 − 1) + 1)) = ((1 +
1)...𝑁)) | 
| 287 | 284, 286 | eleqtrd 2842 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → (𝑛 + 1) ∈ ((1 + 1)...𝑁)) | 
| 288 | 287 | ralrimiva 3145 | . . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑛 + 1) ∈ ((1 + 1)...𝑁)) | 
| 289 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → 𝑦 ∈ ((1 + 1)...𝑁)) | 
| 290 |  | peano2z 12660 | . . . . . . . . . . . . . . . . . . 19
⊢ (1 ∈
ℤ → (1 + 1) ∈ ℤ) | 
| 291 | 278, 290 | ax-mp 5 | . . . . . . . . . . . . . . . . . 18
⊢ (1 + 1)
∈ ℤ | 
| 292 | 11, 291 | jctil 519 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1 + 1) ∈ ℤ
∧ 𝑁 ∈
ℤ)) | 
| 293 |  | elfzelz 13565 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ((1 + 1)...𝑁) → 𝑦 ∈ ℤ) | 
| 294 | 293, 278 | jctir 520 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ((1 + 1)...𝑁) → (𝑦 ∈ ℤ ∧ 1 ∈
ℤ)) | 
| 295 |  | fzsubel 13601 | . . . . . . . . . . . . . . . . 17
⊢ ((((1 +
1) ∈ ℤ ∧ 𝑁
∈ ℤ) ∧ (𝑦
∈ ℤ ∧ 1 ∈ ℤ)) → (𝑦 ∈ ((1 + 1)...𝑁) ↔ (𝑦 − 1) ∈ (((1 + 1) −
1)...(𝑁 −
1)))) | 
| 296 | 292, 294,
295 | syl2an 596 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 ∈ ((1 + 1)...𝑁) ↔ (𝑦 − 1) ∈ (((1 + 1) −
1)...(𝑁 −
1)))) | 
| 297 | 289, 296 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 − 1) ∈ (((1 + 1) −
1)...(𝑁 −
1))) | 
| 298 |  | ax-1cn 11214 | . . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ | 
| 299 | 298, 298 | pncan3oi 11525 | . . . . . . . . . . . . . . . 16
⊢ ((1 + 1)
− 1) = 1 | 
| 300 | 299 | oveq1i 7442 | . . . . . . . . . . . . . . 15
⊢ (((1 + 1)
− 1)...(𝑁 − 1))
= (1...(𝑁 −
1)) | 
| 301 | 297, 300 | eleqtrdi 2850 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → (𝑦 − 1) ∈ (1...(𝑁 − 1))) | 
| 302 | 293 | zcnd 12725 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ((1 + 1)...𝑁) → 𝑦 ∈ ℂ) | 
| 303 |  | elfznn 13594 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℕ) | 
| 304 | 303 | nncnd 12283 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ ℂ) | 
| 305 |  | subadd2 11513 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℂ ∧ 1 ∈
ℂ ∧ 𝑛 ∈
ℂ) → ((𝑦 −
1) = 𝑛 ↔ (𝑛 + 1) = 𝑦)) | 
| 306 | 298, 305 | mp3an2 1450 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑦 − 1) = 𝑛 ↔ (𝑛 + 1) = 𝑦)) | 
| 307 | 306 | bicomd 223 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑛 + 1) = 𝑦 ↔ (𝑦 − 1) = 𝑛)) | 
| 308 |  | eqcom 2743 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (𝑛 + 1) ↔ (𝑛 + 1) = 𝑦) | 
| 309 |  | eqcom 2743 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = (𝑦 − 1) ↔ (𝑦 − 1) = 𝑛) | 
| 310 | 307, 308,
309 | 3bitr4g 314 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) | 
| 311 | 302, 304,
310 | syl2an 596 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ((1 + 1)...𝑁) ∧ 𝑛 ∈ (1...(𝑁 − 1))) → (𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) | 
| 312 | 311 | ralrimiva 3145 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ((1 + 1)...𝑁) → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) | 
| 313 | 312 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) | 
| 314 |  | reu6i 3733 | . . . . . . . . . . . . . 14
⊢ (((𝑦 − 1) ∈ (1...(𝑁 − 1)) ∧ ∀𝑛 ∈ (1...(𝑁 − 1))(𝑦 = (𝑛 + 1) ↔ 𝑛 = (𝑦 − 1))) → ∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1)) | 
| 315 | 301, 313,
314 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((1 + 1)...𝑁)) → ∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1)) | 
| 316 | 315 | ralrimiva 3145 | . . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑦 ∈ ((1 + 1)...𝑁)∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1)) | 
| 317 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) = (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) | 
| 318 | 317 | f1ompt 7130 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 +
1)...𝑁) ↔
(∀𝑛 ∈
(1...(𝑁 − 1))(𝑛 + 1) ∈ ((1 + 1)...𝑁) ∧ ∀𝑦 ∈ ((1 + 1)...𝑁)∃!𝑛 ∈ (1...(𝑁 − 1))𝑦 = (𝑛 + 1))) | 
| 319 | 288, 316,
318 | sylanbrc 583 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)):(1...(𝑁 − 1))–1-1-onto→((1 +
1)...𝑁)) | 
| 320 |  | f1osng 6888 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 1 ∈
V) → {〈𝑁,
1〉}:{𝑁}–1-1-onto→{1}) | 
| 321 | 1, 130, 320 | sylancl 586 | . . . . . . . . . . 11
⊢ (𝜑 → {〈𝑁, 1〉}:{𝑁}–1-1-onto→{1}) | 
| 322 | 14, 16 | ltnled 11409 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1))) | 
| 323 | 20, 322 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1)) | 
| 324 |  | elfzle2 13569 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1)) | 
| 325 | 323, 324 | nsyl 140 | . . . . . . . . . . . 12
⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1))) | 
| 326 |  | disjsn 4710 | . . . . . . . . . . . 12
⊢
(((1...(𝑁 −
1)) ∩ {𝑁}) = ∅
↔ ¬ 𝑁 ∈
(1...(𝑁 −
1))) | 
| 327 | 325, 326 | sylibr 234 | . . . . . . . . . . 11
⊢ (𝜑 → ((1...(𝑁 − 1)) ∩ {𝑁}) = ∅) | 
| 328 |  | 1re 11262 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ | 
| 329 | 328 | ltp1i 12173 | . . . . . . . . . . . . . . 15
⊢ 1 < (1
+ 1) | 
| 330 | 291 | zrei 12621 | . . . . . . . . . . . . . . . 16
⊢ (1 + 1)
∈ ℝ | 
| 331 | 328, 330 | ltnlei 11383 | . . . . . . . . . . . . . . 15
⊢ (1 <
(1 + 1) ↔ ¬ (1 + 1) ≤ 1) | 
| 332 | 329, 331 | mpbi 230 | . . . . . . . . . . . . . 14
⊢  ¬ (1
+ 1) ≤ 1 | 
| 333 |  | elfzle1 13568 | . . . . . . . . . . . . . 14
⊢ (1 ∈
((1 + 1)...𝑁) → (1 +
1) ≤ 1) | 
| 334 | 332, 333 | mto 197 | . . . . . . . . . . . . 13
⊢  ¬ 1
∈ ((1 + 1)...𝑁) | 
| 335 |  | disjsn 4710 | . . . . . . . . . . . . 13
⊢ ((((1 +
1)...𝑁) ∩ {1}) =
∅ ↔ ¬ 1 ∈ ((1 + 1)...𝑁)) | 
| 336 | 334, 335 | mpbir 231 | . . . . . . . . . . . 12
⊢ (((1 +
1)...𝑁) ∩ {1}) =
∅ | 
| 337 | 336 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → (((1 + 1)...𝑁) ∩ {1}) =
∅) | 
| 338 |  | f1oun 6866 | . . . . . . . . . . 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})) | 
| 339 | 319, 321,
327, 337, 338 | syl22anc 838 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {〈𝑁, 1〉}):((1...(𝑁 − 1)) ∪ {𝑁})–1-1-onto→(((1
+ 1)...𝑁) ∪
{1})) | 
| 340 | 130 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
V) | 
| 341 | 158, 97 | eqeltrd 2840 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘1)) | 
| 342 |  | uzid 12894 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) | 
| 343 |  | peano2uz 12944 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) | 
| 344 | 13, 342, 343 | 3syl 18 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) | 
| 345 | 158, 344 | eqeltrrd 2841 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) | 
| 346 |  | fzsplit2 13590 | . . . . . . . . . . . . . . 15
⊢ ((((𝑁 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) | 
| 347 | 341, 345,
346 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) | 
| 348 | 158 | oveq1d 7447 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁)) | 
| 349 |  | fzsn 13607 | . . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁}) | 
| 350 | 11, 349 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁...𝑁) = {𝑁}) | 
| 351 | 348, 350 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁}) | 
| 352 | 351 | uneq2d 4167 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁})) | 
| 353 | 347, 352 | eqtr2d 2777 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁)) | 
| 354 |  | iftrue 4530 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑁 → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = 1) | 
| 355 | 354 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = 1) | 
| 356 | 1, 340, 353, 355 | fmptapd 7192 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∪ {〈𝑁, 1〉}) = (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) | 
| 357 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑁 → (𝑛 ∈ (1...(𝑁 − 1)) ↔ 𝑁 ∈ (1...(𝑁 − 1)))) | 
| 358 | 357 | notbid 318 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑁 → (¬ 𝑛 ∈ (1...(𝑁 − 1)) ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1)))) | 
| 359 | 325, 358 | syl5ibrcom 247 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑛 = 𝑁 → ¬ 𝑛 ∈ (1...(𝑁 − 1)))) | 
| 360 | 359 | necon2ad 2954 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ≠ 𝑁)) | 
| 361 | 360 | imp 406 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → 𝑛 ≠ 𝑁) | 
| 362 |  | ifnefalse 4536 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ≠ 𝑁 → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1)) | 
| 363 | 361, 362 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(𝑁 − 1))) → if(𝑛 = 𝑁, 1, (𝑛 + 1)) = (𝑛 + 1)) | 
| 364 | 363 | mpteq2dva 5241 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = (𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1))) | 
| 365 | 364 | uneq1d 4166 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑛 ∈ (1...(𝑁 − 1)) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) ∪ {〈𝑁, 1〉}) = ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {〈𝑁, 1〉})) | 
| 366 | 356, 365 | eqtr3d 2778 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))) = ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {〈𝑁, 1〉})) | 
| 367 | 347, 352 | eqtrd 2776 | . . . . . . . . . . 11
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁})) | 
| 368 |  | uzid 12894 | . . . . . . . . . . . . . 14
⊢ (1 ∈
ℤ → 1 ∈ (ℤ≥‘1)) | 
| 369 |  | peano2uz 12944 | . . . . . . . . . . . . . 14
⊢ (1 ∈
(ℤ≥‘1) → (1 + 1) ∈
(ℤ≥‘1)) | 
| 370 | 278, 368,
369 | mp2b 10 | . . . . . . . . . . . . 13
⊢ (1 + 1)
∈ (ℤ≥‘1) | 
| 371 |  | fzsplit2 13590 | . . . . . . . . . . . . 13
⊢ (((1 + 1)
∈ (ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘1))
→ (1...𝑁) = ((1...1)
∪ ((1 + 1)...𝑁))) | 
| 372 | 370, 97, 371 | sylancr 587 | . . . . . . . . . . . 12
⊢ (𝜑 → (1...𝑁) = ((1...1) ∪ ((1 + 1)...𝑁))) | 
| 373 |  | fzsn 13607 | . . . . . . . . . . . . . . 15
⊢ (1 ∈
ℤ → (1...1) = {1}) | 
| 374 | 278, 373 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢ (1...1) =
{1} | 
| 375 | 374 | uneq1i 4163 | . . . . . . . . . . . . 13
⊢ ((1...1)
∪ ((1 + 1)...𝑁)) = ({1}
∪ ((1 + 1)...𝑁)) | 
| 376 | 375 | equncomi 4159 | . . . . . . . . . . . 12
⊢ ((1...1)
∪ ((1 + 1)...𝑁)) = (((1
+ 1)...𝑁) ∪
{1}) | 
| 377 | 372, 376 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (𝜑 → (1...𝑁) = (((1 + 1)...𝑁) ∪ {1})) | 
| 378 | 366, 367,
377 | f1oeq123d 6841 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ↦ (𝑛 + 1)) ∪ {〈𝑁, 1〉}):((1...(𝑁 − 1)) ∪ {𝑁})–1-1-onto→(((1
+ 1)...𝑁) ∪
{1}))) | 
| 379 | 339, 378 | mpbird 257 | . . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))):(1...𝑁)–1-1-onto→(1...𝑁)) | 
| 380 |  | f1oco 6870 | . . . . . . . . 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...𝑁)) | 
| 381 | 93, 379, 380 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁)) | 
| 382 |  | f1oeq1 6835 | . . . . . . . . 9
⊢ (𝑓 = ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁))) | 
| 383 | 52, 382 | elab 3678 | . . . . . . . 8
⊢
(((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))):(1...𝑁)–1-1-onto→(1...𝑁)) | 
| 384 | 381, 383 | sylibr 234 | . . . . . . 7
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1)))) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) | 
| 385 | 276, 384 | opelxpd 5723 | . . . . . 6
⊢ (𝜑 → 〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉 ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) | 
| 386 | 1 | nnnn0d 12589 | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 387 |  | nn0fz0 13666 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈ (0...𝑁)) | 
| 388 | 386, 387 | sylib 218 | . . . . . 6
⊢ (𝜑 → 𝑁 ∈ (0...𝑁)) | 
| 389 | 385, 388 | opelxpd 5723 | . . . . 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...𝑁))) | 
| 390 |  | elrab3t 3690 | . . . . 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})))))) | 
| 391 | 73, 389, 390 | 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})))))) | 
| 392 | 7, 391 | mpbird 257 | . . 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}))))}) | 
| 393 | 392, 2 | eleqtrrdi 2851 | . 2
⊢ (𝜑 → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ∈ 𝑆) | 
| 394 |  | fveqeq2 6914 | . . . . . 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 ‘𝑇) = 𝑁)) | 
| 395 | 27, 394 | syl5ibcom 245 | . . . . 5
⊢ (𝜑 → (〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 = 𝑇 → (2nd ‘𝑇) = 𝑁)) | 
| 396 | 1 | nnne0d 12317 | . . . . . 6
⊢ (𝜑 → 𝑁 ≠ 0) | 
| 397 |  | neeq1 3002 | . . . . . 6
⊢
((2nd ‘𝑇) = 𝑁 → ((2nd ‘𝑇) ≠ 0 ↔ 𝑁 ≠ 0)) | 
| 398 | 396, 397 | syl5ibrcom 247 | . . . . 5
⊢ (𝜑 → ((2nd
‘𝑇) = 𝑁 → (2nd
‘𝑇) ≠
0)) | 
| 399 | 395, 398 | syld 47 | . . . 4
⊢ (𝜑 → (〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 = 𝑇 → (2nd ‘𝑇) ≠ 0)) | 
| 400 | 399 | necon2d 2962 | . . 3
⊢ (𝜑 → ((2nd
‘𝑇) = 0 →
〈〈(𝑛 ∈
(1...𝑁) ↦
(((1st ‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ≠ 𝑇)) | 
| 401 | 6, 400 | mpd 15 | . 2
⊢ (𝜑 → 〈〈(𝑛 ∈ (1...𝑁) ↦ (((1st
‘(1st ‘𝑇))‘𝑛) + if(𝑛 = ((2nd ‘(1st
‘𝑇))‘1), 1,
0))), ((2nd ‘(1st ‘𝑇)) ∘ (𝑛 ∈ (1...𝑁) ↦ if(𝑛 = 𝑁, 1, (𝑛 + 1))))〉, 𝑁〉 ≠ 𝑇) | 
| 402 |  | neeq1 3002 | . . 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))))〉, 𝑁〉 ≠ 𝑇)) | 
| 403 | 402 | rspcev 3621 | . 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))))〉, 𝑁〉 ≠ 𝑇) → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) | 
| 404 | 393, 401,
403 | syl2anc 584 | 1
⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |