Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → 𝑁 ∈ ℕ) |
3 | | poimirlem22.s |
. . . . . . . 8
⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
4 | | simplrl 800 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → 𝑧 ∈ 𝑆) |
5 | 1 | nngt0d 11064 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 𝑁) |
6 | | breq2 4657 |
. . . . . . . . . . 11
⊢
((2nd ‘𝑧) = 𝑁 → (0 < (2nd ‘𝑧) ↔ 0 < 𝑁)) |
7 | 6 | biimparc 504 |
. . . . . . . . . 10
⊢ ((0 <
𝑁 ∧ (2nd
‘𝑧) = 𝑁) → 0 < (2nd
‘𝑧)) |
8 | 5, 7 | sylan 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (2nd
‘𝑧) = 𝑁) → 0 < (2nd
‘𝑧)) |
9 | 8 | ad2ant2r 783 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → 0 < (2nd
‘𝑧)) |
10 | 2, 3, 4, 9 | poimirlem5 33414 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → (𝐹‘0) = (1st
‘(1st ‘𝑧))) |
11 | | simplrr 801 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → 𝑘 ∈ 𝑆) |
12 | | breq2 4657 |
. . . . . . . . . . 11
⊢
((2nd ‘𝑘) = 𝑁 → (0 < (2nd ‘𝑘) ↔ 0 < 𝑁)) |
13 | 12 | biimparc 504 |
. . . . . . . . . 10
⊢ ((0 <
𝑁 ∧ (2nd
‘𝑘) = 𝑁) → 0 < (2nd
‘𝑘)) |
14 | 5, 13 | sylan 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (2nd
‘𝑘) = 𝑁) → 0 < (2nd
‘𝑘)) |
15 | 14 | ad2ant2rl 785 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → 0 < (2nd
‘𝑘)) |
16 | 2, 3, 11, 15 | poimirlem5 33414 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → (𝐹‘0) = (1st
‘(1st ‘𝑘))) |
17 | 10, 16 | eqtr3d 2658 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → (1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑘))) |
18 | | elrabi 3359 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ {𝑡 ∈ ((((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...𝑁))) |
19 | 18, 3 | eleq2s 2719 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
20 | | xp1st 7198 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑧) ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
21 | | xp2nd 7199 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
23 | | fvex 6201 |
. . . . . . . . . . . 12
⊢
(2nd ‘(1st ‘𝑧)) ∈ V |
24 | | f1oeq1 6127 |
. . . . . . . . . . . 12
⊢ (𝑓 = (2nd
‘(1st ‘𝑧)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁))) |
25 | 23, 24 | elab 3350 |
. . . . . . . . . . 11
⊢
((2nd ‘(1st ‘𝑧)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
26 | 22, 25 | sylib 208 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁)) |
27 | | f1ofn 6138 |
. . . . . . . . . 10
⊢
((2nd ‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑧)) Fn (1...𝑁)) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑆 → (2nd
‘(1st ‘𝑧)) Fn (1...𝑁)) |
29 | 28 | adantr 481 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) → (2nd
‘(1st ‘𝑧)) Fn (1...𝑁)) |
30 | 29 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → (2nd
‘(1st ‘𝑧)) Fn (1...𝑁)) |
31 | | elrabi 3359 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ {𝑡 ∈ ((((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...𝑁))) |
32 | 31, 3 | eleq2s 2719 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑆 → 𝑘 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
33 | | xp1st 7198 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑘) ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
34 | | xp2nd 7199 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑘) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑘)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
35 | 32, 33, 34 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑆 → (2nd
‘(1st ‘𝑘)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
36 | | fvex 6201 |
. . . . . . . . . . . 12
⊢
(2nd ‘(1st ‘𝑘)) ∈ V |
37 | | f1oeq1 6127 |
. . . . . . . . . . . 12
⊢ (𝑓 = (2nd
‘(1st ‘𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))) |
38 | 36, 37 | elab 3350 |
. . . . . . . . . . 11
⊢
((2nd ‘(1st ‘𝑘)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)) |
39 | 35, 38 | sylib 208 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝑆 → (2nd
‘(1st ‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)) |
40 | | f1ofn 6138 |
. . . . . . . . . 10
⊢
((2nd ‘(1st ‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑘)) Fn (1...𝑁)) |
41 | 39, 40 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝑆 → (2nd
‘(1st ‘𝑘)) Fn (1...𝑁)) |
42 | 41 | adantl 482 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) → (2nd
‘(1st ‘𝑘)) Fn (1...𝑁)) |
43 | 42 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → (2nd
‘(1st ‘𝑘)) Fn (1...𝑁)) |
44 | | simpllr 799 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) |
45 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑁 → (1...𝑛) = (1...𝑁)) |
46 | 45 | imaeq2d 5466 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑁 → ((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) = ((2nd ‘(1st
‘𝑧)) “
(1...𝑁))) |
47 | | f1ofo 6144 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑧)):(1...𝑁)–onto→(1...𝑁)) |
48 | | foima 6120 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑧)):(1...𝑁)–onto→(1...𝑁) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑁)) = (1...𝑁)) |
49 | 26, 47, 48 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑆 → ((2nd
‘(1st ‘𝑧)) “ (1...𝑁)) = (1...𝑁)) |
50 | 46, 49 | sylan9eqr 2678 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 = 𝑁) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) = (1...𝑁)) |
51 | 50 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ 𝑛 = 𝑁) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) = (1...𝑁)) |
52 | 45 | imaeq2d 5466 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑁 → ((2nd
‘(1st ‘𝑘)) “ (1...𝑛)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑁))) |
53 | | f1ofo 6144 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑘)):(1...𝑁)–onto→(1...𝑁)) |
54 | | foima 6120 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑘)):(1...𝑁)–onto→(1...𝑁) → ((2nd
‘(1st ‘𝑘)) “ (1...𝑁)) = (1...𝑁)) |
55 | 39, 53, 54 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ 𝑆 → ((2nd
‘(1st ‘𝑘)) “ (1...𝑁)) = (1...𝑁)) |
56 | 52, 55 | sylan9eqr 2678 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ 𝑆 ∧ 𝑛 = 𝑁) → ((2nd
‘(1st ‘𝑘)) “ (1...𝑛)) = (1...𝑁)) |
57 | 56 | adantll 750 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ 𝑛 = 𝑁) → ((2nd
‘(1st ‘𝑘)) “ (1...𝑛)) = (1...𝑁)) |
58 | 51, 57 | eqtr4d 2659 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ 𝑛 = 𝑁) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑛))) |
59 | 44, 58 | sylan 488 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 = 𝑁) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑛))) |
60 | | simpll 790 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → 𝜑) |
61 | | elnnuz 11724 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈
(ℤ≥‘1)) |
62 | 1, 61 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
63 | | fzm1 12420 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘1) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁))) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑛 ∈ (1...𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁))) |
65 | 64 | anbi1d 741 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ 𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛 ≠ 𝑁))) |
66 | 65 | biimpa 501 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ 𝑁)) → ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛 ≠ 𝑁)) |
67 | | df-ne 2795 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ≠ 𝑁 ↔ ¬ 𝑛 = 𝑁) |
68 | 67 | anbi2i 730 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛 ≠ 𝑁) ↔ ((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ ¬ 𝑛 = 𝑁)) |
69 | | pm5.61 749 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ ¬ 𝑛 = 𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁)) |
70 | 68, 69 | bitri 264 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ (1...(𝑁 − 1)) ∨ 𝑛 = 𝑁) ∧ 𝑛 ≠ 𝑁) ↔ (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁)) |
71 | 66, 70 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ 𝑁)) → (𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁)) |
72 | | 1eluzge0 11732 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
(ℤ≥‘0) |
73 | | fzss1 12380 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
(ℤ≥‘0) → (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))) |
74 | 72, 73 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(1...(𝑁 − 1))
⊆ (0...(𝑁 −
1)) |
75 | 74 | sseli 3599 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (1...(𝑁 − 1)) → 𝑛 ∈ (0...(𝑁 − 1))) |
76 | 75 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ (1...(𝑁 − 1)) ∧ ¬ 𝑛 = 𝑁) → 𝑛 ∈ (0...(𝑁 − 1))) |
77 | 71, 76 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ 𝑁)) → 𝑛 ∈ (0...(𝑁 − 1))) |
78 | 60, 77 | sylan 488 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ 𝑁)) → 𝑛 ∈ (0...(𝑁 − 1))) |
79 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑛 → (𝑚 ∈ (0...(𝑁 − 1)) ↔ 𝑛 ∈ (0...(𝑁 − 1)))) |
80 | 79 | anbi2d 740 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑛 → ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) ↔ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑛 ∈ (0...(𝑁 − 1))))) |
81 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛)) |
82 | 81 | imaeq2d 5466 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑛 → ((2nd
‘(1st ‘𝑧)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑧)) “
(1...𝑛))) |
83 | 81 | imaeq2d 5466 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑛 → ((2nd
‘(1st ‘𝑘)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑛))) |
84 | 82, 83 | eqeq12d 2637 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑛 → (((2nd
‘(1st ‘𝑧)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑚)) ↔
((2nd ‘(1st ‘𝑧)) “ (1...𝑛)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑛)))) |
85 | 80, 84 | imbi12d 334 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑚))) ↔ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑛))))) |
86 | 1 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℕ) |
87 | | poimirlem22.1 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁))) |
88 | 87 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁))) |
89 | | simpl 473 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) → 𝑧 ∈ 𝑆) |
90 | 89 | ad3antlr 767 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑧 ∈ 𝑆) |
91 | | simplrl 800 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → (2nd
‘𝑧) = 𝑁) |
92 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ 𝑆) |
93 | 92 | ad3antlr 767 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ 𝑆) |
94 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → (2nd
‘𝑘) = 𝑁) |
95 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑚 ∈ (0...(𝑁 − 1))) |
96 | 86, 3, 88, 90, 91, 93, 94, 95 | poimirlem12 33421 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑚)) ⊆ ((2nd
‘(1st ‘𝑘)) “ (1...𝑚))) |
97 | 86, 3, 88, 93, 94, 90, 91, 95 | poimirlem12 33421 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑘)) “ (1...𝑚)) ⊆ ((2nd
‘(1st ‘𝑧)) “ (1...𝑚))) |
98 | 96, 97 | eqssd 3620 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑚))) |
99 | 85, 98 | chvarv 2263 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑛))) |
100 | 78, 99 | syldan 487 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ 𝑁)) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑛))) |
101 | 100 | anassrs 680 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 ≠ 𝑁) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑛))) |
102 | 59, 101 | pm2.61dane 2881 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑛))) |
103 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁)) |
104 | | elfzelz 12342 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ) |
105 | 1 | nnzd 11481 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℤ) |
106 | | elfzm1b 12418 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1)))) |
107 | 104, 105,
106 | syl2anr 495 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1)))) |
108 | 103, 107 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ (0...(𝑁 − 1))) |
109 | 60, 108 | sylan 488 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ (0...(𝑁 − 1))) |
110 | | ovex 6678 |
. . . . . . . . . . . 12
⊢ (𝑛 − 1) ∈
V |
111 | | eleq1 2689 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 − 1) → (𝑚 ∈ (0...(𝑁 − 1)) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1)))) |
112 | 111 | anbi2d 740 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 − 1) → ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) ↔ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ (𝑛 − 1) ∈ (0...(𝑁 − 1))))) |
113 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (𝑛 − 1) → (1...𝑚) = (1...(𝑛 − 1))) |
114 | 113 | imaeq2d 5466 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 − 1) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑧)) “
(1...(𝑛 −
1)))) |
115 | 113 | imaeq2d 5466 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 − 1) → ((2nd
‘(1st ‘𝑘)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑘)) “
(1...(𝑛 −
1)))) |
116 | 114, 115 | eqeq12d 2637 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 − 1) → (((2nd
‘(1st ‘𝑧)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑚)) ↔
((2nd ‘(1st ‘𝑧)) “ (1...(𝑛 − 1))) = ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1))))) |
117 | 112, 116 | imbi12d 334 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 − 1) → (((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑧)) “ (1...𝑚)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑚))) ↔ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ (𝑛 − 1) ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1))) = ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1)))))) |
118 | 110, 117,
98 | vtocl 3259 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ (𝑛 − 1) ∈ (0...(𝑁 − 1))) → ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1))) = ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1)))) |
119 | 109, 118 | syldan 487 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1))) = ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1)))) |
120 | 102, 119 | difeq12d 3729 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) ∖ ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1)))) = (((2nd
‘(1st ‘𝑘)) “ (1...𝑛)) ∖ ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1))))) |
121 | | fnsnfv 6258 |
. . . . . . . . . . . 12
⊢
(((2nd ‘(1st ‘𝑧)) Fn (1...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑧))‘𝑛)} = ((2nd ‘(1st
‘𝑧)) “ {𝑛})) |
122 | 28, 121 | sylan 488 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑧))‘𝑛)} = ((2nd ‘(1st
‘𝑧)) “ {𝑛})) |
123 | | elfznn 12370 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ) |
124 | | uncom 3757 |
. . . . . . . . . . . . . . . . 17
⊢
((1...(𝑛 − 1))
∪ {𝑛}) = ({𝑛} ∪ (1...(𝑛 − 1))) |
125 | 124 | difeq1i 3724 |
. . . . . . . . . . . . . . . 16
⊢
(((1...(𝑛 −
1)) ∪ {𝑛}) ∖
(1...(𝑛 − 1))) =
(({𝑛} ∪ (1...(𝑛 − 1))) ∖
(1...(𝑛 −
1))) |
126 | | difun2 4048 |
. . . . . . . . . . . . . . . 16
⊢ (({𝑛} ∪ (1...(𝑛 − 1))) ∖ (1...(𝑛 − 1))) = ({𝑛} ∖ (1...(𝑛 − 1))) |
127 | 125, 126 | eqtri 2644 |
. . . . . . . . . . . . . . 15
⊢
(((1...(𝑛 −
1)) ∪ {𝑛}) ∖
(1...(𝑛 − 1))) =
({𝑛} ∖ (1...(𝑛 − 1))) |
128 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
129 | | npcan1 10455 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛) |
130 | 128, 129 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) = 𝑛) |
131 | | elnnuz 11724 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘1)) |
132 | 131 | biimpi 206 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
(ℤ≥‘1)) |
133 | 130, 132 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) ∈
(ℤ≥‘1)) |
134 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
135 | 134 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℤ) |
136 | | uzid 11702 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 − 1) ∈ ℤ
→ (𝑛 − 1) ∈
(ℤ≥‘(𝑛 − 1))) |
137 | | peano2uz 11741 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 − 1) ∈
(ℤ≥‘(𝑛 − 1)) → ((𝑛 − 1) + 1) ∈
(ℤ≥‘(𝑛 − 1))) |
138 | 135, 136,
137 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → ((𝑛 − 1) + 1) ∈
(ℤ≥‘(𝑛 − 1))) |
139 | 130, 138 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
(ℤ≥‘(𝑛 − 1))) |
140 | | fzsplit2 12366 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑛 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘(𝑛 − 1))) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛))) |
141 | 133, 139,
140 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
(1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛))) |
142 | 130 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → (((𝑛 − 1) + 1)...𝑛) = (𝑛...𝑛)) |
143 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
144 | | fzsn 12383 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℤ → (𝑛...𝑛) = {𝑛}) |
145 | 143, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → (𝑛...𝑛) = {𝑛}) |
146 | 142, 145 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → (((𝑛 − 1) + 1)...𝑛) = {𝑛}) |
147 | 146 | uneq2d 3767 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
((1...(𝑛 − 1)) ∪
(((𝑛 − 1) +
1)...𝑛)) = ((1...(𝑛 − 1)) ∪ {𝑛})) |
148 | 141, 147 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ →
(1...𝑛) = ((1...(𝑛 − 1)) ∪ {𝑛})) |
149 | 148 | difeq1d 3727 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
((1...𝑛) ∖
(1...(𝑛 − 1))) =
(((1...(𝑛 − 1)) ∪
{𝑛}) ∖ (1...(𝑛 − 1)))) |
150 | | nnre 11027 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
151 | | ltm1 10863 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) < 𝑛) |
152 | | peano2rem 10348 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈
ℝ) |
153 | | ltnle 10117 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 − 1) ∈ ℝ ∧
𝑛 ∈ ℝ) →
((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1))) |
154 | 152, 153 | mpancom 703 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℝ → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1))) |
155 | 151, 154 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℝ → ¬
𝑛 ≤ (𝑛 − 1)) |
156 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...(𝑛 − 1)) → 𝑛 ≤ (𝑛 − 1)) |
157 | 155, 156 | nsyl 135 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ → ¬
𝑛 ∈ (1...(𝑛 − 1))) |
158 | 150, 157 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ¬
𝑛 ∈ (1...(𝑛 − 1))) |
159 | | incom 3805 |
. . . . . . . . . . . . . . . . . 18
⊢
((1...(𝑛 − 1))
∩ {𝑛}) = ({𝑛} ∩ (1...(𝑛 − 1))) |
160 | 159 | eqeq1i 2627 |
. . . . . . . . . . . . . . . . 17
⊢
(((1...(𝑛 −
1)) ∩ {𝑛}) = ∅
↔ ({𝑛} ∩
(1...(𝑛 − 1))) =
∅) |
161 | | disjsn 4246 |
. . . . . . . . . . . . . . . . 17
⊢
(((1...(𝑛 −
1)) ∩ {𝑛}) = ∅
↔ ¬ 𝑛 ∈
(1...(𝑛 −
1))) |
162 | | disj3 4021 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝑛} ∩ (1...(𝑛 − 1))) = ∅ ↔ {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1)))) |
163 | 160, 161,
162 | 3bitr3i 290 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑛 ∈ (1...(𝑛 − 1)) ↔ {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1)))) |
164 | 158, 163 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → {𝑛} = ({𝑛} ∖ (1...(𝑛 − 1)))) |
165 | 127, 149,
164 | 3eqtr4a 2682 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
((1...𝑛) ∖
(1...(𝑛 − 1))) =
{𝑛}) |
166 | 123, 165 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...𝑁) → ((1...𝑛) ∖ (1...(𝑛 − 1))) = {𝑛}) |
167 | 166 | imaeq2d 5466 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (1...𝑁) → ((2nd
‘(1st ‘𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = ((2nd
‘(1st ‘𝑧)) “ {𝑛})) |
168 | 167 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = ((2nd
‘(1st ‘𝑧)) “ {𝑛})) |
169 | | dff1o3 6143 |
. . . . . . . . . . . . . 14
⊢
((2nd ‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd
‘(1st ‘𝑧)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡(2nd ‘(1st
‘𝑧)))) |
170 | 169 | simprbi 480 |
. . . . . . . . . . . . 13
⊢
((2nd ‘(1st ‘𝑧)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡(2nd ‘(1st
‘𝑧))) |
171 | | imadif 5973 |
. . . . . . . . . . . . 13
⊢ (Fun
◡(2nd ‘(1st
‘𝑧)) →
((2nd ‘(1st ‘𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = (((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) ∖ ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1))))) |
172 | 26, 170, 171 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑆 → ((2nd
‘(1st ‘𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = (((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) ∖ ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1))))) |
173 | 172 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑧)) “ ((1...𝑛) ∖ (1...(𝑛 − 1)))) = (((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) ∖ ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1))))) |
174 | 122, 168,
173 | 3eqtr2d 2662 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑧))‘𝑛)} = (((2nd ‘(1st
‘𝑧)) “
(1...𝑛)) ∖
((2nd ‘(1st ‘𝑧)) “ (1...(𝑛 − 1))))) |
175 | 4, 174 | sylan 488 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑧))‘𝑛)} = (((2nd ‘(1st
‘𝑧)) “
(1...𝑛)) ∖
((2nd ‘(1st ‘𝑧)) “ (1...(𝑛 − 1))))) |
176 | | eleq1 2689 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑘 → (𝑧 ∈ 𝑆 ↔ 𝑘 ∈ 𝑆)) |
177 | 176 | anbi1d 741 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑘 → ((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) ↔ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)))) |
178 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑘 → (1st ‘𝑧) = (1st ‘𝑘)) |
179 | 178 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑘 → (2nd
‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑘))) |
180 | 179 | fveq1d 6193 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑘 → ((2nd
‘(1st ‘𝑧))‘𝑛) = ((2nd ‘(1st
‘𝑘))‘𝑛)) |
181 | 180 | sneqd 4189 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑘 → {((2nd
‘(1st ‘𝑧))‘𝑛)} = {((2nd ‘(1st
‘𝑘))‘𝑛)}) |
182 | 179 | imaeq1d 5465 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑘 → ((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) = ((2nd ‘(1st
‘𝑘)) “
(1...𝑛))) |
183 | 179 | imaeq1d 5465 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑘 → ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1))) = ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1)))) |
184 | 182, 183 | difeq12d 3729 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑘 → (((2nd
‘(1st ‘𝑧)) “ (1...𝑛)) ∖ ((2nd
‘(1st ‘𝑧)) “ (1...(𝑛 − 1)))) = (((2nd
‘(1st ‘𝑘)) “ (1...𝑛)) ∖ ((2nd
‘(1st ‘𝑘)) “ (1...(𝑛 − 1))))) |
185 | 181, 184 | eqeq12d 2637 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑘 → ({((2nd
‘(1st ‘𝑧))‘𝑛)} = (((2nd ‘(1st
‘𝑧)) “
(1...𝑛)) ∖
((2nd ‘(1st ‘𝑧)) “ (1...(𝑛 − 1)))) ↔ {((2nd
‘(1st ‘𝑘))‘𝑛)} = (((2nd ‘(1st
‘𝑘)) “
(1...𝑛)) ∖
((2nd ‘(1st ‘𝑘)) “ (1...(𝑛 − 1)))))) |
186 | 177, 185 | imbi12d 334 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑘 → (((𝑧 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑧))‘𝑛)} = (((2nd ‘(1st
‘𝑧)) “
(1...𝑛)) ∖
((2nd ‘(1st ‘𝑧)) “ (1...(𝑛 − 1))))) ↔ ((𝑘 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑘))‘𝑛)} = (((2nd ‘(1st
‘𝑘)) “
(1...𝑛)) ∖
((2nd ‘(1st ‘𝑘)) “ (1...(𝑛 − 1))))))) |
187 | 186, 174 | chvarv 2263 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ 𝑆 ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑘))‘𝑛)} = (((2nd ‘(1st
‘𝑘)) “
(1...𝑛)) ∖
((2nd ‘(1st ‘𝑘)) “ (1...(𝑛 − 1))))) |
188 | 11, 187 | sylan 488 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑘))‘𝑛)} = (((2nd ‘(1st
‘𝑘)) “
(1...𝑛)) ∖
((2nd ‘(1st ‘𝑘)) “ (1...(𝑛 − 1))))) |
189 | 120, 175,
188 | 3eqtr4d 2666 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑧))‘𝑛)} = {((2nd ‘(1st
‘𝑘))‘𝑛)}) |
190 | | fvex 6201 |
. . . . . . . . 9
⊢
((2nd ‘(1st ‘𝑧))‘𝑛) ∈ V |
191 | 190 | sneqr 4371 |
. . . . . . . 8
⊢
({((2nd ‘(1st ‘𝑧))‘𝑛)} = {((2nd ‘(1st
‘𝑘))‘𝑛)} → ((2nd
‘(1st ‘𝑧))‘𝑛) = ((2nd ‘(1st
‘𝑘))‘𝑛)) |
192 | 189, 191 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((2nd
‘(1st ‘𝑧))‘𝑛) = ((2nd ‘(1st
‘𝑘))‘𝑛)) |
193 | 30, 43, 192 | eqfnfvd 6314 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → (2nd
‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑘))) |
194 | 19, 20 | syl 17 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑆 → (1st ‘𝑧) ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
195 | 32, 33 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝑆 → (1st ‘𝑘) ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
196 | | xpopth 7207 |
. . . . . . . 8
⊢
(((1st ‘𝑧) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (1st ‘𝑘) ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) → (((1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑘)) ∧
(2nd ‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑘))) ↔
(1st ‘𝑧) =
(1st ‘𝑘))) |
197 | 194, 195,
196 | syl2an 494 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) → (((1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑘)) ∧
(2nd ‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑘))) ↔
(1st ‘𝑧) =
(1st ‘𝑘))) |
198 | 197 | ad2antlr 763 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → (((1st
‘(1st ‘𝑧)) = (1st ‘(1st
‘𝑘)) ∧
(2nd ‘(1st ‘𝑧)) = (2nd ‘(1st
‘𝑘))) ↔
(1st ‘𝑧) =
(1st ‘𝑘))) |
199 | 17, 193, 198 | mpbi2and 956 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → (1st ‘𝑧) = (1st ‘𝑘)) |
200 | | eqtr3 2643 |
. . . . . 6
⊢
(((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁) → (2nd ‘𝑧) = (2nd ‘𝑘)) |
201 | 200 | adantl 482 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → (2nd ‘𝑧) = (2nd ‘𝑘)) |
202 | | xpopth 7207 |
. . . . . . 7
⊢ ((𝑧 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝑘 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) → (((1st ‘𝑧) = (1st ‘𝑘) ∧ (2nd
‘𝑧) = (2nd
‘𝑘)) ↔ 𝑧 = 𝑘)) |
203 | 19, 32, 202 | syl2an 494 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) → (((1st ‘𝑧) = (1st ‘𝑘) ∧ (2nd
‘𝑧) = (2nd
‘𝑘)) ↔ 𝑧 = 𝑘)) |
204 | 203 | ad2antlr 763 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → (((1st ‘𝑧) = (1st ‘𝑘) ∧ (2nd
‘𝑧) = (2nd
‘𝑘)) ↔ 𝑧 = 𝑘)) |
205 | 199, 201,
204 | mpbi2and 956 |
. . . 4
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) ∧ ((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁)) → 𝑧 = 𝑘) |
206 | 205 | ex 450 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) → (((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁) → 𝑧 = 𝑘)) |
207 | 206 | ralrimivva 2971 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 ∀𝑘 ∈ 𝑆 (((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁) → 𝑧 = 𝑘)) |
208 | | fveq2 6191 |
. . . 4
⊢ (𝑧 = 𝑘 → (2nd ‘𝑧) = (2nd ‘𝑘)) |
209 | 208 | eqeq1d 2624 |
. . 3
⊢ (𝑧 = 𝑘 → ((2nd ‘𝑧) = 𝑁 ↔ (2nd ‘𝑘) = 𝑁)) |
210 | 209 | rmo4 3399 |
. 2
⊢
(∃*𝑧 ∈
𝑆 (2nd
‘𝑧) = 𝑁 ↔ ∀𝑧 ∈ 𝑆 ∀𝑘 ∈ 𝑆 (((2nd ‘𝑧) = 𝑁 ∧ (2nd ‘𝑘) = 𝑁) → 𝑧 = 𝑘)) |
211 | 207, 210 | sylibr 224 |
1
⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 𝑁) |