Step | Hyp | Ref
| Expression |
1 | | axlowdimlem14.1 |
. . . . . . 7
β’ π = ({β¨(πΌ + 1), 1β©} βͺ (((1...π) β {(πΌ + 1)}) Γ {0})) |
2 | 1 | axlowdimlem10 28473 |
. . . . . 6
β’ ((π β β β§ πΌ β (1...(π β 1))) β π β (πΌβπ)) |
3 | | elee 28416 |
. . . . . . 7
β’ (π β β β (π β (πΌβπ) β π:(1...π)βΆβ)) |
4 | 3 | adantr 480 |
. . . . . 6
β’ ((π β β β§ πΌ β (1...(π β 1))) β (π β (πΌβπ) β π:(1...π)βΆβ)) |
5 | 2, 4 | mpbid 231 |
. . . . 5
β’ ((π β β β§ πΌ β (1...(π β 1))) β π:(1...π)βΆβ) |
6 | 5 | ffnd 6719 |
. . . 4
β’ ((π β β β§ πΌ β (1...(π β 1))) β π Fn (1...π)) |
7 | | axlowdimlem14.2 |
. . . . . . 7
β’ π
= ({β¨(π½ + 1), 1β©} βͺ (((1...π) β {(π½ + 1)}) Γ {0})) |
8 | 7 | axlowdimlem10 28473 |
. . . . . 6
β’ ((π β β β§ π½ β (1...(π β 1))) β π
β (πΌβπ)) |
9 | | elee 28416 |
. . . . . . 7
β’ (π β β β (π
β (πΌβπ) β π
:(1...π)βΆβ)) |
10 | 9 | adantr 480 |
. . . . . 6
β’ ((π β β β§ π½ β (1...(π β 1))) β (π
β (πΌβπ) β π
:(1...π)βΆβ)) |
11 | 8, 10 | mpbid 231 |
. . . . 5
β’ ((π β β β§ π½ β (1...(π β 1))) β π
:(1...π)βΆβ) |
12 | 11 | ffnd 6719 |
. . . 4
β’ ((π β β β§ π½ β (1...(π β 1))) β π
Fn (1...π)) |
13 | | eqfnfv 7033 |
. . . 4
β’ ((π Fn (1...π) β§ π
Fn (1...π)) β (π = π
β βπ β (1...π)(πβπ) = (π
βπ))) |
14 | 6, 12, 13 | syl2an 595 |
. . 3
β’ (((π β β β§ πΌ β (1...(π β 1))) β§ (π β β β§ π½ β (1...(π β 1)))) β (π = π
β βπ β (1...π)(πβπ) = (π
βπ))) |
15 | 14 | 3impdi 1349 |
. 2
β’ ((π β β β§ πΌ β (1...(π β 1)) β§ π½ β (1...(π β 1))) β (π = π
β βπ β (1...π)(πβπ) = (π
βπ))) |
16 | | fznatpl1 13560 |
. . . . . . 7
β’ ((π β β β§ πΌ β (1...(π β 1))) β (πΌ + 1) β (1...π)) |
17 | 16 | 3adant3 1131 |
. . . . . 6
β’ ((π β β β§ πΌ β (1...(π β 1)) β§ π½ β (1...(π β 1))) β (πΌ + 1) β (1...π)) |
18 | | ax-1ne0 11182 |
. . . . . . . 8
β’ 1 β
0 |
19 | 18 | a1i 11 |
. . . . . . 7
β’ (((π β β β§ πΌ β (1...(π β 1)) β§ π½ β (1...(π β 1))) β§ πΌ β π½) β 1 β 0) |
20 | 1 | axlowdimlem11 28474 |
. . . . . . . 8
β’ (πβ(πΌ + 1)) = 1 |
21 | 20 | a1i 11 |
. . . . . . 7
β’ (((π β β β§ πΌ β (1...(π β 1)) β§ π½ β (1...(π β 1))) β§ πΌ β π½) β (πβ(πΌ + 1)) = 1) |
22 | | elfzelz 13506 |
. . . . . . . . . . . . 13
β’ (πΌ β (1...(π β 1)) β πΌ β β€) |
23 | 22 | zcnd 12672 |
. . . . . . . . . . . 12
β’ (πΌ β (1...(π β 1)) β πΌ β β) |
24 | | elfzelz 13506 |
. . . . . . . . . . . . 13
β’ (π½ β (1...(π β 1)) β π½ β β€) |
25 | 24 | zcnd 12672 |
. . . . . . . . . . . 12
β’ (π½ β (1...(π β 1)) β π½ β β) |
26 | | ax-1cn 11171 |
. . . . . . . . . . . . 13
β’ 1 β
β |
27 | | addcan2 11404 |
. . . . . . . . . . . . 13
β’ ((πΌ β β β§ π½ β β β§ 1 β
β) β ((πΌ + 1) =
(π½ + 1) β πΌ = π½)) |
28 | 26, 27 | mp3an3 1449 |
. . . . . . . . . . . 12
β’ ((πΌ β β β§ π½ β β) β ((πΌ + 1) = (π½ + 1) β πΌ = π½)) |
29 | 23, 25, 28 | syl2an 595 |
. . . . . . . . . . 11
β’ ((πΌ β (1...(π β 1)) β§ π½ β (1...(π β 1))) β ((πΌ + 1) = (π½ + 1) β πΌ = π½)) |
30 | 29 | 3adant1 1129 |
. . . . . . . . . 10
β’ ((π β β β§ πΌ β (1...(π β 1)) β§ π½ β (1...(π β 1))) β ((πΌ + 1) = (π½ + 1) β πΌ = π½)) |
31 | 30 | necon3bid 2984 |
. . . . . . . . 9
β’ ((π β β β§ πΌ β (1...(π β 1)) β§ π½ β (1...(π β 1))) β ((πΌ + 1) β (π½ + 1) β πΌ β π½)) |
32 | 31 | biimpar 477 |
. . . . . . . 8
β’ (((π β β β§ πΌ β (1...(π β 1)) β§ π½ β (1...(π β 1))) β§ πΌ β π½) β (πΌ + 1) β (π½ + 1)) |
33 | 7 | axlowdimlem12 28475 |
. . . . . . . 8
β’ (((πΌ + 1) β (1...π) β§ (πΌ + 1) β (π½ + 1)) β (π
β(πΌ + 1)) = 0) |
34 | 17, 32, 33 | syl2an2r 682 |
. . . . . . 7
β’ (((π β β β§ πΌ β (1...(π β 1)) β§ π½ β (1...(π β 1))) β§ πΌ β π½) β (π
β(πΌ + 1)) = 0) |
35 | 19, 21, 34 | 3netr4d 3017 |
. . . . . 6
β’ (((π β β β§ πΌ β (1...(π β 1)) β§ π½ β (1...(π β 1))) β§ πΌ β π½) β (πβ(πΌ + 1)) β (π
β(πΌ + 1))) |
36 | | df-ne 2940 |
. . . . . . . 8
β’ ((πβπ) β (π
βπ) β Β¬ (πβπ) = (π
βπ)) |
37 | | fveq2 6892 |
. . . . . . . . 9
β’ (π = (πΌ + 1) β (πβπ) = (πβ(πΌ + 1))) |
38 | | fveq2 6892 |
. . . . . . . . 9
β’ (π = (πΌ + 1) β (π
βπ) = (π
β(πΌ + 1))) |
39 | 37, 38 | neeq12d 3001 |
. . . . . . . 8
β’ (π = (πΌ + 1) β ((πβπ) β (π
βπ) β (πβ(πΌ + 1)) β (π
β(πΌ + 1)))) |
40 | 36, 39 | bitr3id 284 |
. . . . . . 7
β’ (π = (πΌ + 1) β (Β¬ (πβπ) = (π
βπ) β (πβ(πΌ + 1)) β (π
β(πΌ + 1)))) |
41 | 40 | rspcev 3613 |
. . . . . 6
β’ (((πΌ + 1) β (1...π) β§ (πβ(πΌ + 1)) β (π
β(πΌ + 1))) β βπ β (1...π) Β¬ (πβπ) = (π
βπ)) |
42 | 17, 35, 41 | syl2an2r 682 |
. . . . 5
β’ (((π β β β§ πΌ β (1...(π β 1)) β§ π½ β (1...(π β 1))) β§ πΌ β π½) β βπ β (1...π) Β¬ (πβπ) = (π
βπ)) |
43 | 42 | ex 412 |
. . . 4
β’ ((π β β β§ πΌ β (1...(π β 1)) β§ π½ β (1...(π β 1))) β (πΌ β π½ β βπ β (1...π) Β¬ (πβπ) = (π
βπ))) |
44 | | df-ne 2940 |
. . . 4
β’ (πΌ β π½ β Β¬ πΌ = π½) |
45 | | rexnal 3099 |
. . . 4
β’
(βπ β
(1...π) Β¬ (πβπ) = (π
βπ) β Β¬ βπ β (1...π)(πβπ) = (π
βπ)) |
46 | 43, 44, 45 | 3imtr3g 294 |
. . 3
β’ ((π β β β§ πΌ β (1...(π β 1)) β§ π½ β (1...(π β 1))) β (Β¬ πΌ = π½ β Β¬ βπ β (1...π)(πβπ) = (π
βπ))) |
47 | 46 | con4d 115 |
. 2
β’ ((π β β β§ πΌ β (1...(π β 1)) β§ π½ β (1...(π β 1))) β (βπ β (1...π)(πβπ) = (π
βπ) β πΌ = π½)) |
48 | 15, 47 | sylbid 239 |
1
β’ ((π β β β§ πΌ β (1...(π β 1)) β§ π½ β (1...(π β 1))) β (π = π
β πΌ = π½)) |