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 | | poimirlem22.3 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑝 ∈ ran 𝐹(𝑝‘𝑛) ≠ 0) |
6 | | poimirlem21.4 |
. . 3
⊢ (𝜑 → (2nd
‘𝑇) = 𝑁) |
7 | 1, 2, 3, 4, 5, 6 | poimirlem20 32599 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
8 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (2nd ‘𝑇) = 𝑁) |
9 | 1 | nnred 10912 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℝ) |
10 | 9 | ltm1d 10835 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 − 1) < 𝑁) |
11 | | nnm1nn0 11211 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
12 | 1, 11 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
13 | 12 | nn0red 11229 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
14 | 13, 9 | ltnled 10063 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1))) |
15 | 10, 14 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1)) |
16 | | elfzle2 12216 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1)) |
17 | 15, 16 | nsyl 134 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1))) |
18 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢
((2nd ‘𝑧) = 𝑁 → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ 𝑁 ∈ (1...(𝑁 − 1)))) |
19 | 18 | notbid 307 |
. . . . . . . . . . . . 13
⊢
((2nd ‘𝑧) = 𝑁 → (¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)) ↔ ¬ 𝑁 ∈ (1...(𝑁 − 1)))) |
20 | 17, 19 | syl5ibrcom 236 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2nd
‘𝑧) = 𝑁 → ¬ (2nd
‘𝑧) ∈
(1...(𝑁 −
1)))) |
21 | 20 | necon2ad 2797 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2nd
‘𝑧) ∈
(1...(𝑁 − 1)) →
(2nd ‘𝑧)
≠ 𝑁)) |
22 | 21 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑧) ≠ 𝑁)) |
23 | 1 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ) |
24 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (2nd ‘𝑡) = (2nd ‘𝑧)) |
25 | 24 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑧))) |
26 | 25 | ifbid 4058 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑧 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑧), 𝑦, (𝑦 + 1))) |
27 | 26 | csbeq1d 3506 |
. . . . . . . . . . . . . . . . . . . 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})))) |
28 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (1st ‘𝑡) = (1st ‘𝑧)) |
29 | 28 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑧))) |
30 | 28 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑧 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑧))) |
31 | 30 | imaeq1d 5384 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑧)) “
(1...𝑗))) |
32 | 31 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1})) |
33 | 30 | imaeq1d 5384 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑧 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑧)) “ ((𝑗 + 1)...𝑁))) |
34 | 33 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑧 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})) |
35 | 32, 34 | uneq12d 3730 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑧 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
36 | 29, 35 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑧 → ((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑧)) ∘𝑓 +
((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
37 | 36 | csbeq2dv 3944 |
. . . . . . . . . . . . . . . . . . . 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})))) |
38 | 27, 37 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 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})))) |
39 | 38 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . . 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}))))) |
40 | 39 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . 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})))))) |
41 | 40, 2 | elrab2 3333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 ↔ (𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘𝑓 +
((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
42 | 41 | simprbi 479 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘𝑓 +
((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
43 | 42 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑧), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑧)) ∘𝑓 +
((((2nd ‘(1st ‘𝑧)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑧)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
44 | | elrabi 3328 |
. . . . . . . . . . . . . . . . . . . 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...𝑁))) |
45 | 44, 2 | eleq2s 2706 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
46 | | xp1st 7089 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑧) ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑆 → (1st ‘𝑧) ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
48 | | xp1st 7089 |
. . . . . . . . . . . . . . . . . 18
⊢
((1st ‘𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝑆 → (1st
‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
50 | | elmapi 7765 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘(1st ‘𝑧)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾)) |
52 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (0..^𝐾) → 𝑛 ∈ ℤ) |
53 | 52 | ssriv 3572 |
. . . . . . . . . . . . . . . 16
⊢
(0..^𝐾) ⊆
ℤ |
54 | | fss 5969 |
. . . . . . . . . . . . . . . 16
⊢
(((1st ‘(1st ‘𝑧)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶ℤ) |
55 | 51, 53, 54 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶ℤ) |
56 | 55 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (1st
‘(1st ‘𝑧)):(1...𝑁)⟶ℤ) |
57 | | xp2nd 7090 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
58 | 47, 57 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
59 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘(1st ‘𝑧)) ∈ V |
60 | | f1oeq1 6040 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (2nd
‘(1st ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))) |
61 | 59, 60 | elab 3319 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
62 | 58, 61 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
63 | 62 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
64 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd
‘𝑧) ∈
(1...(𝑁 −
1))) |
65 | 23, 43, 56, 63, 64 | poimirlem1 32580 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛)) |
66 | 1 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → 𝑁 ∈ ℕ) |
67 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
68 | 67 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) |
69 | 68 | ifbid 4058 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) |
70 | 69 | csbeq1d 3506 |
. . . . . . . . . . . . . . . . . . . . . . . 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})))) |
71 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑇 → (1st ‘𝑡) = (1st ‘𝑇)) |
72 | 71 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
73 | 71 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) |
74 | 73 | imaeq1d 5384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑗))) |
75 | 74 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1})) |
76 | 73 | imaeq1d 5384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
77 | 76 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
78 | 75, 77 | uneq12d 3730 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑇 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
79 | 72, 78 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
80 | 79 | csbeq2dv 3944 |
. . . . . . . . . . . . . . . . . . . . . . . 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})))) |
81 | 70, 80 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . 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})))) |
82 | 81 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . . . . . . 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}))))) |
83 | 82 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . 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})))))) |
84 | 83, 2 | elrab2 3333 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
85 | 84 | simprbi 479 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
86 | 4, 85 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
87 | 86 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
88 | | elrabi 3328 |
. . . . . . . . . . . . . . . . . . . . . . . 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...𝑁))) |
89 | 88, 2 | eleq2s 2706 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
90 | 4, 89 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
91 | | xp1st 7089 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑇 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (1st
‘𝑇) ∈
(((0..^𝐾)
↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
93 | | xp1st 7089 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
95 | | elmapi 7765 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
97 | | fss 5969 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((1st ‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾) ∧ (0..^𝐾) ⊆ ℤ) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶ℤ) |
98 | 96, 53, 97 | sylancl 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶ℤ) |
99 | 98 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶ℤ) |
100 | | xp2nd 7090 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
101 | 92, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
102 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘(1st ‘𝑇)) ∈ V |
103 | | f1oeq1 6040 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
104 | 102, 103 | elab 3319 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
105 | 101, 104 | sylib 207 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
106 | 105 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
107 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) |
108 | | xp2nd 7090 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd ‘𝑇) ∈ (0...𝑁)) |
109 | 90, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (2nd
‘𝑇) ∈ (0...𝑁)) |
110 | 109 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) →
(2nd ‘𝑇)
∈ (0...𝑁)) |
111 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2nd ‘𝑇) ∈ ((0...𝑁) ∖ {(2nd ‘𝑧)}) ↔ ((2nd
‘𝑇) ∈ (0...𝑁) ∧ (2nd
‘𝑇) ≠
(2nd ‘𝑧))) |
112 | 111 | biimpri 217 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2nd ‘𝑇) ∈ (0...𝑁) ∧ (2nd ‘𝑇) ≠ (2nd
‘𝑧)) →
(2nd ‘𝑇)
∈ ((0...𝑁) ∖
{(2nd ‘𝑧)})) |
113 | 110, 112 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → (2nd ‘𝑇) ∈ ((0...𝑁) ∖ {(2nd ‘𝑧)})) |
114 | 66, 87, 99, 106, 107, 113 | poimirlem2 32581 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ∧
(2nd ‘𝑇)
≠ (2nd ‘𝑧)) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛)) |
115 | 114 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) →
((2nd ‘𝑇)
≠ (2nd ‘𝑧) → ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛))) |
116 | 115 | necon1bd 2800 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) →
(¬ ∃*𝑛 ∈
(1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛) → (2nd ‘𝑇) = (2nd ‘𝑧))) |
117 | 116 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘((2nd ‘𝑧) − 1))‘𝑛) ≠ ((𝐹‘(2nd ‘𝑧))‘𝑛) → (2nd ‘𝑇) = (2nd ‘𝑧))) |
118 | 65, 117 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd
‘𝑇) = (2nd
‘𝑧)) |
119 | 118 | neeq1d 2841 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → ((2nd
‘𝑇) ≠ 𝑁 ↔ (2nd
‘𝑧) ≠ 𝑁)) |
120 | 119 | exbiri 650 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → ((2nd
‘𝑧) ≠ 𝑁 → (2nd
‘𝑇) ≠ 𝑁))) |
121 | 22, 120 | mpdd 42 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑧) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑇) ≠ 𝑁)) |
122 | 121 | necon2bd 2798 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑇) = 𝑁 → ¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)))) |
123 | 8, 122 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) |
124 | | xp2nd 7090 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (2nd ‘𝑧) ∈ (0...𝑁)) |
125 | 45, 124 | syl 17 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑆 → (2nd ‘𝑧) ∈ (0...𝑁)) |
126 | | nn0uz 11598 |
. . . . . . . . . . . . . . . . . 18
⊢
ℕ0 = (ℤ≥‘0) |
127 | 12, 126 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘0)) |
128 | | fzpred 12259 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 − 1) ∈
(ℤ≥‘0) → (0...(𝑁 − 1)) = ({0} ∪ ((0 + 1)...(𝑁 − 1)))) |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0...(𝑁 − 1)) = ({0} ∪ ((0 + 1)...(𝑁 − 1)))) |
130 | | 0p1e1 11009 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 + 1) =
1 |
131 | 130 | oveq1i 6559 |
. . . . . . . . . . . . . . . . 17
⊢ ((0 +
1)...(𝑁 − 1)) =
(1...(𝑁 −
1)) |
132 | 131 | uneq2i 3726 |
. . . . . . . . . . . . . . . 16
⊢ ({0}
∪ ((0 + 1)...(𝑁 −
1))) = ({0} ∪ (1...(𝑁
− 1))) |
133 | 129, 132 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0...(𝑁 − 1)) = ({0} ∪ (1...(𝑁 − 1)))) |
134 | 133 | eleq2d 2673 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘𝑧) ∈
(0...(𝑁 − 1)) ↔
(2nd ‘𝑧)
∈ ({0} ∪ (1...(𝑁
− 1))))) |
135 | 134 | notbid 307 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (¬ (2nd
‘𝑧) ∈
(0...(𝑁 − 1)) ↔
¬ (2nd ‘𝑧) ∈ ({0} ∪ (1...(𝑁 − 1))))) |
136 | | ioran 510 |
. . . . . . . . . . . . . 14
⊢ (¬
((2nd ‘𝑧)
= 0 ∨ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) ↔ (¬ (2nd
‘𝑧) = 0 ∧ ¬
(2nd ‘𝑧)
∈ (1...(𝑁 −
1)))) |
137 | | elun 3715 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘𝑧) ∈ ({0} ∪ (1...(𝑁 − 1))) ↔ ((2nd
‘𝑧) ∈ {0} ∨
(2nd ‘𝑧)
∈ (1...(𝑁 −
1)))) |
138 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘𝑧) ∈ V |
139 | 138 | elsn 4140 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘𝑧) ∈ {0} ↔ (2nd
‘𝑧) =
0) |
140 | 139 | orbi1i 541 |
. . . . . . . . . . . . . . 15
⊢
(((2nd ‘𝑧) ∈ {0} ∨ (2nd
‘𝑧) ∈
(1...(𝑁 − 1))) ↔
((2nd ‘𝑧)
= 0 ∨ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)))) |
141 | 137, 140 | bitri 263 |
. . . . . . . . . . . . . 14
⊢
((2nd ‘𝑧) ∈ ({0} ∪ (1...(𝑁 − 1))) ↔ ((2nd
‘𝑧) = 0 ∨
(2nd ‘𝑧)
∈ (1...(𝑁 −
1)))) |
142 | 136, 141 | xchnxbir 322 |
. . . . . . . . . . . . 13
⊢ (¬
(2nd ‘𝑧)
∈ ({0} ∪ (1...(𝑁
− 1))) ↔ (¬ (2nd ‘𝑧) = 0 ∧ ¬ (2nd
‘𝑧) ∈
(1...(𝑁 −
1)))) |
143 | 135, 142 | syl6bb 275 |
. . . . . . . . . . . 12
⊢ (𝜑 → (¬ (2nd
‘𝑧) ∈
(0...(𝑁 − 1)) ↔
(¬ (2nd ‘𝑧) = 0 ∧ ¬ (2nd
‘𝑧) ∈
(1...(𝑁 −
1))))) |
144 | 143 | anbi2d 736 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2nd
‘𝑧) ∈ (0...𝑁) ∧ ¬ (2nd
‘𝑧) ∈
(0...(𝑁 − 1))) ↔
((2nd ‘𝑧)
∈ (0...𝑁) ∧ (¬
(2nd ‘𝑧) =
0 ∧ ¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1)))))) |
145 | | uncom 3719 |
. . . . . . . . . . . . . . . 16
⊢
((0...(𝑁 − 1))
∪ {𝑁}) = ({𝑁} ∪ (0...(𝑁 − 1))) |
146 | 145 | difeq1i 3686 |
. . . . . . . . . . . . . . 15
⊢
(((0...(𝑁 −
1)) ∪ {𝑁}) ∖
(0...(𝑁 − 1))) =
(({𝑁} ∪ (0...(𝑁 − 1))) ∖
(0...(𝑁 −
1))) |
147 | | difun2 4000 |
. . . . . . . . . . . . . . 15
⊢ (({𝑁} ∪ (0...(𝑁 − 1))) ∖ (0...(𝑁 − 1))) = ({𝑁} ∖ (0...(𝑁 − 1))) |
148 | 146, 147 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢
(((0...(𝑁 −
1)) ∪ {𝑁}) ∖
(0...(𝑁 − 1))) =
({𝑁} ∖ (0...(𝑁 − 1))) |
149 | 1 | nncnd 10913 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℂ) |
150 | | npcan1 10334 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
151 | 149, 150 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
152 | 1 | nnnn0d 11228 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
153 | 152, 126 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
154 | 151, 153 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘0)) |
155 | 12 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
156 | | uzid 11578 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
157 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
158 | 155, 156,
157 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
159 | 151, 158 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
160 | | fzsplit2 12237 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 − 1) + 1) ∈
(ℤ≥‘0) ∧ 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) → (0...𝑁) = ((0...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
161 | 154, 159,
160 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0...𝑁) = ((0...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁))) |
162 | 151 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = (𝑁...𝑁)) |
163 | 1 | nnzd 11357 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℤ) |
164 | | fzsn 12254 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁}) |
165 | 163, 164 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑁...𝑁) = {𝑁}) |
166 | 162, 165 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑁 − 1) + 1)...𝑁) = {𝑁}) |
167 | 166 | uneq2d 3729 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((0...(𝑁 − 1)) ∪ (((𝑁 − 1) + 1)...𝑁)) = ((0...(𝑁 − 1)) ∪ {𝑁})) |
168 | 161, 167 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0...𝑁) = ((0...(𝑁 − 1)) ∪ {𝑁})) |
169 | 168 | difeq1d 3689 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((0...𝑁) ∖ (0...(𝑁 − 1))) = (((0...(𝑁 − 1)) ∪ {𝑁}) ∖ (0...(𝑁 − 1)))) |
170 | | elfzle2 12216 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ (0...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1)) |
171 | 15, 170 | nsyl 134 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ 𝑁 ∈ (0...(𝑁 − 1))) |
172 | | incom 3767 |
. . . . . . . . . . . . . . . . 17
⊢
((0...(𝑁 − 1))
∩ {𝑁}) = ({𝑁} ∩ (0...(𝑁 − 1))) |
173 | 172 | eqeq1i 2615 |
. . . . . . . . . . . . . . . 16
⊢
(((0...(𝑁 −
1)) ∩ {𝑁}) = ∅
↔ ({𝑁} ∩
(0...(𝑁 − 1))) =
∅) |
174 | | disjsn 4192 |
. . . . . . . . . . . . . . . 16
⊢
(((0...(𝑁 −
1)) ∩ {𝑁}) = ∅
↔ ¬ 𝑁 ∈
(0...(𝑁 −
1))) |
175 | | disj3 3973 |
. . . . . . . . . . . . . . . 16
⊢ (({𝑁} ∩ (0...(𝑁 − 1))) = ∅ ↔ {𝑁} = ({𝑁} ∖ (0...(𝑁 − 1)))) |
176 | 173, 174,
175 | 3bitr3i 289 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑁 ∈ (0...(𝑁 − 1)) ↔ {𝑁} = ({𝑁} ∖ (0...(𝑁 − 1)))) |
177 | 171, 176 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑁} = ({𝑁} ∖ (0...(𝑁 − 1)))) |
178 | 148, 169,
177 | 3eqtr4a 2670 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((0...𝑁) ∖ (0...(𝑁 − 1))) = {𝑁}) |
179 | 178 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2nd
‘𝑧) ∈
((0...𝑁) ∖
(0...(𝑁 − 1))) ↔
(2nd ‘𝑧)
∈ {𝑁})) |
180 | | eldif 3550 |
. . . . . . . . . . . 12
⊢
((2nd ‘𝑧) ∈ ((0...𝑁) ∖ (0...(𝑁 − 1))) ↔ ((2nd
‘𝑧) ∈ (0...𝑁) ∧ ¬ (2nd
‘𝑧) ∈
(0...(𝑁 −
1)))) |
181 | 138 | elsn 4140 |
. . . . . . . . . . . 12
⊢
((2nd ‘𝑧) ∈ {𝑁} ↔ (2nd ‘𝑧) = 𝑁) |
182 | 179, 180,
181 | 3bitr3g 301 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2nd
‘𝑧) ∈ (0...𝑁) ∧ ¬ (2nd
‘𝑧) ∈
(0...(𝑁 − 1))) ↔
(2nd ‘𝑧) =
𝑁)) |
183 | 144, 182 | bitr3d 269 |
. . . . . . . . . 10
⊢ (𝜑 → (((2nd
‘𝑧) ∈ (0...𝑁) ∧ (¬ (2nd
‘𝑧) = 0 ∧ ¬
(2nd ‘𝑧)
∈ (1...(𝑁 −
1)))) ↔ (2nd ‘𝑧) = 𝑁)) |
184 | 183 | biimpd 218 |
. . . . . . . . 9
⊢ (𝜑 → (((2nd
‘𝑧) ∈ (0...𝑁) ∧ (¬ (2nd
‘𝑧) = 0 ∧ ¬
(2nd ‘𝑧)
∈ (1...(𝑁 −
1)))) → (2nd ‘𝑧) = 𝑁)) |
185 | 184 | expdimp 452 |
. . . . . . . 8
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈ (0...𝑁)) → ((¬
(2nd ‘𝑧) =
0 ∧ ¬ (2nd ‘𝑧) ∈ (1...(𝑁 − 1))) → (2nd
‘𝑧) = 𝑁)) |
186 | 125, 185 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((¬ (2nd
‘𝑧) = 0 ∧ ¬
(2nd ‘𝑧)
∈ (1...(𝑁 − 1)))
→ (2nd ‘𝑧) = 𝑁)) |
187 | 123, 186 | mpan2d 706 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ (2nd ‘𝑧) = 0 → (2nd
‘𝑧) = 𝑁)) |
188 | 1, 2, 3 | poimirlem14 32593 |
. . . . . . . . . 10
⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 𝑁) |
189 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑠 → (2nd ‘𝑧) = (2nd ‘𝑠)) |
190 | 189 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑠 → ((2nd ‘𝑧) = 𝑁 ↔ (2nd ‘𝑠) = 𝑁)) |
191 | 190 | rmo4 3366 |
. . . . . . . . . 10
⊢
(∃*𝑧 ∈
𝑆 (2nd
‘𝑧) = 𝑁 ↔ ∀𝑧 ∈ 𝑆 ∀𝑠 ∈ 𝑆 (((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑠) = 𝑁) → 𝑧 = 𝑠)) |
192 | 188, 191 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 ∀𝑠 ∈ 𝑆 (((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑠) = 𝑁) → 𝑧 = 𝑠)) |
193 | 192 | r19.21bi 2916 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ∀𝑠 ∈ 𝑆 (((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑠) = 𝑁) → 𝑧 = 𝑠)) |
194 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑇 ∈ 𝑆) |
195 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑇 → (2nd ‘𝑠) = (2nd ‘𝑇)) |
196 | 195 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑇 → ((2nd ‘𝑠) = 𝑁 ↔ (2nd ‘𝑇) = 𝑁)) |
197 | 196 | anbi2d 736 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑇 → (((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑠) = 𝑁) ↔ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑇) = 𝑁))) |
198 | | eqeq2 2621 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑇 → (𝑧 = 𝑠 ↔ 𝑧 = 𝑇)) |
199 | 197, 198 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑠 = 𝑇 → ((((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑠) = 𝑁) → 𝑧 = 𝑠) ↔ (((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑇) = 𝑁) → 𝑧 = 𝑇))) |
200 | 199 | rspccv 3279 |
. . . . . . . 8
⊢
(∀𝑠 ∈
𝑆 (((2nd
‘𝑧) = 𝑁 ∧ (2nd
‘𝑠) = 𝑁) → 𝑧 = 𝑠) → (𝑇 ∈ 𝑆 → (((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑇) = 𝑁) → 𝑧 = 𝑇))) |
201 | 193, 194,
200 | sylc 63 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑇) = 𝑁) → 𝑧 = 𝑇)) |
202 | 8, 201 | mpan2d 706 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((2nd ‘𝑧) = 𝑁 → 𝑧 = 𝑇)) |
203 | 187, 202 | syld 46 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ (2nd ‘𝑧) = 0 → 𝑧 = 𝑇)) |
204 | 203 | necon1ad 2799 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝑧 ≠ 𝑇 → (2nd ‘𝑧) = 0)) |
205 | 204 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ 𝑇 → (2nd ‘𝑧) = 0)) |
206 | 1, 2, 3 | poimirlem13 32592 |
. . 3
⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 0) |
207 | | rmoim 3374 |
. . 3
⊢
(∀𝑧 ∈
𝑆 (𝑧 ≠ 𝑇 → (2nd ‘𝑧) = 0) → (∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 0 → ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)) |
208 | 205, 206,
207 | sylc 63 |
. 2
⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |
209 | | reu5 3136 |
. 2
⊢
(∃!𝑧 ∈
𝑆 𝑧 ≠ 𝑇 ↔ (∃𝑧 ∈ 𝑆 𝑧 ≠ 𝑇 ∧ ∃*𝑧 ∈ 𝑆 𝑧 ≠ 𝑇)) |
210 | 7, 208, 209 | sylanbrc 695 |
1
⊢ (𝜑 → ∃!𝑧 ∈ 𝑆 𝑧 ≠ 𝑇) |