Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | | poimirlem22.s |
. . 3
⊢ 𝑆 = {𝑡 ∈ ((((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 |
. . 3
⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) |
4 | | poimirlem22.2 |
. . 3
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
5 | | poimirlem18.3 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 𝐾) |
6 | | poimirlem18.4 |
. . 3
⊢ (𝜑 → (2nd
‘𝑇) =
0) |
7 | 1, 2, 3, 4, 5, 6 | poimirlem17 35339 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
8 | 6 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (2nd ‘𝑇) = 0) |
9 | | 0nnn 11695 |
. . . . . . . . . . . . 13
⊢ ¬ 0
∈ ℕ |
10 | | elfznn 12970 |
. . . . . . . . . . . . 13
⊢ (0 ∈
(1...(𝑁 − 1)) →
0 ∈ ℕ) |
11 | 9, 10 | mto 200 |
. . . . . . . . . . . 12
⊢ ¬ 0
∈ (1...(𝑁 −
1)) |
12 | | eleq1 2838 |
. . . . . . . . . . . 12
⊢
((2nd ‘𝑧) = 0 → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ 0 ∈ (1...(𝑁 − 1)))) |
13 | 11, 12 | mtbiri 331 |
. . . . . . . . . . 11
⊢
((2nd ‘𝑧) = 0 → ¬ (2nd
‘𝑧) ∈
(1...(𝑁 −
1))) |
14 | 13 | necon2ai 2978 |
. . . . . . . . . 10
⊢
((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑧) ≠
0) |
15 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ) |
16 | | fveq2 6651 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (2nd ‘𝑡) = (2nd ‘𝑧)) |
17 | 16 | breq2d 5037 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑧))) |
18 | 17 | ifbid 4436 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑧 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑧), 𝑦, (𝑦 + 1))) |
19 | 18 | csbeq1d 3805 |
. . . . . . . . . . . . . . . . . . . 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})))) |
20 | | 2fveq3 6656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑧))) |
21 | | 2fveq3 6656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑧 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑧))) |
22 | 21 | imaeq1d 5893 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑧)) “
(1...𝑗))) |
23 | 22 | xpeq1d 5546 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1})) |
24 | 21 | imaeq1d 5893 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑧)) “ ((𝑗 + 1)...𝑁))) |
25 | 24 | xpeq1d 5546 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) |
26 | 23, 25 | uneq12d 4065 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
27 | 20, 26 | oveq12d 7161 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑧 → ((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑧)) ∘f + ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
28 | 27 | csbeq2dv 3808 |
. . . . . . . . . . . . . . . . . . . 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})))) |
29 | 19, 28 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑧 → ⦋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})))) |
30 | 29 | mpteq2dv 5121 |
. . . . . . . . . . . . . . . . . 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}))))) |
31 | 30 | eqeq2d 2770 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑧 → (𝐹 = (𝑦 ∈ (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})))))) |
32 | 31, 2 | elrab2 3603 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 ↔ (𝑧 ∈ ((((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})))))) |
33 | 32 | simprbi 501 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘f + ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
34 | 33 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘f + ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
35 | | elrabi 3594 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ {𝑡 ∈ ((((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...𝑁))) |
36 | 35, 2 | eleq2s 2869 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
37 | | xp1st 7718 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑆 → (1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
39 | | xp1st 7718 |
. . . . . . . . . . . . . . . . . 18
⊢
((1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → (1st
‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
41 | | elmapi 8431 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾)) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾)) |
43 | | elfzoelz 13072 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ) |
44 | 43 | ssriv 3892 |
. . . . . . . . . . . . . . . 16
⊢
(0..^𝐾) ⊆
ℤ |
45 | | fss 6505 |
. . . . . . . . . . . . . . . 16
⊢
(((1st ‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶ℤ) |
46 | 42, 44, 45 | sylancl 590 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶ℤ) |
47 | 46 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶ℤ) |
48 | | xp2nd 7719 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
49 | 38, 48 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
50 | | fvex 6664 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘(1st ‘𝑧)) ∈ V |
51 | | f1oeq1 6583 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (2nd
‘(1st ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))) |
52 | 50, 51 | elab 3586 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
53 | 49, 52 | sylib 221 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
54 | 53 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
55 | | simpr 489 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd
‘𝑧) ∈
(1...(𝑁 −
1))) |
56 | 15, 34, 47, 54, 55 | poimirlem1 35323 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛)) |
57 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → 𝑁 ∈ ℕ) |
58 | | fveq2 6651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
59 | 58 | breq2d 5037 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) |
60 | 59 | ifbid 4436 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) |
61 | 60 | csbeq1d 3805 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → ⦋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})))) |
62 | | 2fveq3 6656 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
63 | | 2fveq3 6656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) |
64 | 63 | imaeq1d 5893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑗))) |
65 | 64 | xpeq1d 5546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1})) |
66 | 63 | imaeq1d 5893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
67 | 66 | xpeq1d 5546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
68 | 65, 67 | uneq12d 4065 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑇 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
69 | 62, 68 | oveq12d 7161 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
70 | 69 | csbeq2dv 3808 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → ⦋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})))) |
71 | 61, 70 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑇 → ⦋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})))) |
72 | 71 | mpteq2dv 5121 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑇 → (𝑦 ∈ (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}))))) |
73 | 72 | eqeq2d 2770 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (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})))))) |
74 | 73, 2 | elrab2 3603 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((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})))))) |
75 | 74 | simprbi 501 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
76 | 4, 75 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
77 | 76 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
78 | | elrabi 3594 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑇 ∈ {𝑡 ∈ ((((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...𝑁))) |
79 | 78, 2 | eleq2s 2869 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
80 | 4, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
81 | | xp1st 7718 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (1st
‘𝑇) ∈
(((0..^𝐾)
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
83 | | xp1st 7718 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
85 | | elmapi 8431 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
87 | | fss 6505 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((1st ‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶ℤ) |
88 | 86, 44, 87 | sylancl 590 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶ℤ) |
89 | 88 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶ℤ) |
90 | | xp2nd 7719 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
91 | 82, 90 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
92 | | fvex 6664 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘(1st ‘𝑇)) ∈ V |
93 | | f1oeq1 6583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
94 | 92, 93 | elab 3586 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
95 | 91, 94 | sylib 221 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
96 | 95 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
97 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) |
98 | | xp2nd 7719 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd ‘𝑇) ∈ (0...𝑁)) |
99 | 80, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (2nd
‘𝑇) ∈ (0...𝑁)) |
100 | 99 | adantr 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) →
(2nd ‘𝑇)
∈ (0...𝑁)) |
101 | | eldifsn 4670 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘𝑇) ∈ ((0...𝑁) ∖ {(2nd ‘𝑧)}) ↔ ((2nd
‘𝑇) ∈ (0...𝑁) ∧ (2nd
‘𝑇) ≠
(2nd ‘𝑧))) |
102 | 101 | biimpri 231 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2nd ‘𝑇) ∈ (0...𝑁) ∧ (2nd ‘𝑇) ≠ (2nd
‘𝑧)) →
(2nd ‘𝑇)
∈ ((0...𝑁) ∖
{(2nd ‘𝑧)})) |
103 | 100, 102 | sylan 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → (2nd ‘𝑇) ∈ ((0...𝑁) ∖ {(2nd ‘𝑧)})) |
104 | 57, 77, 89, 96, 97, 103 | poimirlem2 35324 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛)) |
105 | 104 | ex 417 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) →
((2nd ‘𝑇)
≠ (2nd ‘𝑧) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛))) |
106 | 105 | necon1bd 2967 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) →
(¬ ∃*𝑛 ∈
(1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛) → (2nd ‘𝑇) = (2nd ‘𝑧))) |
107 | 106 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛) → (2nd ‘𝑇) = (2nd ‘𝑧))) |
108 | 56, 107 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd
‘𝑇) = (2nd
‘𝑧)) |
109 | 108 | neeq1d 3008 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → ((2nd
‘𝑇) ≠ 0 ↔
(2nd ‘𝑧)
≠ 0)) |
110 | 109 | exbiri 811 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → ((2nd
‘𝑧) ≠ 0 →
(2nd ‘𝑇)
≠ 0))) |
111 | 14, 110 | mpdi 45 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑇) ≠
0)) |
112 | 111 | necon2bd 2965 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑇) = 0 → ¬
(2nd ‘𝑧)
∈ (1...(𝑁 −
1)))) |
113 | 8, 112 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) |
114 | | xp2nd 7719 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd ‘𝑧) ∈ (0...𝑁)) |
115 | 36, 114 | syl 17 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑆 → (2nd ‘𝑧) ∈ (0...𝑁)) |
116 | 1 | nncnd 11675 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℂ) |
117 | | npcan1 11088 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
119 | | nnuz 12306 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℕ =
(ℤ≥‘1) |
120 | 1, 119 | eleqtrdi 2861 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
121 | 118, 120 | eqeltrd 2851 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘1)) |
122 | 1 | nnzd 12110 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℤ) |
123 | | peano2zm 12049 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
124 | 122, 123 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
125 | | uzid 12282 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
126 | | peano2uz 12326 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
127 | 124, 125,
126 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
128 | 118, 127 | eqeltrrd 2852 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
129 | | fzsplit2 12966 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
130 | 121, 128,
129 | syl2anc 588 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
131 | 118 | oveq1d 7158 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁)) |
132 | | fzsn 12983 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁}) |
133 | 122, 132 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑁...𝑁) = {𝑁}) |
134 | 131, 133 | eqtrd 2794 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁}) |
135 | 134 | uneq2d 4064 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
136 | 130, 135 | eqtrd 2794 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
137 | 136 | eleq2d 2836 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘𝑧) ∈ (1...𝑁) ↔ (2nd
‘𝑧) ∈
((1...(𝑁 − 1)) ∪
{𝑁}))) |
138 | 137 | notbid 322 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (¬ (2nd
‘𝑧) ∈ (1...𝑁) ↔ ¬ (2nd
‘𝑧) ∈
((1...(𝑁 − 1)) ∪
{𝑁}))) |
139 | | ioran 982 |
. . . . . . . . . . . . . 14
⊢ (¬
((2nd ‘𝑧)
∈ (1...(𝑁 − 1))
∨ (2nd ‘𝑧) = 𝑁) ↔ (¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd
‘𝑧) = 𝑁)) |
140 | | elun 4050 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd
‘𝑧) ∈ {𝑁})) |
141 | | fvex 6664 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘𝑧) ∈ V |
142 | 141 | elsn 4530 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘𝑧) ∈ {𝑁} ↔ (2nd ‘𝑧) = 𝑁) |
143 | 142 | orbi2i 911 |
. . . . . . . . . . . . . . 15
⊢
(((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd
‘𝑧) ∈ {𝑁}) ↔ ((2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∨
(2nd ‘𝑧) =
𝑁)) |
144 | 140, 143 | bitri 278 |
. . . . . . . . . . . . . 14
⊢
((2nd ‘𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd
‘𝑧) = 𝑁)) |
145 | 139, 144 | xchnxbir 337 |
. . . . . . . . . . . . 13
⊢ (¬
(2nd ‘𝑧)
∈ ((1...(𝑁 − 1))
∪ {𝑁}) ↔ (¬
(2nd ‘𝑧)
∈ (1...(𝑁 − 1))
∧ ¬ (2nd ‘𝑧) = 𝑁)) |
146 | 138, 145 | syl6bb 291 |
. . . . . . . . . . . 12
⊢ (𝜑 → (¬ (2nd
‘𝑧) ∈ (1...𝑁) ↔ (¬ (2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∧
¬ (2nd ‘𝑧) = 𝑁))) |
147 | 146 | anbi2d 632 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2nd
‘𝑧) ∈ (0...𝑁) ∧ ¬ (2nd
‘𝑧) ∈ (1...𝑁)) ↔ ((2nd
‘𝑧) ∈ (0...𝑁) ∧ (¬ (2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∧
¬ (2nd ‘𝑧) = 𝑁)))) |
148 | 1 | nnnn0d 11979 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
149 | | nn0uz 12305 |
. . . . . . . . . . . . . . . . 17
⊢
ℕ0 = (ℤ≥‘0) |
150 | 148, 149 | eleqtrdi 2861 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
151 | | fzpred 12989 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘0) → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁))) |
152 | 150, 151 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁))) |
153 | 152 | difeq1d 4023 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((0...𝑁) ∖ (1...𝑁)) = (({0} ∪ ((0 + 1)...𝑁)) ∖ (1...𝑁))) |
154 | | difun2 4370 |
. . . . . . . . . . . . . . 15
⊢ (({0}
∪ (1...𝑁)) ∖
(1...𝑁)) = ({0} ∖
(1...𝑁)) |
155 | | 0p1e1 11781 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 + 1) =
1 |
156 | 155 | oveq1i 7153 |
. . . . . . . . . . . . . . . . 17
⊢ ((0 +
1)...𝑁) = (1...𝑁) |
157 | 156 | uneq2i 4061 |
. . . . . . . . . . . . . . . 16
⊢ ({0}
∪ ((0 + 1)...𝑁)) = ({0}
∪ (1...𝑁)) |
158 | 157 | difeq1i 4020 |
. . . . . . . . . . . . . . 15
⊢ (({0}
∪ ((0 + 1)...𝑁))
∖ (1...𝑁)) = (({0}
∪ (1...𝑁)) ∖
(1...𝑁)) |
159 | | incom 4102 |
. . . . . . . . . . . . . . . . 17
⊢ ({0}
∩ (1...𝑁)) =
((1...𝑁) ∩
{0}) |
160 | | elfznn 12970 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
(1...𝑁) → 0 ∈
ℕ) |
161 | 9, 160 | mto 200 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬ 0
∈ (1...𝑁) |
162 | | disjsn 4597 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1...𝑁) ∩ {0})
= ∅ ↔ ¬ 0 ∈ (1...𝑁)) |
163 | 161, 162 | mpbir 234 |
. . . . . . . . . . . . . . . . 17
⊢
((1...𝑁) ∩ {0})
= ∅ |
164 | 159, 163 | eqtri 2782 |
. . . . . . . . . . . . . . . 16
⊢ ({0}
∩ (1...𝑁)) =
∅ |
165 | | disj3 4343 |
. . . . . . . . . . . . . . . 16
⊢ (({0}
∩ (1...𝑁)) = ∅
↔ {0} = ({0} ∖ (1...𝑁))) |
166 | 164, 165 | mpbi 233 |
. . . . . . . . . . . . . . 15
⊢ {0} =
({0} ∖ (1...𝑁)) |
167 | 154, 158,
166 | 3eqtr4i 2792 |
. . . . . . . . . . . . . 14
⊢ (({0}
∪ ((0 + 1)...𝑁))
∖ (1...𝑁)) =
{0} |
168 | 153, 167 | eqtrdi 2810 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((0...𝑁) ∖ (1...𝑁)) = {0}) |
169 | 168 | eleq2d 2836 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2nd
‘𝑧) ∈
((0...𝑁) ∖ (1...𝑁)) ↔ (2nd
‘𝑧) ∈
{0})) |
170 | | eldif 3864 |
. . . . . . . . . . . 12
⊢
((2nd ‘𝑧) ∈ ((0...𝑁) ∖ (1...𝑁)) ↔ ((2nd ‘𝑧) ∈ (0...𝑁) ∧ ¬ (2nd ‘𝑧) ∈ (1...𝑁))) |
171 | 141 | elsn 4530 |
. . . . . . . . . . . 12
⊢
((2nd ‘𝑧) ∈ {0} ↔ (2nd
‘𝑧) =
0) |
172 | 169, 170,
171 | 3bitr3g 317 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2nd
‘𝑧) ∈ (0...𝑁) ∧ ¬ (2nd
‘𝑧) ∈ (1...𝑁)) ↔ (2nd
‘𝑧) =
0)) |
173 | 147, 172 | bitr3d 284 |
. . . . . . . . . 10
⊢ (𝜑 → (((2nd
‘𝑧) ∈ (0...𝑁) ∧ (¬ (2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∧
¬ (2nd ‘𝑧) = 𝑁)) ↔ (2nd ‘𝑧) = 0)) |
174 | 173 | biimpd 232 |
. . . . . . . . 9
⊢ (𝜑 → (((2nd
‘𝑧) ∈ (0...𝑁) ∧ (¬ (2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∧
¬ (2nd ‘𝑧) = 𝑁)) → (2nd ‘𝑧) = 0)) |
175 | 174 | expdimp 457 |
. . . . . . . 8
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈ (0...𝑁)) → ((¬
(2nd ‘𝑧)
∈ (1...(𝑁 − 1))
∧ ¬ (2nd ‘𝑧) = 𝑁) → (2nd ‘𝑧) = 0)) |
176 | 115, 175 | sylan2 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((¬ (2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∧
¬ (2nd ‘𝑧) = 𝑁) → (2nd ‘𝑧) = 0)) |
177 | 113, 176 | mpand 695 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ (2nd ‘𝑧) = 𝑁 → (2nd ‘𝑧) = 0)) |
178 | 1, 2, 3 | poimirlem13 35335 |
. . . . . . . . . 10
⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 0) |
179 | | fveqeq2 6660 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑠 → ((2nd ‘𝑧) = 0 ↔ (2nd
‘𝑠) =
0)) |
180 | 179 | rmo4 3641 |
. . . . . . . . . 10
⊢
(∃*𝑧 ∈
𝑆 (2nd
‘𝑧) = 0 ↔
∀𝑧 ∈ 𝑆 ∀𝑠 ∈ 𝑆 (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑠) = 0) → 𝑧 = 𝑠)) |
181 | 178, 180 | sylib 221 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 ∀𝑠 ∈ 𝑆 (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑠) = 0) → 𝑧 = 𝑠)) |
182 | 181 | r19.21bi 3135 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ∀𝑠 ∈ 𝑆 (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑠) = 0) → 𝑧 = 𝑠)) |
183 | 4 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑇 ∈ 𝑆) |
184 | | fveqeq2 6660 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑇 → ((2nd ‘𝑠) = 0 ↔ (2nd
‘𝑇) =
0)) |
185 | 184 | anbi2d 632 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑇 → (((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑠) = 0) ↔
((2nd ‘𝑧)
= 0 ∧ (2nd ‘𝑇) = 0))) |
186 | | eqeq2 2771 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑇 → (𝑧 = 𝑠 ↔ 𝑧 = 𝑇)) |
187 | 185, 186 | imbi12d 349 |
. . . . . . . . 9
⊢ (𝑠 = 𝑇 → ((((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑠) = 0) → 𝑧 = 𝑠) ↔ (((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑇) = 0) → 𝑧 = 𝑇))) |
188 | 187 | rspccv 3536 |
. . . . . . . 8
⊢
(∀𝑠 ∈
𝑆 (((2nd
‘𝑧) = 0 ∧
(2nd ‘𝑠) =
0) → 𝑧 = 𝑠) → (𝑇 ∈ 𝑆 → (((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑇) = 0) → 𝑧 = 𝑇))) |
189 | 182, 183,
188 | sylc 65 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑇) = 0) → 𝑧 = 𝑇)) |
190 | 8, 189 | mpan2d 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑧) = 0 → 𝑧 = 𝑇)) |
191 | 177, 190 | syld 47 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ (2nd ‘𝑧) = 𝑁 → 𝑧 = 𝑇)) |
192 | 191 | necon1ad 2966 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (2nd ‘𝑧) = 𝑁)) |
193 | 192 | ralrimiva 3111 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ 𝑇 → (2nd ‘𝑧) = 𝑁)) |
194 | 1, 2, 3 | poimirlem14 35336 |
. . 3
⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 𝑁) |
195 | | rmoim 3651 |
. . 3
⊢
(∀𝑧 ∈
𝑆 (𝑧 ≠ 𝑇 → (2nd ‘𝑧) = 𝑁) → (∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 𝑁 → ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)) |
196 | 193, 194,
195 | sylc 65 |
. 2
⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
197 | | reu5 3338 |
. 2
⊢
(∃!𝑧 ∈
𝑆 𝑧 ≠ 𝑇 ↔ (∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 ∧ ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)) |
198 | 7, 196, 197 | sylanbrc 587 |
1
⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |