Proof of Theorem poimirlem22
| Step | Hyp | Ref
| Expression |
| 1 | | poimir.0 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 2 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝑁 ∈
ℕ) |
| 3 | | poimirlem22.s |
. . . 4
⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
| 4 | | poimirlem22.1 |
. . . . 5
⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) |
| 5 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) |
| 6 | | poimirlem22.2 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
| 7 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝑇 ∈ 𝑆) |
| 8 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2nd ‘𝑇)
∈ (1...(𝑁 −
1))) |
| 9 | 2, 3, 5, 7, 8 | poimirlem15 37642 |
. . 3
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
〈〈(1st ‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉,
(2nd ‘𝑇)〉 ∈ 𝑆) |
| 10 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
| 11 | 10 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) |
| 12 | 11 | ifbid 4549 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) |
| 13 | 12 | csbeq1d 3903 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑇 → ⦋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})))) |
| 14 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
| 15 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) |
| 16 | 15 | imaeq1d 6077 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑗))) |
| 17 | 16 | xpeq1d 5714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1})) |
| 18 | 15 | imaeq1d 6077 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
| 19 | 18 | xpeq1d 5714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
| 20 | 17, 19 | uneq12d 4169 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑇 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
| 21 | 14, 20 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
| 22 | 21 | csbeq2dv 3906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑇 → ⦋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})))) |
| 23 | 13, 22 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑇 → ⦋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})))) |
| 24 | 23 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑇 → (𝑦 ∈ (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}))))) |
| 25 | 24 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (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})))))) |
| 26 | 25, 3 | elrab2 3695 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((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})))))) |
| 27 | 26 | simprbi 496 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
| 28 | 6, 27 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
| 29 | 28 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
| 30 | | elrabi 3687 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑇 ∈ {𝑡 ∈ ((((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...𝑁))) |
| 31 | 30, 3 | eleq2s 2859 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
| 32 | 6, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
| 33 | | xp1st 8046 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
| 34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1st
‘𝑇) ∈
(((0..^𝐾)
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
| 35 | | xp1st 8046 |
. . . . . . . . . . . . . . . . . 18
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
| 36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
| 37 | | elmapi 8889 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
| 38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
| 39 | | elfzoelz 13699 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ) |
| 40 | 39 | ssriv 3987 |
. . . . . . . . . . . . . . . 16
⊢
(0..^𝐾) ⊆
ℤ |
| 41 | | fss 6752 |
. . . . . . . . . . . . . . . 16
⊢
(((1st ‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶ℤ) |
| 42 | 38, 40, 41 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶ℤ) |
| 43 | 42 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
(1st ‘(1st ‘𝑇)):(1...𝑁)⟶ℤ) |
| 44 | | xp2nd 8047 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
| 45 | 34, 44 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
| 46 | | fvex 6919 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘(1st ‘𝑇)) ∈ V |
| 47 | | f1oeq1 6836 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
| 48 | 46, 47 | elab 3679 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
| 49 | 45, 48 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
| 50 | 49 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
| 51 | 2, 29, 43, 50, 8 | poimirlem1 37628 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
¬ ∃*𝑛 ∈
(1...𝑁)((𝐹‘((2nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑇))‘𝑛)) |
| 52 | 51 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑇))‘𝑛)) |
| 53 | 1 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ≠ (2nd
‘𝑇)) → 𝑁 ∈
ℕ) |
| 54 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → (2nd ‘𝑡) = (2nd ‘𝑧)) |
| 55 | 54 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑧))) |
| 56 | 55 | ifbid 4549 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑧), 𝑦, (𝑦 + 1))) |
| 57 | 56 | csbeq1d 3903 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑧 → ⦋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})))) |
| 58 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑧))) |
| 59 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑧 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑧))) |
| 60 | 59 | imaeq1d 6077 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑧 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑧)) “
(1...𝑗))) |
| 61 | 60 | xpeq1d 5714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1})) |
| 62 | 59 | imaeq1d 6077 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑧 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑧)) “ ((𝑗 + 1)...𝑁))) |
| 63 | 62 | xpeq1d 5714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) |
| 64 | 61, 63 | uneq12d 4169 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
| 65 | 58, 64 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → ((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑧)) ∘f + ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
| 66 | 65 | csbeq2dv 3906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑧 → ⦋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})))) |
| 67 | 57, 66 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑧 → ⦋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})))) |
| 68 | 67 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑧 → (𝑦 ∈ (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}))))) |
| 69 | 68 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑧 → (𝐹 = (𝑦 ∈ (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})))))) |
| 70 | 69, 3 | elrab2 3695 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 ↔ (𝑧 ∈ ((((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})))))) |
| 71 | 70 | simprbi 496 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘f + ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
| 72 | 71 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ≠ (2nd
‘𝑇)) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘f + ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
| 73 | | elrabi 3687 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ {𝑡 ∈ ((((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...𝑁))) |
| 74 | 73, 3 | eleq2s 2859 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
| 75 | | xp1st 8046 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
| 76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → (1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
| 77 | | xp1st 8046 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
| 78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑆 → (1st
‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
| 79 | | elmapi 8889 |
. . . . . . . . . . . . . . . . . 18
⊢
((1st ‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾)) |
| 80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾)) |
| 81 | | fss 6752 |
. . . . . . . . . . . . . . . . 17
⊢
(((1st ‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶ℤ) |
| 82 | 80, 40, 81 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶ℤ) |
| 83 | 82 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ≠ (2nd
‘𝑇)) →
(1st ‘(1st ‘𝑧)):(1...𝑁)⟶ℤ) |
| 84 | | xp2nd 8047 |
. . . . . . . . . . . . . . . . . 18
⊢
((1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
| 85 | 76, 84 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
| 86 | | fvex 6919 |
. . . . . . . . . . . . . . . . . 18
⊢
(2nd ‘(1st ‘𝑧)) ∈ V |
| 87 | | f1oeq1 6836 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (2nd
‘(1st ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))) |
| 88 | 86, 87 | elab 3679 |
. . . . . . . . . . . . . . . . 17
⊢
((2nd ‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
| 89 | 85, 88 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
| 90 | 89 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ≠ (2nd
‘𝑇)) →
(2nd ‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
| 91 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ≠ (2nd
‘𝑇)) →
(2nd ‘𝑇)
∈ (1...(𝑁 −
1))) |
| 92 | | xp2nd 8047 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd ‘𝑧) ∈ (0...𝑁)) |
| 93 | 74, 92 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → (2nd ‘𝑧) ∈ (0...𝑁)) |
| 94 | 93 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (2nd ‘𝑧) ∈ (0...𝑁)) |
| 95 | | eldifsn 4786 |
. . . . . . . . . . . . . . . . 17
⊢
((2nd ‘𝑧) ∈ ((0...𝑁) ∖ {(2nd ‘𝑇)}) ↔ ((2nd
‘𝑧) ∈ (0...𝑁) ∧ (2nd
‘𝑧) ≠
(2nd ‘𝑇))) |
| 96 | 95 | biimpri 228 |
. . . . . . . . . . . . . . . 16
⊢
(((2nd ‘𝑧) ∈ (0...𝑁) ∧ (2nd ‘𝑧) ≠ (2nd
‘𝑇)) →
(2nd ‘𝑧)
∈ ((0...𝑁) ∖
{(2nd ‘𝑇)})) |
| 97 | 94, 96 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ≠ (2nd
‘𝑇)) →
(2nd ‘𝑧)
∈ ((0...𝑁) ∖
{(2nd ‘𝑇)})) |
| 98 | 53, 72, 83, 90, 91, 97 | poimirlem2 37629 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ≠ (2nd
‘𝑇)) →
∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑇))‘𝑛)) |
| 99 | 98 | ex 412 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ((2nd ‘𝑧) ≠ (2nd
‘𝑇) →
∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑇))‘𝑛))) |
| 100 | 99 | necon1bd 2958 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑇) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑇))‘𝑛) → (2nd ‘𝑧) = (2nd ‘𝑇))) |
| 101 | 52, 100 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (2nd ‘𝑧) = (2nd ‘𝑇)) |
| 102 | | eleq1 2829 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘𝑧) = (2nd ‘𝑇) → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2nd
‘𝑇) ∈
(1...(𝑁 −
1)))) |
| 103 | 102 | biimparc 479 |
. . . . . . . . . . . . . . 15
⊢
(((2nd ‘𝑇) ∈ (1...(𝑁 − 1)) ∧ (2nd
‘𝑧) = (2nd
‘𝑇)) →
(2nd ‘𝑧)
∈ (1...(𝑁 −
1))) |
| 104 | 103 | anim2i 617 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((2nd
‘𝑇) ∈
(1...(𝑁 − 1)) ∧
(2nd ‘𝑧) =
(2nd ‘𝑇)))
→ (𝜑 ∧
(2nd ‘𝑧)
∈ (1...(𝑁 −
1)))) |
| 105 | 104 | anassrs 467 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑧) =
(2nd ‘𝑇))
→ (𝜑 ∧
(2nd ‘𝑧)
∈ (1...(𝑁 −
1)))) |
| 106 | 71 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘f + ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
| 107 | | breq1 5146 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 0 → (𝑦 < (2nd ‘𝑧) ↔ 0 < (2nd
‘𝑧))) |
| 108 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 0 → 𝑦 = 0) |
| 109 | 107, 108 | ifbieq1d 4550 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 0 → if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) = if(0 < (2nd
‘𝑧), 0, (𝑦 + 1))) |
| 110 | | elfznn 13593 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑧) ∈
ℕ) |
| 111 | 110 | nngt0d 12315 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → 0 < (2nd
‘𝑧)) |
| 112 | 111 | iftrued 4533 |
. . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → if(0 <
(2nd ‘𝑧),
0, (𝑦 + 1)) =
0) |
| 113 | 112 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → if(0 < (2nd
‘𝑧), 0, (𝑦 + 1)) = 0) |
| 114 | 109, 113 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → if(𝑦 < (2nd ‘𝑧), 𝑦, (𝑦 + 1)) = 0) |
| 115 | 114 | csbeq1d 3903 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘f + ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋0 / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘f + ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
| 116 | | c0ex 11255 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
V |
| 117 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = 0 → (1...𝑗) = (1...0)) |
| 118 | | fz10 13585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1...0) =
∅ |
| 119 | 117, 118 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 0 → (1...𝑗) = ∅) |
| 120 | 119 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 0 → ((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑧)) “
∅)) |
| 121 | 120 | xpeq1d 5714 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 0 → (((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑧)) “ ∅) ×
{1})) |
| 122 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = 0 → (𝑗 + 1) = (0 + 1)) |
| 123 | | 0p1e1 12388 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 + 1) =
1 |
| 124 | 122, 123 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = 0 → (𝑗 + 1) = 1) |
| 125 | 124 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 0 → ((𝑗 + 1)...𝑁) = (1...𝑁)) |
| 126 | 125 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 0 → ((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑧)) “
(1...𝑁))) |
| 127 | 126 | xpeq1d 5714 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 0 → (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑧)) “ (1...𝑁)) × {0})) |
| 128 | 121, 127 | uneq12d 4169 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 0 → ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑧)) “ ∅) × {1}) ∪
(((2nd ‘(1st ‘𝑧)) “ (1...𝑁)) × {0}))) |
| 129 | | ima0 6095 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((2nd ‘(1st ‘𝑧)) “ ∅) =
∅ |
| 130 | 129 | xpeq1i 5711 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((2nd ‘(1st ‘𝑧)) “ ∅) × {1}) = (∅
× {1}) |
| 131 | | 0xp 5784 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∅
× {1}) = ∅ |
| 132 | 130, 131 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((2nd ‘(1st ‘𝑧)) “ ∅) × {1}) =
∅ |
| 133 | 132 | uneq1i 4164 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((2nd ‘(1st ‘𝑧)) “ ∅) × {1}) ∪
(((2nd ‘(1st ‘𝑧)) “ (1...𝑁)) × {0})) = (∅ ∪
(((2nd ‘(1st ‘𝑧)) “ (1...𝑁)) × {0})) |
| 134 | | uncom 4158 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∅
∪ (((2nd ‘(1st ‘𝑧)) “ (1...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑧)) “ (1...𝑁)) × {0}) ∪
∅) |
| 135 | | un0 4394 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((2nd ‘(1st ‘𝑧)) “ (1...𝑁)) × {0}) ∪ ∅) =
(((2nd ‘(1st ‘𝑧)) “ (1...𝑁)) × {0}) |
| 136 | 133, 134,
135 | 3eqtri 2769 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((2nd ‘(1st ‘𝑧)) “ ∅) × {1}) ∪
(((2nd ‘(1st ‘𝑧)) “ (1...𝑁)) × {0})) = (((2nd
‘(1st ‘𝑧)) “ (1...𝑁)) × {0}) |
| 137 | 128, 136 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 0 → ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((2nd
‘(1st ‘𝑧)) “ (1...𝑁)) × {0})) |
| 138 | 137 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 0 → ((1st
‘(1st ‘𝑧)) ∘f + ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑧)) ∘f + (((2nd
‘(1st ‘𝑧)) “ (1...𝑁)) × {0}))) |
| 139 | 116, 138 | csbie 3934 |
. . . . . . . . . . . . . . . . 17
⊢
⦋0 / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘f + ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑧)) ∘f + (((2nd
‘(1st ‘𝑧)) “ (1...𝑁)) × {0})) |
| 140 | | f1ofo 6855 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2nd ‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑧)):(1...𝑁)–onto→(1...𝑁)) |
| 141 | 89, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)):(1...𝑁)–onto→(1...𝑁)) |
| 142 | | foima 6825 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2nd ‘(1st ‘𝑧)):(1...𝑁)–onto→(1...𝑁) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑁)) = (1...𝑁)) |
| 143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑆 → ((2nd
‘(1st ‘𝑧)) “ (1...𝑁)) = (1...𝑁)) |
| 144 | 143 | xpeq1d 5714 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → (((2nd
‘(1st ‘𝑧)) “ (1...𝑁)) × {0}) = ((1...𝑁) × {0})) |
| 145 | 144 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑆 → ((1st
‘(1st ‘𝑧)) ∘f + (((2nd
‘(1st ‘𝑧)) “ (1...𝑁)) × {0})) = ((1st
‘(1st ‘𝑧)) ∘f + ((1...𝑁) ×
{0}))) |
| 146 | | ovexd 7466 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → (1...𝑁) ∈ V) |
| 147 | 80 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → (1st
‘(1st ‘𝑧)) Fn (1...𝑁)) |
| 148 | | fnconstg 6796 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
V → ((1...𝑁) ×
{0}) Fn (1...𝑁)) |
| 149 | 116, 148 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → ((1...𝑁) × {0}) Fn (1...𝑁)) |
| 150 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑧))‘𝑛) = ((1st ‘(1st
‘𝑧))‘𝑛)) |
| 151 | 116 | fvconst2 7224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0) |
| 152 | 151 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0) |
| 153 | 80 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑧))‘𝑛) ∈ (0..^𝐾)) |
| 154 | | elfzonn0 13747 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1st ‘(1st ‘𝑧))‘𝑛) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑧))‘𝑛) ∈
ℕ0) |
| 155 | 153, 154 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑧))‘𝑛) ∈
ℕ0) |
| 156 | 155 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑧))‘𝑛) ∈ ℂ) |
| 157 | 156 | addridd 11461 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑧))‘𝑛) + 0) = ((1st
‘(1st ‘𝑧))‘𝑛)) |
| 158 | 146, 147,
149, 147, 150, 152, 157 | offveq 7723 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑆 → ((1st
‘(1st ‘𝑧)) ∘f + ((1...𝑁) × {0})) =
(1st ‘(1st ‘𝑧))) |
| 159 | 145, 158 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → ((1st
‘(1st ‘𝑧)) ∘f + (((2nd
‘(1st ‘𝑧)) “ (1...𝑁)) × {0})) = (1st
‘(1st ‘𝑧))) |
| 160 | 139, 159 | eqtrid 2789 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → ⦋0 / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘f + ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1st
‘(1st ‘𝑧))) |
| 161 | 160 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → ⦋0 / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘f + ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1st
‘(1st ‘𝑧))) |
| 162 | 115, 161 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑦 = 0) → ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘f + ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (1st
‘(1st ‘𝑧))) |
| 163 | | nnm1nn0 12567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
| 164 | 1, 163 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
| 165 | | 0elfz 13664 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 − 1) ∈
ℕ0 → 0 ∈ (0...(𝑁 − 1))) |
| 166 | 164, 165 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈ (0...(𝑁 − 1))) |
| 167 | 166 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → 0 ∈ (0...(𝑁 − 1))) |
| 168 | | fvexd 6921 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (1st
‘(1st ‘𝑧)) ∈ V) |
| 169 | 106, 162,
167, 168 | fvmptd 7023 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝐹‘0) = (1st
‘(1st ‘𝑧))) |
| 170 | 105, 169 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑧) =
(2nd ‘𝑇))
∧ 𝑧 ∈ 𝑆) → (𝐹‘0) = (1st
‘(1st ‘𝑧))) |
| 171 | 170 | an32s 652 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) = (2nd ‘𝑇)) → (𝐹‘0) = (1st
‘(1st ‘𝑧))) |
| 172 | 101, 171 | mpdan 687 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝐹‘0) = (1st
‘(1st ‘𝑧))) |
| 173 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑇 → (2nd ‘𝑧) = (2nd ‘𝑇)) |
| 174 | 173 | eleq1d 2826 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑇 → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ (2nd
‘𝑇) ∈
(1...(𝑁 −
1)))) |
| 175 | 174 | anbi2d 630 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑇 → ((𝜑 ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) ↔ (𝜑 ∧ (2nd ‘𝑇) ∈ (1...(𝑁 − 1))))) |
| 176 | | 2fveq3 6911 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑇 → (1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇))) |
| 177 | 176 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑇 → ((𝐹‘0) = (1st
‘(1st ‘𝑧)) ↔ (𝐹‘0) = (1st
‘(1st ‘𝑇)))) |
| 178 | 175, 177 | imbi12d 344 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑇 → (((𝜑 ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1st
‘(1st ‘𝑧))) ↔ ((𝜑 ∧ (2nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1st
‘(1st ‘𝑇))))) |
| 179 | 169 | expcom 413 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑆 → ((𝜑 ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1st
‘(1st ‘𝑧)))) |
| 180 | 178, 179 | vtoclga 3577 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ 𝑆 → ((𝜑 ∧ (2nd ‘𝑇) ∈ (1...(𝑁 − 1))) → (𝐹‘0) = (1st
‘(1st ‘𝑇)))) |
| 181 | 7, 180 | mpcom 38 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
(𝐹‘0) =
(1st ‘(1st ‘𝑇))) |
| 182 | 181 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝐹‘0) = (1st
‘(1st ‘𝑇))) |
| 183 | 172, 182 | eqtr3d 2779 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇))) |
| 184 | 183 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇))) |
| 185 | 1 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑁 ∈ ℕ) |
| 186 | 6 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑇 ∈ 𝑆) |
| 187 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2nd ‘𝑇) ∈ (1...(𝑁 − 1))) |
| 188 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → 𝑧 ∈ 𝑆) |
| 189 | 34 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
(1st ‘𝑇)
∈ (((0..^𝐾)
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
| 190 | | xpopth 8055 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) → (((1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇)) ∧
(2nd ‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑇))) ↔
(1st ‘𝑧) =
(1st ‘𝑇))) |
| 191 | 76, 189, 190 | syl2anr 597 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (((1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇)) ∧
(2nd ‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑇))) ↔
(1st ‘𝑧) =
(1st ‘𝑇))) |
| 192 | 32 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
| 193 | | xpopth 8055 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1st ‘𝑧) = (1st ‘𝑇) ∧ (2nd
‘𝑧) = (2nd
‘𝑇)) ↔ 𝑧 = 𝑇)) |
| 194 | 193 | biimpd 229 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1st ‘𝑧) = (1st ‘𝑇) ∧ (2nd
‘𝑧) = (2nd
‘𝑇)) → 𝑧 = 𝑇)) |
| 195 | 74, 192, 194 | syl2anr 597 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (((1st ‘𝑧) = (1st ‘𝑇) ∧ (2nd
‘𝑧) = (2nd
‘𝑇)) → 𝑧 = 𝑇)) |
| 196 | 101, 195 | mpan2d 694 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ((1st ‘𝑧) = (1st ‘𝑇) → 𝑧 = 𝑇)) |
| 197 | 191, 196 | sylbid 240 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (((1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇)) ∧
(2nd ‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑇))) → 𝑧 = 𝑇)) |
| 198 | 183, 197 | mpand 695 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ((2nd
‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑇)) → 𝑧 = 𝑇)) |
| 199 | 198 | necon3d 2961 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (2nd
‘(1st ‘𝑧)) ≠ (2nd
‘(1st ‘𝑇)))) |
| 200 | 199 | imp 406 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2nd
‘(1st ‘𝑧)) ≠ (2nd
‘(1st ‘𝑇))) |
| 201 | 185, 3, 186, 187, 188, 200 | poimirlem9 37636 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2nd
‘(1st ‘𝑧)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}))))) |
| 202 | 101 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (2nd ‘𝑧) = (2nd ‘𝑇)) |
| 203 | 184, 201,
202 | jca31 514 |
. . . . . . 7
⊢ ((((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) ∧ 𝑧 ≠ 𝑇) → (((1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇)) ∧
(2nd ‘(1st ‘𝑧)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))) ∧
(2nd ‘𝑧) =
(2nd ‘𝑇))) |
| 204 | 203 | ex 412 |
. . . . . 6
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (((1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇)) ∧
(2nd ‘(1st ‘𝑧)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))) ∧
(2nd ‘𝑧) =
(2nd ‘𝑇)))) |
| 205 | | simplr 769 |
. . . . . . . 8
⊢
((((1st ‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇)) ∧
(2nd ‘(1st ‘𝑧)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))) ∧
(2nd ‘𝑧) =
(2nd ‘𝑇))
→ (2nd ‘(1st ‘𝑧)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}))))) |
| 206 | | elfznn 13593 |
. . . . . . . . . . . . . 14
⊢
((2nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑇) ∈
ℕ) |
| 207 | 206 | nnred 12281 |
. . . . . . . . . . . . 13
⊢
((2nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑇) ∈
ℝ) |
| 208 | 207 | ltp1d 12198 |
. . . . . . . . . . . . 13
⊢
((2nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑇) <
((2nd ‘𝑇)
+ 1)) |
| 209 | 207, 208 | ltned 11397 |
. . . . . . . . . . . 12
⊢
((2nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑇) ≠
((2nd ‘𝑇)
+ 1)) |
| 210 | 209 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2nd ‘𝑇)
≠ ((2nd ‘𝑇) + 1)) |
| 211 | | fveq1 6905 |
. . . . . . . . . . . . 13
⊢
((2nd ‘(1st ‘𝑇)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)})))) →
((2nd ‘(1st ‘𝑇))‘(2nd ‘𝑇)) = (((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))))‘(2nd ‘𝑇))) |
| 212 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2nd ‘𝑇) ∈ ℝ → (2nd
‘𝑇) ∈
ℝ) |
| 213 | | ltp1 12107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2nd ‘𝑇) ∈ ℝ → (2nd
‘𝑇) <
((2nd ‘𝑇)
+ 1)) |
| 214 | 212, 213 | ltned 11397 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2nd ‘𝑇) ∈ ℝ → (2nd
‘𝑇) ≠
((2nd ‘𝑇)
+ 1)) |
| 215 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(2nd ‘𝑇) ∈ V |
| 216 | | ovex 7464 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2nd ‘𝑇) + 1) ∈ V |
| 217 | 215, 216,
216, 215 | fpr 7174 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2nd ‘𝑇) ≠ ((2nd ‘𝑇) + 1) →
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}⟶{((2nd
‘𝑇) + 1),
(2nd ‘𝑇)}) |
| 218 | 214, 217 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2nd ‘𝑇) ∈ ℝ →
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}⟶{((2nd
‘𝑇) + 1),
(2nd ‘𝑇)}) |
| 219 | | f1oi 6886 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ( I
↾ ((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})):((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})–1-1-onto→((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) |
| 220 | | f1of 6848 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (( I
↾ ((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})):((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})–1-1-onto→((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) → ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})):((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})⟶((1...𝑁)
∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) |
| 221 | 219, 220 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ( I
↾ ((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})):((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})⟶((1...𝑁)
∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) |
| 222 | | disjdif 4472 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) =
∅ |
| 223 | | fun 6770 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}⟶{((2nd
‘𝑇) + 1),
(2nd ‘𝑇)}
∧ ( I ↾ ((1...𝑁)
∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})):((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})⟶((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)})) ∧
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = ∅) →
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}))):({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) +
1)}))⟶({((2nd ‘𝑇) + 1), (2nd ‘𝑇)} ∪ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) |
| 224 | 222, 223 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}:{(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}⟶{((2nd
‘𝑇) + 1),
(2nd ‘𝑇)}
∧ ( I ↾ ((1...𝑁)
∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})):((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})⟶((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)})) →
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}))):({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) +
1)}))⟶({((2nd ‘𝑇) + 1), (2nd ‘𝑇)} ∪ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) |
| 225 | 218, 221,
224 | sylancl 586 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘𝑇) ∈ ℝ →
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}))):({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) +
1)}))⟶({((2nd ‘𝑇) + 1), (2nd ‘𝑇)} ∪ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) |
| 226 | 215 | prid1 4762 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘𝑇) ∈ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} |
| 227 | | elun1 4182 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2nd ‘𝑇) ∈ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} → (2nd
‘𝑇) ∈
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) |
| 228 | 226, 227 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(2nd ‘𝑇) ∈ ({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)})) |
| 229 | | fvco3 7008 |
. . . . . . . . . . . . . . . . . . 19
⊢
((({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}))):({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) +
1)}))⟶({((2nd ‘𝑇) + 1), (2nd ‘𝑇)} ∪ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) ∧ (2nd
‘𝑇) ∈
({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∪ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) →
(((2nd ‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))))‘(2nd ‘𝑇)) = ((2nd ‘(1st
‘𝑇))‘(({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))‘(2nd ‘𝑇)))) |
| 230 | 225, 228,
229 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘𝑇) ∈ ℝ → (((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))))‘(2nd ‘𝑇)) = ((2nd ‘(1st
‘𝑇))‘(({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))‘(2nd ‘𝑇)))) |
| 231 | 218 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2nd ‘𝑇) ∈ ℝ →
{〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} Fn {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) |
| 232 | | fnresi 6697 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ( I
↾ ((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) Fn ((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) |
| 233 | 222, 226 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = ∅ ∧
(2nd ‘𝑇)
∈ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}) |
| 234 | | fvun1 7000 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} Fn {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∧ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})) Fn ((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}) ∧ (({(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} ∩ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = ∅ ∧
(2nd ‘𝑇)
∈ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) → (({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))‘(2nd ‘𝑇)) = ({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}‘(2nd
‘𝑇))) |
| 235 | 232, 233,
234 | mp3an23 1455 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} Fn {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)} →
(({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)})))‘(2nd ‘𝑇)) = ({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}‘(2nd
‘𝑇))) |
| 236 | 231, 235 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2nd ‘𝑇) ∈ ℝ →
(({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)})))‘(2nd ‘𝑇)) = ({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉}‘(2nd
‘𝑇))) |
| 237 | 215, 216 | fvpr1 7212 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2nd ‘𝑇) ≠ ((2nd ‘𝑇) + 1) →
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}‘(2nd ‘𝑇)) = ((2nd
‘𝑇) +
1)) |
| 238 | 214, 237 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2nd ‘𝑇) ∈ ℝ →
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉}‘(2nd ‘𝑇)) = ((2nd
‘𝑇) +
1)) |
| 239 | 236, 238 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘𝑇) ∈ ℝ →
(({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)})))‘(2nd ‘𝑇)) = ((2nd ‘𝑇) + 1)) |
| 240 | 239 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘𝑇) ∈ ℝ → ((2nd
‘(1st ‘𝑇))‘(({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))‘(2nd ‘𝑇))) = ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1))) |
| 241 | 230, 240 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢
((2nd ‘𝑇) ∈ ℝ → (((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))))‘(2nd ‘𝑇)) = ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))) |
| 242 | 207, 241 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))))‘(2nd ‘𝑇)) = ((2nd ‘(1st
‘𝑇))‘((2nd ‘𝑇) + 1))) |
| 243 | 242 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇)) = (((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))))‘(2nd ‘𝑇)) ↔ ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇)) = ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)))) |
| 244 | 243 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
(((2nd ‘(1st ‘𝑇))‘(2nd ‘𝑇)) = (((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))))‘(2nd ‘𝑇)) ↔ ((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇)) = ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)))) |
| 245 | | f1of1 6847 |
. . . . . . . . . . . . . . . . 17
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁)) |
| 246 | 49, 245 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁)) |
| 247 | 246 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁)) |
| 248 | 1 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 249 | | npcan1 11688 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
| 250 | 248, 249 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
| 251 | 164 | nn0zd 12639 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
| 252 | | uzid 12893 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
| 253 | 251, 252 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
| 254 | | peano2uz 12943 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
| 255 | 253, 254 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
| 256 | 250, 255 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
| 257 | | fzss2 13604 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
| 258 | 256, 257 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
| 259 | 258 | sselda 3983 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2nd ‘𝑇)
∈ (1...𝑁)) |
| 260 | | fzp1elp1 13617 |
. . . . . . . . . . . . . . . . 17
⊢
((2nd ‘𝑇) ∈ (1...(𝑁 − 1)) → ((2nd
‘𝑇) + 1) ∈
(1...((𝑁 − 1) +
1))) |
| 261 | 260 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2nd ‘𝑇)
+ 1) ∈ (1...((𝑁
− 1) + 1))) |
| 262 | 250 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁)) |
| 263 | 262 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
(1...((𝑁 − 1) + 1)) =
(1...𝑁)) |
| 264 | 261, 263 | eleqtrd 2843 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2nd ‘𝑇)
+ 1) ∈ (1...𝑁)) |
| 265 | | f1veqaeq 7277 |
. . . . . . . . . . . . . . 15
⊢
(((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1→(1...𝑁) ∧ ((2nd ‘𝑇) ∈ (1...𝑁) ∧ ((2nd ‘𝑇) + 1) ∈ (1...𝑁))) → (((2nd
‘(1st ‘𝑇))‘(2nd ‘𝑇)) = ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)) → (2nd
‘𝑇) =
((2nd ‘𝑇)
+ 1))) |
| 266 | 247, 259,
264, 265 | syl12anc 837 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
(((2nd ‘(1st ‘𝑇))‘(2nd ‘𝑇)) = ((2nd
‘(1st ‘𝑇))‘((2nd ‘𝑇) + 1)) → (2nd
‘𝑇) =
((2nd ‘𝑇)
+ 1))) |
| 267 | 244, 266 | sylbid 240 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
(((2nd ‘(1st ‘𝑇))‘(2nd ‘𝑇)) = (((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))))‘(2nd ‘𝑇)) → (2nd ‘𝑇) = ((2nd
‘𝑇) +
1))) |
| 268 | 211, 267 | syl5 34 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2nd ‘(1st ‘𝑇)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)})))) →
(2nd ‘𝑇) =
((2nd ‘𝑇)
+ 1))) |
| 269 | 268 | necon3d 2961 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2nd ‘𝑇)
≠ ((2nd ‘𝑇) + 1) → (2nd
‘(1st ‘𝑇)) ≠ ((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))))) |
| 270 | 210, 269 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
(2nd ‘(1st ‘𝑇)) ≠ ((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))))) |
| 271 | | 2fveq3 6911 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑇 → (2nd
‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑇))) |
| 272 | 271 | neeq1d 3000 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑇 → ((2nd
‘(1st ‘𝑧)) ≠ ((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))) ↔ (2nd ‘(1st ‘𝑇)) ≠ ((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))))) |
| 273 | 270, 272 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
(𝑧 = 𝑇 → (2nd
‘(1st ‘𝑧)) ≠ ((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)})))))) |
| 274 | 273 | necon2d 2963 |
. . . . . . . 8
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2nd ‘(1st ‘𝑧)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)})))) →
𝑧 ≠ 𝑇)) |
| 275 | 205, 274 | syl5 34 |
. . . . . . 7
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
((((1st ‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇)) ∧
(2nd ‘(1st ‘𝑧)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))) ∧
(2nd ‘𝑧) =
(2nd ‘𝑇))
→ 𝑧 ≠ 𝑇)) |
| 276 | 275 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → ((((1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇)) ∧
(2nd ‘(1st ‘𝑧)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))) ∧
(2nd ‘𝑧) =
(2nd ‘𝑇))
→ 𝑧 ≠ 𝑇)) |
| 277 | 204, 276 | impbid 212 |
. . . . 5
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 ↔ (((1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇)) ∧
(2nd ‘(1st ‘𝑧)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))) ∧
(2nd ‘𝑧) =
(2nd ‘𝑇)))) |
| 278 | | eqop 8056 |
. . . . . . . 8
⊢ (𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (𝑧 = 〈〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉,
(2nd ‘𝑇)〉 ↔ ((1st ‘𝑧) = 〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉
∧ (2nd ‘𝑧) = (2nd ‘𝑇)))) |
| 279 | | eqop 8056 |
. . . . . . . . . 10
⊢
((1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ((1st ‘𝑧) = 〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉
↔ ((1st ‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇)) ∧
(2nd ‘(1st ‘𝑧)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}))))))) |
| 280 | 75, 279 | syl 17 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → ((1st ‘𝑧) = 〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉
↔ ((1st ‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇)) ∧
(2nd ‘(1st ‘𝑧)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) +
1)}))))))) |
| 281 | 280 | anbi1d 631 |
. . . . . . . 8
⊢ (𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (((1st ‘𝑧) = 〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉
∧ (2nd ‘𝑧) = (2nd ‘𝑇)) ↔ (((1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇)) ∧
(2nd ‘(1st ‘𝑧)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))) ∧
(2nd ‘𝑧) =
(2nd ‘𝑇)))) |
| 282 | 278, 281 | bitrd 279 |
. . . . . . 7
⊢ (𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (𝑧 = 〈〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉,
(2nd ‘𝑇)〉 ↔ (((1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇)) ∧
(2nd ‘(1st ‘𝑧)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))) ∧
(2nd ‘𝑧) =
(2nd ‘𝑇)))) |
| 283 | 74, 282 | syl 17 |
. . . . . 6
⊢ (𝑧 ∈ 𝑆 → (𝑧 = 〈〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉,
(2nd ‘𝑇)〉 ↔ (((1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇)) ∧
(2nd ‘(1st ‘𝑧)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))) ∧
(2nd ‘𝑧) =
(2nd ‘𝑇)))) |
| 284 | 283 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝑧 = 〈〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉,
(2nd ‘𝑇)〉 ↔ (((1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑇)) ∧
(2nd ‘(1st ‘𝑧)) = ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))) ∧
(2nd ‘𝑧) =
(2nd ‘𝑇)))) |
| 285 | 277, 284 | bitr4d 282 |
. . . 4
⊢ (((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ∧
𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 ↔ 𝑧 = 〈〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉,
(2nd ‘𝑇)〉)) |
| 286 | 285 | ralrimiva 3146 |
. . 3
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
∀𝑧 ∈ 𝑆 (𝑧 ≠ 𝑇 ↔ 𝑧 = 〈〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉,
(2nd ‘𝑇)〉)) |
| 287 | | reu6i 3734 |
. . 3
⊢
((〈〈(1st ‘(1st ‘𝑇)), ((2nd
‘(1st ‘𝑇)) ∘ ({〈(2nd
‘𝑇), ((2nd
‘𝑇) + 1)〉,
〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾
((1...𝑁) ∖
{(2nd ‘𝑇),
((2nd ‘𝑇)
+ 1)}))))〉, (2nd ‘𝑇)〉 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 (𝑧 ≠ 𝑇 ↔ 𝑧 = 〈〈(1st
‘(1st ‘𝑇)), ((2nd ‘(1st
‘𝑇)) ∘
({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd
‘𝑇) + 1),
(2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd
‘𝑇), ((2nd
‘𝑇) + 1)}))))〉,
(2nd ‘𝑇)〉)) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
| 288 | 9, 286, 287 | syl2anc 584 |
. 2
⊢ ((𝜑 ∧ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
| 289 | | xp2nd 8047 |
. . . . . . 7
⊢ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd ‘𝑇) ∈ (0...𝑁)) |
| 290 | 32, 289 | syl 17 |
. . . . . 6
⊢ (𝜑 → (2nd
‘𝑇) ∈ (0...𝑁)) |
| 291 | 290 | biantrurd 532 |
. . . . 5
⊢ (𝜑 → (¬ (2nd
‘𝑇) ∈
(1...(𝑁 − 1)) ↔
((2nd ‘𝑇)
∈ (0...𝑁) ∧ ¬
(2nd ‘𝑇)
∈ (1...(𝑁 −
1))))) |
| 292 | 1 | nnnn0d 12587 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 293 | | nn0uz 12920 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
| 294 | 292, 293 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
| 295 | | fzpred 13612 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘0) → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁))) |
| 296 | 294, 295 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁))) |
| 297 | 123 | oveq1i 7441 |
. . . . . . . . . . 11
⊢ ((0 +
1)...𝑁) = (1...𝑁) |
| 298 | 297 | uneq2i 4165 |
. . . . . . . . . 10
⊢ ({0}
∪ ((0 + 1)...𝑁)) = ({0}
∪ (1...𝑁)) |
| 299 | 296, 298 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝜑 → (0...𝑁) = ({0} ∪ (1...𝑁))) |
| 300 | 299 | difeq1d 4125 |
. . . . . . . 8
⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1)))) |
| 301 | | difundir 4291 |
. . . . . . . . . 10
⊢ (({0}
∪ (1...𝑁)) ∖
(1...(𝑁 − 1))) =
(({0} ∖ (1...(𝑁
− 1))) ∪ ((1...𝑁)
∖ (1...(𝑁 −
1)))) |
| 302 | | 0lt1 11785 |
. . . . . . . . . . . . . 14
⊢ 0 <
1 |
| 303 | | 0re 11263 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
| 304 | | 1re 11261 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
| 305 | 303, 304 | ltnlei 11382 |
. . . . . . . . . . . . . 14
⊢ (0 < 1
↔ ¬ 1 ≤ 0) |
| 306 | 302, 305 | mpbi 230 |
. . . . . . . . . . . . 13
⊢ ¬ 1
≤ 0 |
| 307 | | elfzle1 13567 |
. . . . . . . . . . . . 13
⊢ (0 ∈
(1...(𝑁 − 1)) →
1 ≤ 0) |
| 308 | 306, 307 | mto 197 |
. . . . . . . . . . . 12
⊢ ¬ 0
∈ (1...(𝑁 −
1)) |
| 309 | | incom 4209 |
. . . . . . . . . . . . . 14
⊢
((1...(𝑁 − 1))
∩ {0}) = ({0} ∩ (1...(𝑁 − 1))) |
| 310 | 309 | eqeq1i 2742 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑁 −
1)) ∩ {0}) = ∅ ↔ ({0} ∩ (1...(𝑁 − 1))) = ∅) |
| 311 | | disjsn 4711 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑁 −
1)) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (1...(𝑁 − 1))) |
| 312 | | disj3 4454 |
. . . . . . . . . . . . 13
⊢ (({0}
∩ (1...(𝑁 − 1)))
= ∅ ↔ {0} = ({0} ∖ (1...(𝑁 − 1)))) |
| 313 | 310, 311,
312 | 3bitr3i 301 |
. . . . . . . . . . . 12
⊢ (¬ 0
∈ (1...(𝑁 − 1))
↔ {0} = ({0} ∖ (1...(𝑁 − 1)))) |
| 314 | 308, 313 | mpbi 230 |
. . . . . . . . . . 11
⊢ {0} =
({0} ∖ (1...(𝑁
− 1))) |
| 315 | 314 | uneq1i 4164 |
. . . . . . . . . 10
⊢ ({0}
∪ ((1...𝑁) ∖
(1...(𝑁 − 1)))) =
(({0} ∖ (1...(𝑁
− 1))) ∪ ((1...𝑁)
∖ (1...(𝑁 −
1)))) |
| 316 | 301, 315 | eqtr4i 2768 |
. . . . . . . . 9
⊢ (({0}
∪ (1...𝑁)) ∖
(1...(𝑁 − 1))) = ({0}
∪ ((1...𝑁) ∖
(1...(𝑁 −
1)))) |
| 317 | | difundir 4291 |
. . . . . . . . . . . 12
⊢
(((1...(𝑁 −
1)) ∪ {𝑁}) ∖
(1...(𝑁 − 1))) =
(((1...(𝑁 − 1))
∖ (1...(𝑁 −
1))) ∪ ({𝑁} ∖
(1...(𝑁 −
1)))) |
| 318 | | difid 4376 |
. . . . . . . . . . . . 13
⊢
((1...(𝑁 − 1))
∖ (1...(𝑁 −
1))) = ∅ |
| 319 | 318 | uneq1i 4164 |
. . . . . . . . . . . 12
⊢
(((1...(𝑁 −
1)) ∖ (1...(𝑁 −
1))) ∪ ({𝑁} ∖
(1...(𝑁 − 1)))) =
(∅ ∪ ({𝑁} ∖
(1...(𝑁 −
1)))) |
| 320 | | uncom 4158 |
. . . . . . . . . . . . 13
⊢ (∅
∪ ({𝑁} ∖
(1...(𝑁 − 1)))) =
(({𝑁} ∖ (1...(𝑁 − 1))) ∪
∅) |
| 321 | | un0 4394 |
. . . . . . . . . . . . 13
⊢ (({𝑁} ∖ (1...(𝑁 − 1))) ∪ ∅) =
({𝑁} ∖ (1...(𝑁 − 1))) |
| 322 | 320, 321 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ (∅
∪ ({𝑁} ∖
(1...(𝑁 − 1)))) =
({𝑁} ∖ (1...(𝑁 − 1))) |
| 323 | 317, 319,
322 | 3eqtri 2769 |
. . . . . . . . . . 11
⊢
(((1...(𝑁 −
1)) ∪ {𝑁}) ∖
(1...(𝑁 − 1))) =
({𝑁} ∖ (1...(𝑁 − 1))) |
| 324 | | nnuz 12921 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
| 325 | 1, 324 | eleqtrdi 2851 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
| 326 | 250, 325 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘1)) |
| 327 | | fzsplit2 13589 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
| 328 | 326, 256,
327 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
| 329 | 250 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁)) |
| 330 | 1 | nnzd 12640 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 331 | | fzsn 13606 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁}) |
| 332 | 330, 331 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁...𝑁) = {𝑁}) |
| 333 | 329, 332 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁}) |
| 334 | 333 | uneq2d 4168 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
| 335 | 328, 334 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
| 336 | 335 | difeq1d 4125 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ (1...(𝑁 − 1)))) |
| 337 | 1 | nnred 12281 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 338 | 337 | ltm1d 12200 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 − 1) < 𝑁) |
| 339 | 164 | nn0red 12588 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
| 340 | 339, 337 | ltnled 11408 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1))) |
| 341 | 338, 340 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1)) |
| 342 | | elfzle2 13568 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1)) |
| 343 | 341, 342 | nsyl 140 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1))) |
| 344 | | incom 4209 |
. . . . . . . . . . . . . 14
⊢
((1...(𝑁 − 1))
∩ {𝑁}) = ({𝑁} ∩ (1...(𝑁 − 1))) |
| 345 | 344 | eqeq1i 2742 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑁 −
1)) ∩ {𝑁}) = ∅
↔ ({𝑁} ∩
(1...(𝑁 − 1))) =
∅) |
| 346 | | disjsn 4711 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑁 −
1)) ∩ {𝑁}) = ∅
↔ ¬ 𝑁 ∈
(1...(𝑁 −
1))) |
| 347 | | disj3 4454 |
. . . . . . . . . . . . 13
⊢ (({𝑁} ∩ (1...(𝑁 − 1))) = ∅ ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1)))) |
| 348 | 345, 346,
347 | 3bitr3i 301 |
. . . . . . . . . . . 12
⊢ (¬
𝑁 ∈ (1...(𝑁 − 1)) ↔ {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1)))) |
| 349 | 343, 348 | sylib 218 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑁} = ({𝑁} ∖ (1...(𝑁 − 1)))) |
| 350 | 323, 336,
349 | 3eqtr4a 2803 |
. . . . . . . . . 10
⊢ (𝜑 → ((1...𝑁) ∖ (1...(𝑁 − 1))) = {𝑁}) |
| 351 | 350 | uneq2d 4168 |
. . . . . . . . 9
⊢ (𝜑 → ({0} ∪ ((1...𝑁) ∖ (1...(𝑁 − 1)))) = ({0} ∪
{𝑁})) |
| 352 | 316, 351 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝜑 → (({0} ∪ (1...𝑁)) ∖ (1...(𝑁 − 1))) = ({0} ∪
{𝑁})) |
| 353 | 300, 352 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((0...𝑁) ∖ (1...(𝑁 − 1))) = ({0} ∪ {𝑁})) |
| 354 | 353 | eleq2d 2827 |
. . . . . 6
⊢ (𝜑 → ((2nd
‘𝑇) ∈
((0...𝑁) ∖
(1...(𝑁 − 1))) ↔
(2nd ‘𝑇)
∈ ({0} ∪ {𝑁}))) |
| 355 | | eldif 3961 |
. . . . . 6
⊢
((2nd ‘𝑇) ∈ ((0...𝑁) ∖ (1...(𝑁 − 1))) ↔ ((2nd
‘𝑇) ∈ (0...𝑁) ∧ ¬ (2nd
‘𝑇) ∈
(1...(𝑁 −
1)))) |
| 356 | | elun 4153 |
. . . . . . 7
⊢
((2nd ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2nd ‘𝑇) ∈ {0} ∨
(2nd ‘𝑇)
∈ {𝑁})) |
| 357 | 215 | elsn 4641 |
. . . . . . . 8
⊢
((2nd ‘𝑇) ∈ {0} ↔ (2nd
‘𝑇) =
0) |
| 358 | 215 | elsn 4641 |
. . . . . . . 8
⊢
((2nd ‘𝑇) ∈ {𝑁} ↔ (2nd ‘𝑇) = 𝑁) |
| 359 | 357, 358 | orbi12i 915 |
. . . . . . 7
⊢
(((2nd ‘𝑇) ∈ {0} ∨ (2nd
‘𝑇) ∈ {𝑁}) ↔ ((2nd
‘𝑇) = 0 ∨
(2nd ‘𝑇) =
𝑁)) |
| 360 | 356, 359 | bitri 275 |
. . . . . 6
⊢
((2nd ‘𝑇) ∈ ({0} ∪ {𝑁}) ↔ ((2nd ‘𝑇) = 0 ∨ (2nd
‘𝑇) = 𝑁)) |
| 361 | 354, 355,
360 | 3bitr3g 313 |
. . . . 5
⊢ (𝜑 → (((2nd
‘𝑇) ∈ (0...𝑁) ∧ ¬ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) ↔
((2nd ‘𝑇)
= 0 ∨ (2nd ‘𝑇) = 𝑁))) |
| 362 | 291, 361 | bitrd 279 |
. . . 4
⊢ (𝜑 → (¬ (2nd
‘𝑇) ∈
(1...(𝑁 − 1)) ↔
((2nd ‘𝑇)
= 0 ∨ (2nd ‘𝑇) = 𝑁))) |
| 363 | 362 | biimpa 476 |
. . 3
⊢ ((𝜑 ∧ ¬ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
((2nd ‘𝑇)
= 0 ∨ (2nd ‘𝑇) = 𝑁)) |
| 364 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (2nd
‘𝑇) = 0) → 𝑁 ∈
ℕ) |
| 365 | 4 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (2nd
‘𝑇) = 0) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) |
| 366 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (2nd
‘𝑇) = 0) → 𝑇 ∈ 𝑆) |
| 367 | | poimirlem22.4 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) |
| 368 | 367 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ (2nd
‘𝑇) = 0) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) |
| 369 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ (2nd
‘𝑇) = 0) →
(2nd ‘𝑇) =
0) |
| 370 | 364, 3, 365, 366, 368, 369 | poimirlem18 37645 |
. . . 4
⊢ ((𝜑 ∧ (2nd
‘𝑇) = 0) →
∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
| 371 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (2nd
‘𝑇) = 𝑁) → 𝑁 ∈ ℕ) |
| 372 | 4 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (2nd
‘𝑇) = 𝑁) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) |
| 373 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (2nd
‘𝑇) = 𝑁) → 𝑇 ∈ 𝑆) |
| 374 | | poimirlem22.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0) |
| 375 | 374 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ (2nd
‘𝑇) = 𝑁) ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0) |
| 376 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ (2nd
‘𝑇) = 𝑁) → (2nd
‘𝑇) = 𝑁) |
| 377 | 371, 3, 372, 373, 375, 376 | poimirlem21 37648 |
. . . 4
⊢ ((𝜑 ∧ (2nd
‘𝑇) = 𝑁) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
| 378 | 370, 377 | jaodan 960 |
. . 3
⊢ ((𝜑 ∧ ((2nd
‘𝑇) = 0 ∨
(2nd ‘𝑇) =
𝑁)) → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
| 379 | 363, 378 | syldan 591 |
. 2
⊢ ((𝜑 ∧ ¬ (2nd
‘𝑇) ∈
(1...(𝑁 − 1))) →
∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
| 380 | 288, 379 | pm2.61dan 813 |
1
⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |