Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
𝑁 ∈
ℕ) |
3 | | poimirlem22.s |
. . . . . . . 8
⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
4 | | poimirlem22.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) |
5 | 4 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) |
6 | | simplrl 777 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
𝑧 ∈ 𝑆) |
7 | | simprl 771 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
(2nd ‘𝑧) =
0) |
8 | 2, 3, 5, 6, 7 | poimirlem10 35551 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
((𝐹‘(𝑁 − 1)) ∘f
− ((1...𝑁) ×
{1})) = (1st ‘(1st ‘𝑧))) |
9 | | simplrr 778 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
𝑘 ∈ 𝑆) |
10 | | simprr 773 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
(2nd ‘𝑘) =
0) |
11 | 2, 3, 5, 9, 10 | poimirlem10 35551 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
((𝐹‘(𝑁 − 1)) ∘f
− ((1...𝑁) ×
{1})) = (1st ‘(1st ‘𝑘))) |
12 | 8, 11 | eqtr3d 2780 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
(1st ‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑘))) |
13 | | elrabi 3609 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ {𝑡 ∈ ((((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...𝑁))) |
14 | 13, 3 | eleq2s 2857 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
15 | | xp1st 7812 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑆 → (1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
17 | | xp2nd 7813 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
19 | | fvex 6749 |
. . . . . . . . . . . 12
⊢
(2nd ‘(1st ‘𝑧)) ∈ V |
20 | | f1oeq1 6668 |
. . . . . . . . . . . 12
⊢ (𝑓 = (2nd
‘(1st ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))) |
21 | 19, 20 | elab 3600 |
. . . . . . . . . . 11
⊢
((2nd ‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
22 | 18, 21 | sylib 221 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
23 | | f1ofn 6681 |
. . . . . . . . . 10
⊢
((2nd ‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑧)) Fn (1...𝑁)) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)) Fn (1...𝑁)) |
25 | 24 | adantr 484 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) → (2nd
‘(1st ‘𝑧)) Fn (1...𝑁)) |
26 | 25 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
(2nd ‘(1st ‘𝑧)) Fn (1...𝑁)) |
27 | | elrabi 3609 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ {𝑡 ∈ ((((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...𝑁))) |
28 | 27, 3 | eleq2s 2857 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝑆 → 𝑘 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
29 | | xp1st 7812 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑘) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑆 → (1st ‘𝑘) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
31 | | xp2nd 7813 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑘) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑘)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑆 → (2nd
‘(1st ‘𝑘)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
33 | | fvex 6749 |
. . . . . . . . . . . 12
⊢
(2nd ‘(1st ‘𝑘)) ∈ V |
34 | | f1oeq1 6668 |
. . . . . . . . . . . 12
⊢ (𝑓 = (2nd
‘(1st ‘𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))) |
35 | 33, 34 | elab 3600 |
. . . . . . . . . . 11
⊢
((2nd ‘(1st ‘𝑘)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)) |
36 | 32, 35 | sylib 221 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝑆 → (2nd
‘(1st ‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)) |
37 | | f1ofn 6681 |
. . . . . . . . . 10
⊢
((2nd ‘(1st ‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑘)) Fn (1...𝑁)) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝑆 → (2nd
‘(1st ‘𝑘)) Fn (1...𝑁)) |
39 | 38 | adantl 485 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) → (2nd
‘(1st ‘𝑘)) Fn (1...𝑁)) |
40 | 39 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
(2nd ‘(1st ‘𝑘)) Fn (1...𝑁)) |
41 | | eleq1 2826 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑁) ↔ 𝑛 ∈ (1...𝑁))) |
42 | 41 | anbi2d 632 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑚 ∈ (1...𝑁)) ↔ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑛 ∈ (1...𝑁)))) |
43 | | oveq2 7240 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛)) |
44 | 43 | imaeq2d 5944 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → ((2nd
‘(1st ‘𝑧)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑧)) “
(1...𝑛))) |
45 | 43 | imaeq2d 5944 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → ((2nd
‘(1st ‘𝑘)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑛))) |
46 | 44, 45 | eqeq12d 2754 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (((2nd
‘(1st ‘𝑧)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑚)) ↔
((2nd ‘(1st ‘𝑧)) “ (1...𝑛)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑛)))) |
47 | 42, 46 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑚 ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑚))) ↔ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑛))))) |
48 | 1 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑁 ∈ ℕ) |
49 | 4 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑚 ∈ (1...𝑁)) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) |
50 | | simpl 486 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) → 𝑧 ∈ 𝑆) |
51 | 50 | ad3antlr 731 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑧 ∈ 𝑆) |
52 | | simplrl 777 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑚 ∈ (1...𝑁)) → (2nd ‘𝑧) = 0) |
53 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ 𝑆) |
54 | 53 | ad3antlr 731 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑘 ∈ 𝑆) |
55 | | simplrr 778 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑚 ∈ (1...𝑁)) → (2nd ‘𝑘) = 0) |
56 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑚 ∈ (1...𝑁)) → 𝑚 ∈ (1...𝑁)) |
57 | 48, 3, 49, 51, 52, 54, 55, 56 | poimirlem11 35552 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑚 ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑚)) ⊆ ((2nd
‘(1st ‘𝑘)) “ (1...𝑚))) |
58 | 48, 3, 49, 54, 55, 51, 52, 56 | poimirlem11 35552 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑚 ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑘)) “ (1...𝑚)) ⊆ ((2nd
‘(1st ‘𝑧)) “ (1...𝑚))) |
59 | 57, 58 | eqssd 3933 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑚 ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑚))) |
60 | 47, 59 | chvarvv 2007 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑛))) |
61 | | simpll 767 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
𝜑) |
62 | | elfznn 13166 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ) |
63 | | nnm1nn0 12156 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...𝑁) → (𝑛 − 1) ∈
ℕ0) |
65 | 64 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = 1) → (𝑛 − 1) ∈
ℕ0) |
66 | 62 | nncnd 11871 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ) |
67 | | ax-1cn 10812 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℂ |
68 | | subeq0 11129 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 −
1) = 0 ↔ 𝑛 =
1)) |
69 | 66, 67, 68 | sylancl 589 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = 0 ↔ 𝑛 = 1)) |
70 | 69 | necon3abid 2978 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) ≠ 0 ↔ ¬ 𝑛 = 1)) |
71 | 70 | biimpar 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = 1) → (𝑛 − 1) ≠ 0) |
72 | | elnnne0 12129 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 − 1) ∈ ℕ
↔ ((𝑛 − 1)
∈ ℕ0 ∧ (𝑛 − 1) ≠ 0)) |
73 | 65, 71, 72 | sylanbrc 586 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = 1) → (𝑛 − 1) ∈ ℕ) |
74 | 73 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = 1)) → (𝑛 − 1) ∈ ℕ) |
75 | 64 | nn0red 12176 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...𝑁) → (𝑛 − 1) ∈ ℝ) |
76 | 75 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ ℝ) |
77 | 62 | nnred 11870 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℝ) |
78 | 77 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℝ) |
79 | 1 | nnred 11870 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℝ) |
80 | 79 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑁 ∈ ℝ) |
81 | 77 | lem1d 11790 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...𝑁) → (𝑛 − 1) ≤ 𝑛) |
82 | 81 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ≤ 𝑛) |
83 | | elfzle2 13141 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ≤ 𝑁) |
84 | 83 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ≤ 𝑁) |
85 | 76, 78, 80, 82, 84 | letrd 11014 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ≤ 𝑁) |
86 | 85 | adantrr 717 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = 1)) → (𝑛 − 1) ≤ 𝑁) |
87 | 1 | nnzd 12306 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ ℤ) |
88 | | fznn 13205 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℤ → ((𝑛 − 1) ∈ (1...𝑁) ↔ ((𝑛 − 1) ∈ ℕ ∧ (𝑛 − 1) ≤ 𝑁))) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑛 − 1) ∈ (1...𝑁) ↔ ((𝑛 − 1) ∈ ℕ ∧ (𝑛 − 1) ≤ 𝑁))) |
90 | 89 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = 1)) → ((𝑛 − 1) ∈ (1...𝑁) ↔ ((𝑛 − 1) ∈ ℕ ∧ (𝑛 − 1) ≤ 𝑁))) |
91 | 74, 86, 90 | mpbir2and 713 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = 1)) → (𝑛 − 1) ∈ (1...𝑁)) |
92 | 61, 91 | sylan 583 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧
(𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = 1)) → (𝑛 − 1) ∈ (1...𝑁)) |
93 | | ovex 7265 |
. . . . . . . . . . . . . 14
⊢ (𝑛 − 1) ∈
V |
94 | | eleq1 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = (𝑛 − 1) → (𝑚 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (1...𝑁))) |
95 | 94 | anbi2d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (𝑛 − 1) → ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑚 ∈ (1...𝑁)) ↔ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧
(𝑛 − 1) ∈
(1...𝑁)))) |
96 | | oveq2 7240 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (𝑛 − 1) → (1...𝑚) = (1...(𝑛 − 1))) |
97 | 96 | imaeq2d 5944 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = (𝑛 − 1) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑧)) “
(1...(𝑛 −
1)))) |
98 | 96 | imaeq2d 5944 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = (𝑛 − 1) → ((2nd
‘(1st ‘𝑘)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑘)) “
(1...(𝑛 −
1)))) |
99 | 97, 98 | eqeq12d 2754 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (𝑛 − 1) → (((2nd
‘(1st ‘𝑧)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑚)) ↔
((2nd ‘(1st ‘𝑧)) “ (1...(𝑛 − 1))) = ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1))))) |
100 | 95, 99 | imbi12d 348 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 − 1) → (((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑚 ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑚))) ↔ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧
(𝑛 − 1) ∈
(1...𝑁)) →
((2nd ‘(1st ‘𝑧)) “ (1...(𝑛 − 1))) = ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1)))))) |
101 | 93, 100, 59 | vtocl 3487 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧
(𝑛 − 1) ∈
(1...𝑁)) →
((2nd ‘(1st ‘𝑧)) “ (1...(𝑛 − 1))) = ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1)))) |
102 | 92, 101 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧
(𝑛 ∈ (1...𝑁) ∧ ¬ 𝑛 = 1)) → ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1))) = ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1)))) |
103 | 102 | expr 460 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (¬ 𝑛 = 1 → ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1))) = ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1))))) |
104 | | ima0 5960 |
. . . . . . . . . . . . 13
⊢
((2nd ‘(1st ‘𝑧)) “ ∅) =
∅ |
105 | | ima0 5960 |
. . . . . . . . . . . . 13
⊢
((2nd ‘(1st ‘𝑘)) “ ∅) =
∅ |
106 | 104, 105 | eqtr4i 2769 |
. . . . . . . . . . . 12
⊢
((2nd ‘(1st ‘𝑧)) “ ∅) = ((2nd
‘(1st ‘𝑘)) “ ∅) |
107 | | oveq1 7239 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 1 → (𝑛 − 1) = (1 − 1)) |
108 | | 1m1e0 11927 |
. . . . . . . . . . . . . . . 16
⊢ (1
− 1) = 0 |
109 | 107, 108 | eqtrdi 2795 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 1 → (𝑛 − 1) = 0) |
110 | 109 | oveq2d 7248 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → (1...(𝑛 − 1)) =
(1...0)) |
111 | | fz10 13158 |
. . . . . . . . . . . . . 14
⊢ (1...0) =
∅ |
112 | 110, 111 | eqtrdi 2795 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 1 → (1...(𝑛 − 1)) =
∅) |
113 | 112 | imaeq2d 5944 |
. . . . . . . . . . . 12
⊢ (𝑛 = 1 → ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1))) = ((2nd
‘(1st ‘𝑧)) “ ∅)) |
114 | 112 | imaeq2d 5944 |
. . . . . . . . . . . 12
⊢ (𝑛 = 1 → ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1))) = ((2nd
‘(1st ‘𝑘)) “ ∅)) |
115 | 106, 113,
114 | 3eqtr4a 2805 |
. . . . . . . . . . 11
⊢ (𝑛 = 1 → ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1))) = ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1)))) |
116 | 103, 115 | pm2.61d2 184 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1))) = ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1)))) |
117 | 60, 116 | difeq12d 4053 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) ∖ ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1)))) = (((2nd
‘(1st ‘𝑘)) “ (1...𝑛)) ∖ ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1))))) |
118 | | fnsnfv 6809 |
. . . . . . . . . . . 12
⊢
(((2nd ‘(1st ‘𝑧)) Fn (1...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑧))‘𝑛)} = ((2nd ‘(1st
‘𝑧)) “ {𝑛})) |
119 | 24, 118 | sylan 583 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑧))‘𝑛)} = ((2nd ‘(1st
‘𝑧)) “ {𝑛})) |
120 | 62 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ) |
121 | | uncom 4082 |
. . . . . . . . . . . . . . . 16
⊢
((1...(𝑛 − 1))
∪ {𝑛}) = ({𝑛} ∪ (1...(𝑛 − 1))) |
122 | 121 | difeq1i 4048 |
. . . . . . . . . . . . . . 15
⊢
(((1...(𝑛 −
1)) ∪ {𝑛}) ∖
(1...(𝑛 − 1))) =
(({𝑛} ∪ (1...(𝑛 − 1))) ∖
(1...(𝑛 −
1))) |
123 | | difun2 4410 |
. . . . . . . . . . . . . . 15
⊢ (({𝑛} ∪ (1...(𝑛 − 1))) ∖ (1...(𝑛 − 1))) = ({𝑛} ∖ (1...(𝑛 − 1))) |
124 | 122, 123 | eqtri 2766 |
. . . . . . . . . . . . . 14
⊢
(((1...(𝑛 −
1)) ∪ {𝑛}) ∖
(1...(𝑛 − 1))) =
({𝑛} ∖ (1...(𝑛 − 1))) |
125 | | nncn 11863 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
126 | | npcan1 11282 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛) |
127 | 125, 126 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) = 𝑛) |
128 | | elnnuz 12503 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘1)) |
129 | 128 | biimpi 219 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
(ℤ≥‘1)) |
130 | 127, 129 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) ∈
(ℤ≥‘1)) |
131 | 63 | nn0zd 12305 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℤ) |
132 | | uzid 12478 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 − 1) ∈ ℤ
→ (𝑛 − 1) ∈
(ℤ≥‘(𝑛 − 1))) |
133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
(ℤ≥‘(𝑛 − 1))) |
134 | | peano2uz 12522 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 − 1) ∈
(ℤ≥‘(𝑛 − 1)) → ((𝑛 − 1) + 1) ∈
(ℤ≥‘(𝑛 − 1))) |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) ∈
(ℤ≥‘(𝑛 − 1))) |
136 | 127, 135 | eqeltrrd 2840 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
(ℤ≥‘(𝑛 − 1))) |
137 | | fzsplit2 13162 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘(𝑛 − 1))) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛))) |
138 | 130, 136,
137 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ →
(1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛))) |
139 | 127 | oveq1d 7247 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → (((𝑛 − 1) + 1)...𝑛) = (𝑛...𝑛)) |
140 | | nnz 12224 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
141 | | fzsn 13179 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℤ → (𝑛...𝑛) = {𝑛}) |
142 | 140, 141 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → (𝑛...𝑛) = {𝑛}) |
143 | 139, 142 | eqtrd 2778 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (((𝑛 − 1) + 1)...𝑛) = {𝑛}) |
144 | 143 | uneq2d 4092 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ →
((1...(𝑛 − 1)) ∪
(((𝑛 − 1) +
1)...𝑛)) = ((1...(𝑛 − 1)) ∪ {𝑛})) |
145 | 138, 144 | eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
(1...𝑛) = ((1...(𝑛 − 1)) ∪ {𝑛})) |
146 | 145 | difeq1d 4051 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
((1...𝑛) ∖
(1...(𝑛 − 1))) =
(((1...(𝑛 − 1)) ∪
{𝑛}) ∖ (1...(𝑛 − 1)))) |
147 | | nnre 11862 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
148 | | ltm1 11699 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) < 𝑛) |
149 | | peano2rem 11170 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈
ℝ) |
150 | | ltnle 10937 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 − 1) ∈ ℝ ∧
𝑛 ∈ ℝ) →
((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1))) |
151 | 149, 150 | mpancom 688 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℝ → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1))) |
152 | 148, 151 | mpbid 235 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ → ¬
𝑛 ≤ (𝑛 − 1)) |
153 | | elfzle2 13141 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...(𝑛 − 1)) → 𝑛 ≤ (𝑛 − 1)) |
154 | 152, 153 | nsyl 142 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℝ → ¬
𝑛 ∈ (1...(𝑛 − 1))) |
155 | 147, 154 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ¬
𝑛 ∈ (1...(𝑛 − 1))) |
156 | | incom 4130 |
. . . . . . . . . . . . . . . . 17
⊢
((1...(𝑛 − 1))
∩ {𝑛}) = ({𝑛} ∩ (1...(𝑛 − 1))) |
157 | 156 | eqeq1i 2743 |
. . . . . . . . . . . . . . . 16
⊢
(((1...(𝑛 −
1)) ∩ {𝑛}) = ∅
↔ ({𝑛} ∩
(1...(𝑛 − 1))) =
∅) |
158 | | disjsn 4642 |
. . . . . . . . . . . . . . . 16
⊢
(((1...(𝑛 −
1)) ∩ {𝑛}) = ∅
↔ ¬ 𝑛 ∈
(1...(𝑛 −
1))) |
159 | | disj3 4383 |
. . . . . . . . . . . . . . . 16
⊢ (({𝑛} ∩ (1...(𝑛 − 1))) = ∅ ↔ {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1)))) |
160 | 157, 158,
159 | 3bitr3i 304 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑛 ∈ (1...(𝑛 − 1)) ↔ {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1)))) |
161 | 155, 160 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1)))) |
162 | 124, 146,
161 | 3eqtr4a 2805 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
((1...𝑛) ∖
(1...(𝑛 − 1))) =
{𝑛}) |
163 | 120, 162 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((1...𝑛) ∖ (1...(𝑛 − 1))) = {𝑛}) |
164 | 163 | imaeq2d 5944 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = ((2nd
‘(1st ‘𝑧)) “ {𝑛})) |
165 | | dff1o3 6686 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd
‘(1st ‘𝑧)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡(2nd ‘(1st
‘𝑧)))) |
166 | 165 | simprbi 500 |
. . . . . . . . . . . . . 14
⊢
((2nd ‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡(2nd ‘(1st
‘𝑧))) |
167 | 22, 166 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑆 → Fun ◡(2nd ‘(1st
‘𝑧))) |
168 | | imadif 6482 |
. . . . . . . . . . . . 13
⊢ (Fun
◡(2nd ‘(1st
‘𝑧)) →
((2nd ‘(1st ‘𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = (((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) ∖ ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1))))) |
169 | 167, 168 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑆 → ((2nd
‘(1st ‘𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = (((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) ∖ ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1))))) |
170 | 169 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = (((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) ∖ ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1))))) |
171 | 119, 164,
170 | 3eqtr2d 2784 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑧))‘𝑛)} = (((2nd ‘(1st
‘𝑧)) “
(1...𝑛)) ∖
((2nd ‘(1st ‘𝑧)) “ (1...(𝑛 − 1))))) |
172 | 6, 171 | sylan 583 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑧))‘𝑛)} = (((2nd ‘(1st
‘𝑧)) “
(1...𝑛)) ∖
((2nd ‘(1st ‘𝑧)) “ (1...(𝑛 − 1))))) |
173 | | eleq1 2826 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑘 → (𝑧 ∈ 𝑆 ↔ 𝑘 ∈ 𝑆)) |
174 | 173 | anbi1d 633 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑘 → ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) ↔ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)))) |
175 | | 2fveq3 6741 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑘 → (2nd
‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑘))) |
176 | 175 | fveq1d 6738 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑘 → ((2nd
‘(1st ‘𝑧))‘𝑛) = ((2nd ‘(1st
‘𝑘))‘𝑛)) |
177 | 176 | sneqd 4568 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑘 → {((2nd
‘(1st ‘𝑧))‘𝑛)} = {((2nd ‘(1st
‘𝑘))‘𝑛)}) |
178 | 175 | imaeq1d 5943 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑘 → ((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑛))) |
179 | 175 | imaeq1d 5943 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑘 → ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1))) = ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1)))) |
180 | 178, 179 | difeq12d 4053 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑘 → (((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) ∖ ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1)))) = (((2nd
‘(1st ‘𝑘)) “ (1...𝑛)) ∖ ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1))))) |
181 | 177, 180 | eqeq12d 2754 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑘 → ({((2nd
‘(1st ‘𝑧))‘𝑛)} = (((2nd ‘(1st
‘𝑧)) “
(1...𝑛)) ∖
((2nd ‘(1st ‘𝑧)) “ (1...(𝑛 − 1)))) ↔ {((2nd
‘(1st ‘𝑘))‘𝑛)} = (((2nd ‘(1st
‘𝑘)) “
(1...𝑛)) ∖
((2nd ‘(1st ‘𝑘)) “ (1...(𝑛 − 1)))))) |
182 | 174, 181 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑘 → (((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑧))‘𝑛)} = (((2nd ‘(1st
‘𝑧)) “
(1...𝑛)) ∖
((2nd ‘(1st ‘𝑧)) “ (1...(𝑛 − 1))))) ↔ ((𝑘 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑘))‘𝑛)} = (((2nd ‘(1st
‘𝑘)) “
(1...𝑛)) ∖
((2nd ‘(1st ‘𝑘)) “ (1...(𝑛 − 1))))))) |
183 | 182, 171 | chvarvv 2007 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑘))‘𝑛)} = (((2nd ‘(1st
‘𝑘)) “
(1...𝑛)) ∖
((2nd ‘(1st ‘𝑘)) “ (1...(𝑛 − 1))))) |
184 | 9, 183 | sylan 583 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑘))‘𝑛)} = (((2nd ‘(1st
‘𝑘)) “
(1...𝑛)) ∖
((2nd ‘(1st ‘𝑘)) “ (1...(𝑛 − 1))))) |
185 | 117, 172,
184 | 3eqtr4d 2788 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑧))‘𝑛)} = {((2nd ‘(1st
‘𝑘))‘𝑛)}) |
186 | | fvex 6749 |
. . . . . . . . 9
⊢
((2nd ‘(1st ‘𝑧))‘𝑛) ∈ V |
187 | 186 | sneqr 4766 |
. . . . . . . 8
⊢
({((2nd ‘(1st ‘𝑧))‘𝑛)} = {((2nd ‘(1st
‘𝑘))‘𝑛)} → ((2nd
‘(1st ‘𝑧))‘𝑛) = ((2nd ‘(1st
‘𝑘))‘𝑛)) |
188 | 185, 187 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑧))‘𝑛) = ((2nd ‘(1st
‘𝑘))‘𝑛)) |
189 | 26, 40, 188 | eqfnfvd 6874 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
(2nd ‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑘))) |
190 | | xpopth 7821 |
. . . . . . . 8
⊢
(((1st ‘𝑧) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (1st ‘𝑘) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) → (((1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑘)) ∧
(2nd ‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑘))) ↔
(1st ‘𝑧) =
(1st ‘𝑘))) |
191 | 16, 30, 190 | syl2an 599 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) → (((1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑘)) ∧
(2nd ‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑘))) ↔
(1st ‘𝑧) =
(1st ‘𝑘))) |
192 | 191 | ad2antlr 727 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
(((1st ‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑘)) ∧
(2nd ‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑘))) ↔
(1st ‘𝑧) =
(1st ‘𝑘))) |
193 | 12, 189, 192 | mpbi2and 712 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
(1st ‘𝑧) =
(1st ‘𝑘)) |
194 | | eqtr3 2764 |
. . . . . 6
⊢
(((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑘) = 0) → (2nd
‘𝑧) = (2nd
‘𝑘)) |
195 | 194 | adantl 485 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
(2nd ‘𝑧) =
(2nd ‘𝑘)) |
196 | | xpopth 7821 |
. . . . . . 7
⊢ ((𝑧 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑘 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1st ‘𝑧) = (1st ‘𝑘) ∧ (2nd
‘𝑧) = (2nd
‘𝑘)) ↔ 𝑧 = 𝑘)) |
197 | 14, 28, 196 | syl2an 599 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) → (((1st ‘𝑧) = (1st ‘𝑘) ∧ (2nd
‘𝑧) = (2nd
‘𝑘)) ↔ 𝑧 = 𝑘)) |
198 | 197 | ad2antlr 727 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
(((1st ‘𝑧)
= (1st ‘𝑘)
∧ (2nd ‘𝑧) = (2nd ‘𝑘)) ↔ 𝑧 = 𝑘)) |
199 | 193, 195,
198 | mpbi2and 712 |
. . . 4
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0)) →
𝑧 = 𝑘) |
200 | 199 | ex 416 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) → (((2nd ‘𝑧) = 0 ∧ (2nd
‘𝑘) = 0) → 𝑧 = 𝑘)) |
201 | 200 | ralrimivva 3113 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 ∀𝑘 ∈ 𝑆 (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑘) = 0) → 𝑧 = 𝑘)) |
202 | | fveqeq2 6745 |
. . 3
⊢ (𝑧 = 𝑘 → ((2nd ‘𝑧) = 0 ↔ (2nd
‘𝑘) =
0)) |
203 | 202 | rmo4 3658 |
. 2
⊢
(∃*𝑧 ∈
𝑆 (2nd
‘𝑧) = 0 ↔
∀𝑧 ∈ 𝑆 ∀𝑘 ∈ 𝑆 (((2nd ‘𝑧) = 0 ∧ (2nd ‘𝑘) = 0) → 𝑧 = 𝑘)) |
204 | 201, 203 | sylibr 237 |
1
⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 0) |