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 37338 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
8 | 6 | adantr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (2nd ‘𝑇) = 0) |
9 | | 0nnn 12300 |
. . . . . . . . . . . . 13
⊢ ¬ 0
∈ ℕ |
10 | | elfznn 13584 |
. . . . . . . . . . . . 13
⊢ (0 ∈
(1...(𝑁 − 1)) →
0 ∈ ℕ) |
11 | 9, 10 | mto 196 |
. . . . . . . . . . . 12
⊢ ¬ 0
∈ (1...(𝑁 −
1)) |
12 | | eleq1 2814 |
. . . . . . . . . . . 12
⊢
((2nd ‘𝑧) = 0 → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ 0 ∈ (1...(𝑁 − 1)))) |
13 | 11, 12 | mtbiri 326 |
. . . . . . . . . . 11
⊢
((2nd ‘𝑧) = 0 → ¬ (2nd
‘𝑧) ∈
(1...(𝑁 −
1))) |
14 | 13 | necon2ai 2960 |
. . . . . . . . . 10
⊢
((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑧) ≠
0) |
15 | 1 | ad2antrr 724 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ) |
16 | | fveq2 6901 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (2nd ‘𝑡) = (2nd ‘𝑧)) |
17 | 16 | breq2d 5165 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑧))) |
18 | 17 | ifbid 4556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑧 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑧), 𝑦, (𝑦 + 1))) |
19 | 18 | csbeq1d 3896 |
. . . . . . . . . . . . . . . . . . . 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 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑧))) |
21 | | 2fveq3 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑧 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑧))) |
22 | 21 | imaeq1d 6068 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑧)) “
(1...𝑗))) |
23 | 22 | xpeq1d 5711 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1})) |
24 | 21 | imaeq1d 6068 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑧)) “ ((𝑗 + 1)...𝑁))) |
25 | 24 | xpeq1d 5711 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) |
26 | 23, 25 | uneq12d 4164 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
27 | 20, 26 | oveq12d 7442 |
. . . . . . . . . . . . . . . . . . . . 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 3899 |
. . . . . . . . . . . . . . . . . . . 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 2766 |
. . . . . . . . . . . . . . . . . . 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 5255 |
. . . . . . . . . . . . . . . . . 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 2737 |
. . . . . . . . . . . . . . . . 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 3684 |
. . . . . . . . . . . . . . . 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 495 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘f + ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
34 | 33 | ad2antlr 725 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘f + ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
35 | | elrabi 3675 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ {𝑡 ∈ ((((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 2844 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
37 | | xp1st 8035 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
38 | | xp1st 8035 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
39 | | elmapi 8878 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾)) |
40 | 36, 37, 38, 39 | 4syl 19 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾)) |
41 | | elfzoelz 13686 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ) |
42 | 41 | ssriv 3983 |
. . . . . . . . . . . . . . . 16
⊢
(0..^𝐾) ⊆
ℤ |
43 | | fss 6744 |
. . . . . . . . . . . . . . . 16
⊢
(((1st ‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶ℤ) |
44 | 40, 42, 43 | sylancl 584 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶ℤ) |
45 | 44 | ad2antlr 725 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶ℤ) |
46 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → (1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
47 | | xp2nd 8036 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
49 | | fvex 6914 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘(1st ‘𝑧)) ∈ V |
50 | | f1oeq1 6831 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (2nd
‘(1st ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))) |
51 | 49, 50 | elab 3666 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
52 | 48, 51 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
53 | 52 | ad2antlr 725 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
54 | | simpr 483 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd
‘𝑧) ∈
(1...(𝑁 −
1))) |
55 | 15, 34, 45, 53, 54 | poimirlem1 37322 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛)) |
56 | 1 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → 𝑁 ∈ ℕ) |
57 | | fveq2 6901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
58 | 57 | breq2d 5165 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) |
59 | 58 | ifbid 4556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) |
60 | 59 | csbeq1d 3896 |
. . . . . . . . . . . . . . . . . . . . . . . 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})))) |
61 | | 2fveq3 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
62 | | 2fveq3 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) |
63 | 62 | imaeq1d 6068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑗))) |
64 | 63 | xpeq1d 5711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1})) |
65 | 62 | imaeq1d 6068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
66 | 65 | xpeq1d 5711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
67 | 64, 66 | uneq12d 4164 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑇 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
68 | 61, 67 | oveq12d 7442 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
69 | 68 | csbeq2dv 3899 |
. . . . . . . . . . . . . . . . . . . . . . . 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})))) |
70 | 60, 69 | eqtrd 2766 |
. . . . . . . . . . . . . . . . . . . . . . 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})))) |
71 | 70 | mpteq2dv 5255 |
. . . . . . . . . . . . . . . . . . . . . 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}))))) |
72 | 71 | eqeq2d 2737 |
. . . . . . . . . . . . . . . . . . . . 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})))))) |
73 | 72, 2 | elrab2 3684 |
. . . . . . . . . . . . . . . . . . . 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})))))) |
74 | 73 | simprbi 495 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
75 | 4, 74 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
76 | 75 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
77 | | elrabi 3675 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑇 ∈ {𝑡 ∈ ((((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...𝑁))) |
78 | 77, 2 | eleq2s 2844 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
79 | 4, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
80 | | xp1st 8035 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
81 | | xp1st 8035 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
82 | | elmapi 8878 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
83 | 79, 80, 81, 82 | 4syl 19 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
84 | | fss 6744 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((1st ‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶ℤ) |
85 | 83, 42, 84 | sylancl 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶ℤ) |
86 | 85 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶ℤ) |
87 | | xp2nd 8036 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
88 | 4, 78, 80, 87 | 4syl 19 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
89 | | fvex 6914 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘(1st ‘𝑇)) ∈ V |
90 | | f1oeq1 6831 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
91 | 89, 90 | elab 3666 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
92 | 88, 91 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
93 | 92 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
94 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) |
95 | | xp2nd 8036 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd ‘𝑇) ∈ (0...𝑁)) |
96 | 79, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (2nd
‘𝑇) ∈ (0...𝑁)) |
97 | 96 | adantr 479 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) →
(2nd ‘𝑇)
∈ (0...𝑁)) |
98 | | eldifsn 4795 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘𝑇) ∈ ((0...𝑁) ∖ {(2nd ‘𝑧)}) ↔ ((2nd
‘𝑇) ∈ (0...𝑁) ∧ (2nd
‘𝑇) ≠
(2nd ‘𝑧))) |
99 | 98 | biimpri 227 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2nd ‘𝑇) ∈ (0...𝑁) ∧ (2nd ‘𝑇) ≠ (2nd
‘𝑧)) →
(2nd ‘𝑇)
∈ ((0...𝑁) ∖
{(2nd ‘𝑧)})) |
100 | 97, 99 | sylan 578 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → (2nd ‘𝑇) ∈ ((0...𝑁) ∖ {(2nd ‘𝑧)})) |
101 | 56, 76, 86, 93, 94, 100 | poimirlem2 37323 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛)) |
102 | 101 | ex 411 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) →
((2nd ‘𝑇)
≠ (2nd ‘𝑧) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛))) |
103 | 102 | necon1bd 2948 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) →
(¬ ∃*𝑛 ∈
(1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛) → (2nd ‘𝑇) = (2nd ‘𝑧))) |
104 | 103 | adantlr 713 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛) → (2nd ‘𝑇) = (2nd ‘𝑧))) |
105 | 55, 104 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd
‘𝑇) = (2nd
‘𝑧)) |
106 | 105 | neeq1d 2990 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → ((2nd
‘𝑇) ≠ 0 ↔
(2nd ‘𝑧)
≠ 0)) |
107 | 106 | exbiri 809 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → ((2nd
‘𝑧) ≠ 0 →
(2nd ‘𝑇)
≠ 0))) |
108 | 14, 107 | mpdi 45 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑇) ≠
0)) |
109 | 108 | necon2bd 2946 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑇) = 0 → ¬
(2nd ‘𝑧)
∈ (1...(𝑁 −
1)))) |
110 | 8, 109 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) |
111 | | xp2nd 8036 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd ‘𝑧) ∈ (0...𝑁)) |
112 | 36, 111 | syl 17 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑆 → (2nd ‘𝑧) ∈ (0...𝑁)) |
113 | 1 | nncnd 12280 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℂ) |
114 | | npcan1 11689 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
116 | | nnuz 12917 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℕ =
(ℤ≥‘1) |
117 | 1, 116 | eleqtrdi 2836 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
118 | 115, 117 | eqeltrd 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘1)) |
119 | 1 | nnzd 12637 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℤ) |
120 | | peano2zm 12657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
121 | | uzid 12889 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
122 | | peano2uz 12937 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
123 | 119, 120,
121, 122 | 4syl 19 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
124 | 115, 123 | eqeltrrd 2827 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
125 | | fzsplit2 13580 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
126 | 118, 124,
125 | syl2anc 582 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
127 | 115 | oveq1d 7439 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁)) |
128 | | fzsn 13597 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁}) |
129 | 119, 128 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑁...𝑁) = {𝑁}) |
130 | 127, 129 | eqtrd 2766 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁}) |
131 | 130 | uneq2d 4163 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
132 | 126, 131 | eqtrd 2766 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1...𝑁) = ((1...(𝑁 − 1)) ∪ {𝑁})) |
133 | 132 | eleq2d 2812 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘𝑧) ∈ (1...𝑁) ↔ (2nd
‘𝑧) ∈
((1...(𝑁 − 1)) ∪
{𝑁}))) |
134 | 133 | notbid 317 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (¬ (2nd
‘𝑧) ∈ (1...𝑁) ↔ ¬ (2nd
‘𝑧) ∈
((1...(𝑁 − 1)) ∪
{𝑁}))) |
135 | | ioran 981 |
. . . . . . . . . . . . . 14
⊢ (¬
((2nd ‘𝑧)
∈ (1...(𝑁 − 1))
∨ (2nd ‘𝑧) = 𝑁) ↔ (¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∧ ¬ (2nd
‘𝑧) = 𝑁)) |
136 | | elun 4148 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd
‘𝑧) ∈ {𝑁})) |
137 | | fvex 6914 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘𝑧) ∈ V |
138 | 137 | elsn 4648 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘𝑧) ∈ {𝑁} ↔ (2nd ‘𝑧) = 𝑁) |
139 | 138 | orbi2i 910 |
. . . . . . . . . . . . . . 15
⊢
(((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd
‘𝑧) ∈ {𝑁}) ↔ ((2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∨
(2nd ‘𝑧) =
𝑁)) |
140 | 136, 139 | bitri 274 |
. . . . . . . . . . . . . 14
⊢
((2nd ‘𝑧) ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ∨ (2nd
‘𝑧) = 𝑁)) |
141 | 135, 140 | xchnxbir 332 |
. . . . . . . . . . . . 13
⊢ (¬
(2nd ‘𝑧)
∈ ((1...(𝑁 − 1))
∪ {𝑁}) ↔ (¬
(2nd ‘𝑧)
∈ (1...(𝑁 − 1))
∧ ¬ (2nd ‘𝑧) = 𝑁)) |
142 | 134, 141 | bitrdi 286 |
. . . . . . . . . . . 12
⊢ (𝜑 → (¬ (2nd
‘𝑧) ∈ (1...𝑁) ↔ (¬ (2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∧
¬ (2nd ‘𝑧) = 𝑁))) |
143 | 142 | anbi2d 628 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2nd
‘𝑧) ∈ (0...𝑁) ∧ ¬ (2nd
‘𝑧) ∈ (1...𝑁)) ↔ ((2nd
‘𝑧) ∈ (0...𝑁) ∧ (¬ (2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∧
¬ (2nd ‘𝑧) = 𝑁)))) |
144 | 1 | nnnn0d 12584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
145 | | nn0uz 12916 |
. . . . . . . . . . . . . . . . 17
⊢
ℕ0 = (ℤ≥‘0) |
146 | 144, 145 | eleqtrdi 2836 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
147 | | fzpred 13603 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘0) → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁))) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0...𝑁) = ({0} ∪ ((0 + 1)...𝑁))) |
149 | 148 | difeq1d 4120 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((0...𝑁) ∖ (1...𝑁)) = (({0} ∪ ((0 + 1)...𝑁)) ∖ (1...𝑁))) |
150 | | difun2 4485 |
. . . . . . . . . . . . . . 15
⊢ (({0}
∪ (1...𝑁)) ∖
(1...𝑁)) = ({0} ∖
(1...𝑁)) |
151 | | 0p1e1 12386 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 + 1) =
1 |
152 | 151 | oveq1i 7434 |
. . . . . . . . . . . . . . . . 17
⊢ ((0 +
1)...𝑁) = (1...𝑁) |
153 | 152 | uneq2i 4160 |
. . . . . . . . . . . . . . . 16
⊢ ({0}
∪ ((0 + 1)...𝑁)) = ({0}
∪ (1...𝑁)) |
154 | 153 | difeq1i 4117 |
. . . . . . . . . . . . . . 15
⊢ (({0}
∪ ((0 + 1)...𝑁))
∖ (1...𝑁)) = (({0}
∪ (1...𝑁)) ∖
(1...𝑁)) |
155 | | incom 4202 |
. . . . . . . . . . . . . . . . 17
⊢ ({0}
∩ (1...𝑁)) =
((1...𝑁) ∩
{0}) |
156 | | elfznn 13584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
(1...𝑁) → 0 ∈
ℕ) |
157 | 9, 156 | mto 196 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬ 0
∈ (1...𝑁) |
158 | | disjsn 4720 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1...𝑁) ∩ {0})
= ∅ ↔ ¬ 0 ∈ (1...𝑁)) |
159 | 157, 158 | mpbir 230 |
. . . . . . . . . . . . . . . . 17
⊢
((1...𝑁) ∩ {0})
= ∅ |
160 | 155, 159 | eqtri 2754 |
. . . . . . . . . . . . . . . 16
⊢ ({0}
∩ (1...𝑁)) =
∅ |
161 | | disj3 4458 |
. . . . . . . . . . . . . . . 16
⊢ (({0}
∩ (1...𝑁)) = ∅
↔ {0} = ({0} ∖ (1...𝑁))) |
162 | 160, 161 | mpbi 229 |
. . . . . . . . . . . . . . 15
⊢ {0} =
({0} ∖ (1...𝑁)) |
163 | 150, 154,
162 | 3eqtr4i 2764 |
. . . . . . . . . . . . . 14
⊢ (({0}
∪ ((0 + 1)...𝑁))
∖ (1...𝑁)) =
{0} |
164 | 149, 163 | eqtrdi 2782 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((0...𝑁) ∖ (1...𝑁)) = {0}) |
165 | 164 | eleq2d 2812 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2nd
‘𝑧) ∈
((0...𝑁) ∖ (1...𝑁)) ↔ (2nd
‘𝑧) ∈
{0})) |
166 | | eldif 3957 |
. . . . . . . . . . . 12
⊢
((2nd ‘𝑧) ∈ ((0...𝑁) ∖ (1...𝑁)) ↔ ((2nd ‘𝑧) ∈ (0...𝑁) ∧ ¬ (2nd ‘𝑧) ∈ (1...𝑁))) |
167 | 137 | elsn 4648 |
. . . . . . . . . . . 12
⊢
((2nd ‘𝑧) ∈ {0} ↔ (2nd
‘𝑧) =
0) |
168 | 165, 166,
167 | 3bitr3g 312 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2nd
‘𝑧) ∈ (0...𝑁) ∧ ¬ (2nd
‘𝑧) ∈ (1...𝑁)) ↔ (2nd
‘𝑧) =
0)) |
169 | 143, 168 | bitr3d 280 |
. . . . . . . . . 10
⊢ (𝜑 → (((2nd
‘𝑧) ∈ (0...𝑁) ∧ (¬ (2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∧
¬ (2nd ‘𝑧) = 𝑁)) ↔ (2nd ‘𝑧) = 0)) |
170 | 169 | biimpd 228 |
. . . . . . . . 9
⊢ (𝜑 → (((2nd
‘𝑧) ∈ (0...𝑁) ∧ (¬ (2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∧
¬ (2nd ‘𝑧) = 𝑁)) → (2nd ‘𝑧) = 0)) |
171 | 170 | expdimp 451 |
. . . . . . . 8
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈ (0...𝑁)) → ((¬
(2nd ‘𝑧)
∈ (1...(𝑁 − 1))
∧ ¬ (2nd ‘𝑧) = 𝑁) → (2nd ‘𝑧) = 0)) |
172 | 112, 171 | sylan2 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((¬ (2nd
‘𝑧) ∈
(1...(𝑁 − 1)) ∧
¬ (2nd ‘𝑧) = 𝑁) → (2nd ‘𝑧) = 0)) |
173 | 110, 172 | mpand 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ (2nd ‘𝑧) = 𝑁 → (2nd ‘𝑧) = 0)) |
174 | 1, 2, 3 | poimirlem13 37334 |
. . . . . . . . . 10
⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 0) |
175 | | fveqeq2 6910 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑠 → ((2nd ‘𝑧) = 0 ↔ (2nd
‘𝑠) =
0)) |
176 | 175 | rmo4 3724 |
. . . . . . . . . 10
⊢
(∃*𝑧 ∈
𝑆 (2nd
‘𝑧) = 0 ↔
∀𝑧 ∈ 𝑆 ∀𝑠 ∈ 𝑆 (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑠) = 0) → 𝑧 = 𝑠)) |
177 | 174, 176 | sylib 217 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 ∀𝑠 ∈ 𝑆 (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑠) = 0) → 𝑧 = 𝑠)) |
178 | 177 | r19.21bi 3239 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ∀𝑠 ∈ 𝑆 (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑠) = 0) → 𝑧 = 𝑠)) |
179 | 4 | adantr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑇 ∈ 𝑆) |
180 | | fveqeq2 6910 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑇 → ((2nd ‘𝑠) = 0 ↔ (2nd
‘𝑇) =
0)) |
181 | 180 | anbi2d 628 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑇 → (((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑠) = 0) ↔
((2nd ‘𝑧)
= 0 ∧ (2nd ‘𝑇) = 0))) |
182 | | eqeq2 2738 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑇 → (𝑧 = 𝑠 ↔ 𝑧 = 𝑇)) |
183 | 181, 182 | imbi12d 343 |
. . . . . . . . 9
⊢ (𝑠 = 𝑇 → ((((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑠) = 0) → 𝑧 = 𝑠) ↔ (((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑇) = 0) → 𝑧 = 𝑇))) |
184 | 183 | rspccv 3605 |
. . . . . . . 8
⊢
(∀𝑠 ∈
𝑆 (((2nd
‘𝑧) = 0 ∧
(2nd ‘𝑠) =
0) → 𝑧 = 𝑠) → (𝑇 ∈ 𝑆 → (((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑇) = 0) → 𝑧 = 𝑇))) |
185 | 178, 179,
184 | sylc 65 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑇) = 0) → 𝑧 = 𝑇)) |
186 | 8, 185 | mpan2d 692 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑧) = 0 → 𝑧 = 𝑇)) |
187 | 173, 186 | syld 47 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ (2nd ‘𝑧) = 𝑁 → 𝑧 = 𝑇)) |
188 | 187 | necon1ad 2947 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (2nd ‘𝑧) = 𝑁)) |
189 | 188 | ralrimiva 3136 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ 𝑇 → (2nd ‘𝑧) = 𝑁)) |
190 | 1, 2, 3 | poimirlem14 37335 |
. . 3
⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 𝑁) |
191 | | rmoim 3734 |
. . 3
⊢
(∀𝑧 ∈
𝑆 (𝑧 ≠ 𝑇 → (2nd ‘𝑧) = 𝑁) → (∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 𝑁 → ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)) |
192 | 189, 190,
191 | sylc 65 |
. 2
⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
193 | | reu5 3366 |
. 2
⊢
(∃!𝑧 ∈
𝑆 𝑧 ≠ 𝑇 ↔ (∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 ∧ ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)) |
194 | 7, 192, 193 | sylanbrc 581 |
1
⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |