Step | Hyp | Ref
| Expression |
1 | | hashf 14244 |
. . . 4
β’
β―:VβΆ(β0 βͺ {+β}) |
2 | | ffun 6672 |
. . . 4
β’
(β―:VβΆ(β0 βͺ {+β}) β Fun
β―) |
3 | 1, 2 | ax-mp 5 |
. . 3
β’ Fun
β― |
4 | | erdszelem.a |
. . . 4
β’ (π β π΄ β (1...π)) |
5 | | erdsze.n |
. . . . 5
β’ (π β π β β) |
6 | | erdsze.f |
. . . . 5
β’ (π β πΉ:(1...π)β1-1ββ) |
7 | | erdszelem.k |
. . . . 5
β’ πΎ = (π₯ β (1...π) β¦ sup((β― β {π¦ β π« (1...π₯) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π₯ β π¦)}), β, < )) |
8 | | erdszelem.o |
. . . . 5
β’ π Or β |
9 | 5, 6, 7, 8 | erdszelem5 33846 |
. . . 4
β’ ((π β§ π΄ β (1...π)) β (πΎβπ΄) β (β― β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)})) |
10 | 4, 9 | mpdan 686 |
. . 3
β’ (π β (πΎβπ΄) β (β― β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)})) |
11 | | fvelima 6909 |
. . 3
β’ ((Fun
β― β§ (πΎβπ΄) β (β― β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)})) β βπ β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)} (β―βπ ) = (πΎβπ΄)) |
12 | 3, 10, 11 | sylancr 588 |
. 2
β’ (π β βπ β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)} (β―βπ ) = (πΎβπ΄)) |
13 | | eqid 2733 |
. . . . . 6
β’ {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)} = {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)} |
14 | 13 | erdszelem1 33842 |
. . . . 5
β’ (π β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)} β (π β (1...π΄) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π )) β§ π΄ β π )) |
15 | | simprl1 1219 |
. . . . . . . . 9
β’ ((π β§ ((π β (1...π΄) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π )) β§ π΄ β π ) β§ (β―βπ ) = (πΎβπ΄))) β π β (1...π΄)) |
16 | | elfzuz3 13444 |
. . . . . . . . . . 11
β’ (π΄ β (1...π) β π β (β€β₯βπ΄)) |
17 | | fzss2 13487 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ΄) β (1...π΄) β (1...π)) |
18 | 4, 16, 17 | 3syl 18 |
. . . . . . . . . 10
β’ (π β (1...π΄) β (1...π)) |
19 | 18 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((π β (1...π΄) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π )) β§ π΄ β π ) β§ (β―βπ ) = (πΎβπ΄))) β (1...π΄) β (1...π)) |
20 | 15, 19 | sstrd 3955 |
. . . . . . . 8
β’ ((π β§ ((π β (1...π΄) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π )) β§ π΄ β π ) β§ (β―βπ ) = (πΎβπ΄))) β π β (1...π)) |
21 | | velpw 4566 |
. . . . . . . 8
β’ (π β π« (1...π) β π β (1...π)) |
22 | 20, 21 | sylibr 233 |
. . . . . . 7
β’ ((π β§ ((π β (1...π΄) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π )) β§ π΄ β π ) β§ (β―βπ ) = (πΎβπ΄))) β π β π« (1...π)) |
23 | | erdszelem7.m |
. . . . . . . . . . 11
β’ (π β Β¬ (πΎβπ΄) β (1...(π
β 1))) |
24 | 5, 6, 7, 8 | erdszelem6 33847 |
. . . . . . . . . . . . . . 15
β’ (π β πΎ:(1...π)βΆβ) |
25 | 24, 4 | ffvelcdmd 7037 |
. . . . . . . . . . . . . 14
β’ (π β (πΎβπ΄) β β) |
26 | | nnuz 12811 |
. . . . . . . . . . . . . 14
β’ β =
(β€β₯β1) |
27 | 25, 26 | eleqtrdi 2844 |
. . . . . . . . . . . . 13
β’ (π β (πΎβπ΄) β
(β€β₯β1)) |
28 | | erdszelem7.r |
. . . . . . . . . . . . . 14
β’ (π β π
β β) |
29 | | nnz 12525 |
. . . . . . . . . . . . . 14
β’ (π
β β β π
β
β€) |
30 | | peano2zm 12551 |
. . . . . . . . . . . . . 14
β’ (π
β β€ β (π
β 1) β
β€) |
31 | 28, 29, 30 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β (π
β 1) β β€) |
32 | | elfz5 13439 |
. . . . . . . . . . . . 13
β’ (((πΎβπ΄) β (β€β₯β1)
β§ (π
β 1) β
β€) β ((πΎβπ΄) β (1...(π
β 1)) β (πΎβπ΄) β€ (π
β 1))) |
33 | 27, 31, 32 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β ((πΎβπ΄) β (1...(π
β 1)) β (πΎβπ΄) β€ (π
β 1))) |
34 | | nnltlem1 12575 |
. . . . . . . . . . . . 13
β’ (((πΎβπ΄) β β β§ π
β β) β ((πΎβπ΄) < π
β (πΎβπ΄) β€ (π
β 1))) |
35 | 25, 28, 34 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β ((πΎβπ΄) < π
β (πΎβπ΄) β€ (π
β 1))) |
36 | 33, 35 | bitr4d 282 |
. . . . . . . . . . 11
β’ (π β ((πΎβπ΄) β (1...(π
β 1)) β (πΎβπ΄) < π
)) |
37 | 23, 36 | mtbid 324 |
. . . . . . . . . 10
β’ (π β Β¬ (πΎβπ΄) < π
) |
38 | 28 | nnred 12173 |
. . . . . . . . . . 11
β’ (π β π
β β) |
39 | 13 | erdszelem2 33843 |
. . . . . . . . . . . . . 14
β’ ((β―
β {π¦ β π«
(1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)}) β Fin β§ (β― β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)}) β β) |
40 | 39 | simpri 487 |
. . . . . . . . . . . . 13
β’ (β―
β {π¦ β π«
(1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)}) β β |
41 | | nnssre 12162 |
. . . . . . . . . . . . 13
β’ β
β β |
42 | 40, 41 | sstri 3954 |
. . . . . . . . . . . 12
β’ (β―
β {π¦ β π«
(1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)}) β β |
43 | 42, 10 | sselid 3943 |
. . . . . . . . . . 11
β’ (π β (πΎβπ΄) β β) |
44 | 38, 43 | lenltd 11306 |
. . . . . . . . . 10
β’ (π β (π
β€ (πΎβπ΄) β Β¬ (πΎβπ΄) < π
)) |
45 | 37, 44 | mpbird 257 |
. . . . . . . . 9
β’ (π β π
β€ (πΎβπ΄)) |
46 | 45 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((π β (1...π΄) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π )) β§ π΄ β π ) β§ (β―βπ ) = (πΎβπ΄))) β π
β€ (πΎβπ΄)) |
47 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ ((π β (1...π΄) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π )) β§ π΄ β π ) β§ (β―βπ ) = (πΎβπ΄))) β (β―βπ ) = (πΎβπ΄)) |
48 | 46, 47 | breqtrrd 5134 |
. . . . . . 7
β’ ((π β§ ((π β (1...π΄) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π )) β§ π΄ β π ) β§ (β―βπ ) = (πΎβπ΄))) β π
β€ (β―βπ )) |
49 | | simprl2 1220 |
. . . . . . 7
β’ ((π β§ ((π β (1...π΄) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π )) β§ π΄ β π ) β§ (β―βπ ) = (πΎβπ΄))) β (πΉ βΎ π ) Isom < , π (π , (πΉ β π ))) |
50 | 22, 48, 49 | jca32 517 |
. . . . . 6
β’ ((π β§ ((π β (1...π΄) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π )) β§ π΄ β π ) β§ (β―βπ ) = (πΎβπ΄))) β (π β π« (1...π) β§ (π
β€ (β―βπ ) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π ))))) |
51 | 50 | expr 458 |
. . . . 5
β’ ((π β§ (π β (1...π΄) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π )) β§ π΄ β π )) β ((β―βπ ) = (πΎβπ΄) β (π β π« (1...π) β§ (π
β€ (β―βπ ) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π )))))) |
52 | 14, 51 | sylan2b 595 |
. . . 4
β’ ((π β§ π β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)}) β ((β―βπ ) = (πΎβπ΄) β (π β π« (1...π) β§ (π
β€ (β―βπ ) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π )))))) |
53 | 52 | expimpd 455 |
. . 3
β’ (π β ((π β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)} β§ (β―βπ ) = (πΎβπ΄)) β (π β π« (1...π) β§ (π
β€ (β―βπ ) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π )))))) |
54 | 53 | reximdv2 3158 |
. 2
β’ (π β (βπ β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)} (β―βπ ) = (πΎβπ΄) β βπ β π« (1...π)(π
β€ (β―βπ ) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π ))))) |
55 | 12, 54 | mpd 15 |
1
β’ (π β βπ β π« (1...π)(π
β€ (β―βπ ) β§ (πΉ βΎ π ) Isom < , π (π , (πΉ β π )))) |