Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | | poimirlem22.s |
. . 3
⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
3 | | poimirlem22.1 |
. . 3
⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (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 33426 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
8 | 6 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (2nd ‘𝑇) = 0) |
9 | | 0nnn 11052 |
. . . . . . . . . . . . 13
⊢ ¬ 0
∈ ℕ |
10 | | elfznn 12370 |
. . . . . . . . . . . . 13
⊢ (0 ∈
(1...(𝑁 − 1)) →
0 ∈ ℕ) |
11 | 9, 10 | mto 188 |
. . . . . . . . . . . 12
⊢ ¬ 0
∈ (1...(𝑁 −
1)) |
12 | | eleq1 2689 |
. . . . . . . . . . . 12
⊢
((2nd ‘𝑧) = 0 → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ 0 ∈ (1...(𝑁 − 1)))) |
13 | 11, 12 | mtbiri 317 |
. . . . . . . . . . 11
⊢
((2nd ‘𝑧) = 0 → ¬ (2nd
‘𝑧) ∈
(1...(𝑁 −
1))) |
14 | 13 | necon2ai 2823 |
. . . . . . . . . 10
⊢
((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑧) ≠
0) |
15 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ) |
16 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (2nd ‘𝑡) = (2nd ‘𝑧)) |
17 | 16 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑧))) |
18 | 17 | ifbid 4108 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑧 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑧), 𝑦, (𝑦 + 1))) |
19 | 18 | csbeq1d 3540 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
20 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (1st ‘𝑡) = (1st ‘𝑧)) |
21 | 20 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑧))) |
22 | 20 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑧 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑧))) |
23 | 22 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑧)) “
(1...𝑗))) |
24 | 23 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1})) |
25 | 22 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑧)) “ ((𝑗 + 1)...𝑁))) |
26 | 25 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) |
27 | 24, 26 | uneq12d 3768 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
28 | 21, 27 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑧 → ((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑧)) ∘𝑓 +
((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
29 | 28 | csbeq2dv 3992 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2nd ‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘𝑓 +
((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
30 | 19, 29 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑧 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘𝑓 +
((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
31 | 30 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑧 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘𝑓 +
((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
32 | 31 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑧 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘𝑓 +
((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
33 | 32, 2 | elrab2 3366 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 ↔ (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘𝑓 +
((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
34 | 33 | simprbi 480 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘𝑓 +
((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
35 | 34 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘𝑓 +
((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
36 | | elrabi 3359 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑧 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
37 | 36, 2 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
38 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑧) ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑆 → (1st ‘𝑧) ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
40 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . 18
⊢
((1st ‘𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → (1st
‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
42 | | elmapi 7879 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾)) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾)) |
44 | | elfzoelz 12470 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ) |
45 | 44 | ssriv 3607 |
. . . . . . . . . . . . . . . 16
⊢
(0..^𝐾) ⊆
ℤ |
46 | | fss 6056 |
. . . . . . . . . . . . . . . 16
⊢
(((1st ‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶ℤ) |
47 | 43, 45, 46 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶ℤ) |
48 | 47 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶ℤ) |
49 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
50 | 39, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
51 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘(1st ‘𝑧)) ∈ V |
52 | | f1oeq1 6127 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (2nd
‘(1st ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))) |
53 | 51, 52 | elab 3350 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
54 | 50, 53 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
55 | 54 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
56 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd
‘𝑧) ∈
(1...(𝑁 −
1))) |
57 | 15, 35, 48, 55, 56 | poimirlem1 33410 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛)) |
58 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → 𝑁 ∈ ℕ) |
59 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
60 | 59 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) |
61 | 60 | ifbid 4108 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) |
62 | 61 | csbeq1d 3540 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
63 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑇 → (1st ‘𝑡) = (1st ‘𝑇)) |
64 | 63 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
65 | 63 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) |
66 | 65 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑗))) |
67 | 66 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1})) |
68 | 65 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
69 | 68 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
70 | 67, 69 | uneq12d 3768 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑇 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
71 | 64, 70 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
72 | 71 | csbeq2dv 3992 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
73 | 62, 72 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
74 | 73 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
75 | 74 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
76 | 75, 2 | elrab2 3366 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
77 | 76 | simprbi 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
78 | 4, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
79 | 78 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
80 | | elrabi 3359 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
81 | 80, 2 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
82 | 4, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
83 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑇 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (1st
‘𝑇) ∈
(((0..^𝐾)
↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
85 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
87 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
89 | | fss 6056 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((1st ‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶ℤ) |
90 | 88, 45, 89 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶ℤ) |
91 | 90 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶ℤ) |
92 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
93 | 84, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
94 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘(1st ‘𝑇)) ∈ V |
95 | | f1oeq1 6127 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
96 | 94, 95 | elab 3350 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
97 | 93, 96 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
98 | 97 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
99 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) |
100 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd ‘𝑇) ∈ (0...𝑁)) |
101 | 82, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (2nd
‘𝑇) ∈ (0...𝑁)) |
102 | 101 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) →
(2nd ‘𝑇)
∈ (0...𝑁)) |
103 | | eldifsn 4317 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘𝑇) ∈ ((0...𝑁) ∖ {(2nd ‘𝑧)}) ↔ ((2nd
‘𝑇) ∈ (0...𝑁) ∧ (2nd
‘𝑇) ≠
(2nd ‘𝑧))) |
104 | 103 | biimpri 218 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2nd ‘𝑇) ∈ (0...𝑁) ∧ (2nd ‘𝑇) ≠ (2nd
‘𝑧)) →
(2nd ‘𝑇)
∈ ((0...𝑁) ∖
{(2nd ‘𝑧)})) |
105 | 102, 104 | sylan 488 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → (2nd ‘𝑇) ∈ ((0...𝑁) ∖ {(2nd ‘𝑧)})) |
106 | 58, 79, 91, 98, 99, 105 | poimirlem2 33411 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛)) |
107 | 106 | ex 450 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) →
((2nd ‘𝑇)
≠ (2nd ‘𝑧) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛))) |
108 | 107 | necon1bd 2812 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) →
(¬ ∃*𝑛 ∈
(1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛) → (2nd ‘𝑇) = (2nd ‘𝑧))) |
109 | 108 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛) → (2nd ‘𝑇) = (2nd ‘𝑧))) |
110 | 57, 109 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd
‘𝑇) = (2nd
‘𝑧)) |
111 | 110 | neeq1d 2853 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → ((2nd
‘𝑇) ≠ 0 ↔
(2nd ‘𝑧)
≠ 0)) |
112 | 111 | exbiri 652 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → ((2nd
‘𝑧) ≠ 0 →
(2nd ‘𝑇)
≠ 0))) |
113 | 14, 112 | mpdi 45 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑇) ≠
0)) |
114 | 113 | necon2bd 2810 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑇) = 0 → ¬
(2nd ‘𝑧)
∈ (1...(𝑁 −
1)))) |
115 | 8, 114 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) |
116 | | xp2nd 7199 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd ‘𝑧) ∈ (0...𝑁)) |
117 | 37, 116 | syl 17 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑆 → (2nd ‘𝑧) ∈ (0...𝑁)) |
118 | 1 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℂ) |
119 | | npcan1 10455 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
121 | | nnuz 11723 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℕ =
(ℤ≥‘1) |
122 | 1, 121 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
123 | 120, 122 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘1)) |
124 | 1 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℤ) |
125 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
126 | 124, 125 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
127 | | uzid 11702 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
128 | | peano2uz 11741 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
129 | 126, 127,
128 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
130 | 120, 129 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
131 | | fzsplit2 12366 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
132 | 123, 130,
131 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
133 | 120 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁)) |
134 | | fzsn 12383 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁}) |
135 | 124, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑁...𝑁) = {𝑁}) |
136 | 133, 135 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁}) |
137 | 136 | uneq2d 3767 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
138 | 132, 137 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
139 | 138 | eleq2d 2687 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘𝑧) ∈ (1...𝑁) ↔ (2nd
‘𝑧) ∈
((1...(𝑁 − 1)) ∪
{𝑁}))) |
140 | 139 | notbid 308 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (¬ (2nd
‘𝑧) ∈ (1...𝑁) ↔ ¬ (2nd
‘𝑧) ∈
((1...(𝑁 − 1)) ∪
{𝑁}))) |
141 | | ioran 511 |
. . . . . . . . . . . . . 14
⊢ (¬
((2nd ‘𝑧)
∈ (1...(𝑁 − 1))
∨ (2nd ‘𝑧) = 𝑁) ↔ (¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd
‘𝑧) = 𝑁)) |
142 | | elun 3753 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd
‘𝑧) ∈ {𝑁})) |
143 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘𝑧) ∈ V |
144 | 143 | elsn 4192 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘𝑧) ∈ {𝑁} ↔ (2nd ‘𝑧) = 𝑁) |
145 | 144 | orbi2i 541 |
. . . . . . . . . . . . . . 15
⊢
(((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd
‘𝑧) ∈ {𝑁}) ↔ ((2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∨
(2nd ‘𝑧) =
𝑁)) |
146 | 142, 145 | bitri 264 |
. . . . . . . . . . . . . 14
⊢
((2nd ‘𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd
‘𝑧) = 𝑁)) |
147 | 141, 146 | xchnxbir 323 |
. . . . . . . . . . . . 13
⊢ (¬
(2nd ‘𝑧)
∈ ((1...(𝑁 − 1))
∪ {𝑁}) ↔ (¬
(2nd ‘𝑧)
∈ (1...(𝑁 − 1))
∧ ¬ (2nd ‘𝑧) = 𝑁)) |
148 | 140, 147 | syl6bb 276 |
. . . . . . . . . . . 12
⊢ (𝜑 → (¬ (2nd
‘𝑧) ∈ (1...𝑁) ↔ (¬ (2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∧
¬ (2nd ‘𝑧) = 𝑁))) |
149 | 148 | anbi2d 740 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2nd
‘𝑧) ∈ (0...𝑁) ∧ ¬ (2nd
‘𝑧) ∈ (1...𝑁)) ↔ ((2nd
‘𝑧) ∈ (0...𝑁) ∧ (¬ (2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∧
¬ (2nd ‘𝑧) = 𝑁)))) |
150 | 1 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
151 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . 17
⊢
ℕ0 = (ℤ≥‘0) |
152 | 150, 151 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
153 | | fzpred 12389 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘0) → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁))) |
154 | 152, 153 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁))) |
155 | 154 | difeq1d 3727 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((0...𝑁) ∖ (1...𝑁)) = (({0} ∪ ((0 + 1)...𝑁)) ∖ (1...𝑁))) |
156 | | difun2 4048 |
. . . . . . . . . . . . . . 15
⊢ (({0}
∪ (1...𝑁)) ∖
(1...𝑁)) = ({0} ∖
(1...𝑁)) |
157 | | 0p1e1 11132 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 + 1) =
1 |
158 | 157 | oveq1i 6660 |
. . . . . . . . . . . . . . . . 17
⊢ ((0 +
1)...𝑁) = (1...𝑁) |
159 | 158 | uneq2i 3764 |
. . . . . . . . . . . . . . . 16
⊢ ({0}
∪ ((0 + 1)...𝑁)) = ({0}
∪ (1...𝑁)) |
160 | 159 | difeq1i 3724 |
. . . . . . . . . . . . . . 15
⊢ (({0}
∪ ((0 + 1)...𝑁))
∖ (1...𝑁)) = (({0}
∪ (1...𝑁)) ∖
(1...𝑁)) |
161 | | incom 3805 |
. . . . . . . . . . . . . . . . 17
⊢ ({0}
∩ (1...𝑁)) =
((1...𝑁) ∩
{0}) |
162 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
(1...𝑁) → 0 ∈
ℕ) |
163 | 9, 162 | mto 188 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬ 0
∈ (1...𝑁) |
164 | | disjsn 4246 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1...𝑁) ∩ {0})
= ∅ ↔ ¬ 0 ∈ (1...𝑁)) |
165 | 163, 164 | mpbir 221 |
. . . . . . . . . . . . . . . . 17
⊢
((1...𝑁) ∩ {0})
= ∅ |
166 | 161, 165 | eqtri 2644 |
. . . . . . . . . . . . . . . 16
⊢ ({0}
∩ (1...𝑁)) =
∅ |
167 | | disj3 4021 |
. . . . . . . . . . . . . . . 16
⊢ (({0}
∩ (1...𝑁)) = ∅
↔ {0} = ({0} ∖ (1...𝑁))) |
168 | 166, 167 | mpbi 220 |
. . . . . . . . . . . . . . 15
⊢ {0} =
({0} ∖ (1...𝑁)) |
169 | 156, 160,
168 | 3eqtr4i 2654 |
. . . . . . . . . . . . . 14
⊢ (({0}
∪ ((0 + 1)...𝑁))
∖ (1...𝑁)) =
{0} |
170 | 155, 169 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((0...𝑁) ∖ (1...𝑁)) = {0}) |
171 | 170 | eleq2d 2687 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2nd
‘𝑧) ∈
((0...𝑁) ∖ (1...𝑁)) ↔ (2nd
‘𝑧) ∈
{0})) |
172 | | eldif 3584 |
. . . . . . . . . . . 12
⊢
((2nd ‘𝑧) ∈ ((0...𝑁) ∖ (1...𝑁)) ↔ ((2nd ‘𝑧) ∈ (0...𝑁) ∧ ¬ (2nd ‘𝑧) ∈ (1...𝑁))) |
173 | 143 | elsn 4192 |
. . . . . . . . . . . 12
⊢
((2nd ‘𝑧) ∈ {0} ↔ (2nd
‘𝑧) =
0) |
174 | 171, 172,
173 | 3bitr3g 302 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2nd
‘𝑧) ∈ (0...𝑁) ∧ ¬ (2nd
‘𝑧) ∈ (1...𝑁)) ↔ (2nd
‘𝑧) =
0)) |
175 | 149, 174 | bitr3d 270 |
. . . . . . . . . 10
⊢ (𝜑 → (((2nd
‘𝑧) ∈ (0...𝑁) ∧ (¬ (2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∧
¬ (2nd ‘𝑧) = 𝑁)) ↔ (2nd ‘𝑧) = 0)) |
176 | 175 | biimpd 219 |
. . . . . . . . 9
⊢ (𝜑 → (((2nd
‘𝑧) ∈ (0...𝑁) ∧ (¬ (2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∧
¬ (2nd ‘𝑧) = 𝑁)) → (2nd ‘𝑧) = 0)) |
177 | 176 | expdimp 453 |
. . . . . . . 8
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈ (0...𝑁)) → ((¬
(2nd ‘𝑧)
∈ (1...(𝑁 − 1))
∧ ¬ (2nd ‘𝑧) = 𝑁) → (2nd ‘𝑧) = 0)) |
178 | 117, 177 | sylan2 491 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((¬ (2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∧
¬ (2nd ‘𝑧) = 𝑁) → (2nd ‘𝑧) = 0)) |
179 | 115, 178 | mpand 711 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ (2nd ‘𝑧) = 𝑁 → (2nd ‘𝑧) = 0)) |
180 | 1, 2, 3 | poimirlem13 33422 |
. . . . . . . . . 10
⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 0) |
181 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑠 → (2nd ‘𝑧) = (2nd ‘𝑠)) |
182 | 181 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑠 → ((2nd ‘𝑧) = 0 ↔ (2nd
‘𝑠) =
0)) |
183 | 182 | rmo4 3399 |
. . . . . . . . . 10
⊢
(∃*𝑧 ∈
𝑆 (2nd
‘𝑧) = 0 ↔
∀𝑧 ∈ 𝑆 ∀𝑠 ∈ 𝑆 (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑠) = 0) → 𝑧 = 𝑠)) |
184 | 180, 183 | sylib 208 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 ∀𝑠 ∈ 𝑆 (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑠) = 0) → 𝑧 = 𝑠)) |
185 | 184 | r19.21bi 2932 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ∀𝑠 ∈ 𝑆 (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑠) = 0) → 𝑧 = 𝑠)) |
186 | 4 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑇 ∈ 𝑆) |
187 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑇 → (2nd ‘𝑠) = (2nd ‘𝑇)) |
188 | 187 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑇 → ((2nd ‘𝑠) = 0 ↔ (2nd
‘𝑇) =
0)) |
189 | 188 | anbi2d 740 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑇 → (((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑠) = 0) ↔
((2nd ‘𝑧)
= 0 ∧ (2nd ‘𝑇) = 0))) |
190 | | eqeq2 2633 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑇 → (𝑧 = 𝑠 ↔ 𝑧 = 𝑇)) |
191 | 189, 190 | imbi12d 334 |
. . . . . . . . 9
⊢ (𝑠 = 𝑇 → ((((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑠) = 0) → 𝑧 = 𝑠) ↔ (((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑇) = 0) → 𝑧 = 𝑇))) |
192 | 191 | rspccv 3306 |
. . . . . . . 8
⊢
(∀𝑠 ∈
𝑆 (((2nd
‘𝑧) = 0 ∧
(2nd ‘𝑠) =
0) → 𝑧 = 𝑠) → (𝑇 ∈ 𝑆 → (((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑇) = 0) → 𝑧 = 𝑇))) |
193 | 185, 186,
192 | sylc 65 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑇) = 0) → 𝑧 = 𝑇)) |
194 | 8, 193 | mpan2d 710 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑧) = 0 → 𝑧 = 𝑇)) |
195 | 179, 194 | syld 47 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ (2nd ‘𝑧) = 𝑁 → 𝑧 = 𝑇)) |
196 | 195 | necon1ad 2811 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (2nd ‘𝑧) = 𝑁)) |
197 | 196 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ 𝑇 → (2nd ‘𝑧) = 𝑁)) |
198 | 1, 2, 3 | poimirlem14 33423 |
. . 3
⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 𝑁) |
199 | | rmoim 3407 |
. . 3
⊢
(∀𝑧 ∈
𝑆 (𝑧 ≠ 𝑇 → (2nd ‘𝑧) = 𝑁) → (∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 𝑁 → ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)) |
200 | 197, 198,
199 | sylc 65 |
. 2
⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
201 | | reu5 3159 |
. 2
⊢
(∃!𝑧 ∈
𝑆 𝑧 ≠ 𝑇 ↔ (∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 ∧ ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)) |
202 | 7, 200, 201 | sylanbrc 698 |
1
⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |