Step | Hyp | Ref
| Expression |
1 | | nnex 12164 |
. . . . 5
β’ β
β V |
2 | 1 | ssex 5279 |
. . . 4
β’ (π΄ β β β π΄ β V) |
3 | | 1z 12538 |
. . . . . . . 8
β’ 1 β
β€ |
4 | | unbenlem.1 |
. . . . . . . 8
β’ πΊ = (rec((π₯ β V β¦ (π₯ + 1)), 1) βΎ Ο) |
5 | 3, 4 | om2uzf1oi 13864 |
. . . . . . 7
β’ πΊ:Οβ1-1-ontoβ(β€β₯β1) |
6 | | nnuz 12811 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
7 | | f1oeq3 6775 |
. . . . . . . 8
β’ (β
= (β€β₯β1) β (πΊ:Οβ1-1-ontoββ β πΊ:Οβ1-1-ontoβ(β€β₯β1))) |
8 | 6, 7 | ax-mp 5 |
. . . . . . 7
β’ (πΊ:Οβ1-1-ontoββ β πΊ:Οβ1-1-ontoβ(β€β₯β1)) |
9 | 5, 8 | mpbir 230 |
. . . . . 6
β’ πΊ:Οβ1-1-ontoββ |
10 | | f1ocnv 6797 |
. . . . . 6
β’ (πΊ:Οβ1-1-ontoββ β β‘πΊ:ββ1-1-ontoβΟ) |
11 | | f1of1 6784 |
. . . . . 6
β’ (β‘πΊ:ββ1-1-ontoβΟ β β‘πΊ:ββ1-1βΟ) |
12 | 9, 10, 11 | mp2b 10 |
. . . . 5
β’ β‘πΊ:ββ1-1βΟ |
13 | | f1ores 6799 |
. . . . 5
β’ ((β‘πΊ:ββ1-1βΟ β§ π΄ β β) β (β‘πΊ βΎ π΄):π΄β1-1-ontoβ(β‘πΊ β π΄)) |
14 | 12, 13 | mpan 689 |
. . . 4
β’ (π΄ β β β (β‘πΊ βΎ π΄):π΄β1-1-ontoβ(β‘πΊ β π΄)) |
15 | | f1oeng 8914 |
. . . 4
β’ ((π΄ β V β§ (β‘πΊ βΎ π΄):π΄β1-1-ontoβ(β‘πΊ β π΄)) β π΄ β (β‘πΊ β π΄)) |
16 | 2, 14, 15 | syl2anc 585 |
. . 3
β’ (π΄ β β β π΄ β (β‘πΊ β π΄)) |
17 | 16 | adantr 482 |
. 2
β’ ((π΄ β β β§
βπ β β
βπ β π΄ π < π) β π΄ β (β‘πΊ β π΄)) |
18 | | imassrn 6025 |
. . . 4
β’ (β‘πΊ β π΄) β ran β‘πΊ |
19 | | dfdm4 5852 |
. . . . 5
β’ dom πΊ = ran β‘πΊ |
20 | | f1of 6785 |
. . . . . . 7
β’ (πΊ:Οβ1-1-ontoββ β πΊ:ΟβΆβ) |
21 | 9, 20 | ax-mp 5 |
. . . . . 6
β’ πΊ:ΟβΆβ |
22 | 21 | fdmi 6681 |
. . . . 5
β’ dom πΊ = Ο |
23 | 19, 22 | eqtr3i 2763 |
. . . 4
β’ ran β‘πΊ = Ο |
24 | 18, 23 | sseqtri 3981 |
. . 3
β’ (β‘πΊ β π΄) β Ο |
25 | 3, 4 | om2uzuzi 13860 |
. . . . . . . . . . 11
β’ (π¦ β Ο β (πΊβπ¦) β
(β€β₯β1)) |
26 | 25, 6 | eleqtrrdi 2845 |
. . . . . . . . . 10
β’ (π¦ β Ο β (πΊβπ¦) β β) |
27 | | breq1 5109 |
. . . . . . . . . . . 12
β’ (π = (πΊβπ¦) β (π < π β (πΊβπ¦) < π)) |
28 | 27 | rexbidv 3172 |
. . . . . . . . . . 11
β’ (π = (πΊβπ¦) β (βπ β π΄ π < π β βπ β π΄ (πΊβπ¦) < π)) |
29 | 28 | rspcv 3576 |
. . . . . . . . . 10
β’ ((πΊβπ¦) β β β (βπ β β βπ β π΄ π < π β βπ β π΄ (πΊβπ¦) < π)) |
30 | 26, 29 | syl 17 |
. . . . . . . . 9
β’ (π¦ β Ο β
(βπ β β
βπ β π΄ π < π β βπ β π΄ (πΊβπ¦) < π)) |
31 | 30 | adantr 482 |
. . . . . . . 8
β’ ((π¦ β Ο β§ π΄ β β) β
(βπ β β
βπ β π΄ π < π β βπ β π΄ (πΊβπ¦) < π)) |
32 | | f1ocnv 6797 |
. . . . . . . . . . . . . . . . 17
β’ ((β‘πΊ βΎ π΄):π΄β1-1-ontoβ(β‘πΊ β π΄) β β‘(β‘πΊ βΎ π΄):(β‘πΊ β π΄)β1-1-ontoβπ΄) |
33 | 14, 32 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β β‘(β‘πΊ βΎ π΄):(β‘πΊ β π΄)β1-1-ontoβπ΄) |
34 | | f1ofun 6787 |
. . . . . . . . . . . . . . . . . 18
β’ (πΊ:Οβ1-1-ontoββ β Fun πΊ) |
35 | 9, 34 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ Fun πΊ |
36 | | funcnvres2 6582 |
. . . . . . . . . . . . . . . . 17
β’ (Fun
πΊ β β‘(β‘πΊ βΎ π΄) = (πΊ βΎ (β‘πΊ β π΄))) |
37 | | f1oeq1 6773 |
. . . . . . . . . . . . . . . . 17
β’ (β‘(β‘πΊ βΎ π΄) = (πΊ βΎ (β‘πΊ β π΄)) β (β‘(β‘πΊ βΎ π΄):(β‘πΊ β π΄)β1-1-ontoβπ΄ β (πΊ βΎ (β‘πΊ β π΄)):(β‘πΊ β π΄)β1-1-ontoβπ΄)) |
38 | 35, 36, 37 | mp2b 10 |
. . . . . . . . . . . . . . . 16
β’ (β‘(β‘πΊ βΎ π΄):(β‘πΊ β π΄)β1-1-ontoβπ΄ β (πΊ βΎ (β‘πΊ β π΄)):(β‘πΊ β π΄)β1-1-ontoβπ΄) |
39 | 33, 38 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β (πΊ βΎ (β‘πΊ β π΄)):(β‘πΊ β π΄)β1-1-ontoβπ΄) |
40 | | f1ofo 6792 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊ βΎ (β‘πΊ β π΄)):(β‘πΊ β π΄)β1-1-ontoβπ΄ β (πΊ βΎ (β‘πΊ β π΄)):(β‘πΊ β π΄)βontoβπ΄) |
41 | | forn 6760 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊ βΎ (β‘πΊ β π΄)):(β‘πΊ β π΄)βontoβπ΄ β ran (πΊ βΎ (β‘πΊ β π΄)) = π΄) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((πΊ βΎ (β‘πΊ β π΄)):(β‘πΊ β π΄)β1-1-ontoβπ΄ β ran (πΊ βΎ (β‘πΊ β π΄)) = π΄) |
43 | 42 | eleq2d 2820 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ βΎ (β‘πΊ β π΄)):(β‘πΊ β π΄)β1-1-ontoβπ΄ β (π β ran (πΊ βΎ (β‘πΊ β π΄)) β π β π΄)) |
44 | | f1ofn 6786 |
. . . . . . . . . . . . . . . . 17
β’ ((πΊ βΎ (β‘πΊ β π΄)):(β‘πΊ β π΄)β1-1-ontoβπ΄ β (πΊ βΎ (β‘πΊ β π΄)) Fn (β‘πΊ β π΄)) |
45 | | fvelrnb 6904 |
. . . . . . . . . . . . . . . . 17
β’ ((πΊ βΎ (β‘πΊ β π΄)) Fn (β‘πΊ β π΄) β (π β ran (πΊ βΎ (β‘πΊ β π΄)) β βπ β (β‘πΊ β π΄)((πΊ βΎ (β‘πΊ β π΄))βπ) = π)) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ βΎ (β‘πΊ β π΄)):(β‘πΊ β π΄)β1-1-ontoβπ΄ β (π β ran (πΊ βΎ (β‘πΊ β π΄)) β βπ β (β‘πΊ β π΄)((πΊ βΎ (β‘πΊ β π΄))βπ) = π)) |
47 | 43, 46 | bitr3d 281 |
. . . . . . . . . . . . . . 15
β’ ((πΊ βΎ (β‘πΊ β π΄)):(β‘πΊ β π΄)β1-1-ontoβπ΄ β (π β π΄ β βπ β (β‘πΊ β π΄)((πΊ βΎ (β‘πΊ β π΄))βπ) = π)) |
48 | 39, 47 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β (π β π΄ β βπ β (β‘πΊ β π΄)((πΊ βΎ (β‘πΊ β π΄))βπ) = π)) |
49 | 48 | biimpa 478 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π β π΄) β βπ β (β‘πΊ β π΄)((πΊ βΎ (β‘πΊ β π΄))βπ) = π) |
50 | | fvres 6862 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (β‘πΊ β π΄) β ((πΊ βΎ (β‘πΊ β π΄))βπ) = (πΊβπ)) |
51 | 50 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (β‘πΊ β π΄) β (((πΊ βΎ (β‘πΊ β π΄))βπ) = π β (πΊβπ) = π)) |
52 | 51 | biimpa 478 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (β‘πΊ β π΄) β§ ((πΊ βΎ (β‘πΊ β π΄))βπ) = π) β (πΊβπ) = π) |
53 | 52 | adantll 713 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦ β Ο β§ π β (β‘πΊ β π΄)) β§ ((πΊ βΎ (β‘πΊ β π΄))βπ) = π) β (πΊβπ) = π) |
54 | 24 | sseli 3941 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (β‘πΊ β π΄) β π β Ο) |
55 | 3, 4 | om2uzlt2i 13862 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π¦ β Ο β§ π β Ο) β (π¦ β π β (πΊβπ¦) < (πΊβπ))) |
56 | 54, 55 | sylan2 594 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦ β Ο β§ π β (β‘πΊ β π΄)) β (π¦ β π β (πΊβπ¦) < (πΊβπ))) |
57 | | breq2 5110 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΊβπ) = π β ((πΊβπ¦) < (πΊβπ) β (πΊβπ¦) < π)) |
58 | 56, 57 | sylan9bb 511 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦ β Ο β§ π β (β‘πΊ β π΄)) β§ (πΊβπ) = π) β (π¦ β π β (πΊβπ¦) < π)) |
59 | 53, 58 | syldan 592 |
. . . . . . . . . . . . . . . . 17
β’ (((π¦ β Ο β§ π β (β‘πΊ β π΄)) β§ ((πΊ βΎ (β‘πΊ β π΄))βπ) = π) β (π¦ β π β (πΊβπ¦) < π)) |
60 | 59 | biimparc 481 |
. . . . . . . . . . . . . . . 16
β’ (((πΊβπ¦) < π β§ ((π¦ β Ο β§ π β (β‘πΊ β π΄)) β§ ((πΊ βΎ (β‘πΊ β π΄))βπ) = π)) β π¦ β π) |
61 | 60 | exp44 439 |
. . . . . . . . . . . . . . 15
β’ ((πΊβπ¦) < π β (π¦ β Ο β (π β (β‘πΊ β π΄) β (((πΊ βΎ (β‘πΊ β π΄))βπ) = π β π¦ β π)))) |
62 | 61 | imp31 419 |
. . . . . . . . . . . . . 14
β’ ((((πΊβπ¦) < π β§ π¦ β Ο) β§ π β (β‘πΊ β π΄)) β (((πΊ βΎ (β‘πΊ β π΄))βπ) = π β π¦ β π)) |
63 | 62 | reximdva 3162 |
. . . . . . . . . . . . 13
β’ (((πΊβπ¦) < π β§ π¦ β Ο) β (βπ β (β‘πΊ β π΄)((πΊ βΎ (β‘πΊ β π΄))βπ) = π β βπ β (β‘πΊ β π΄)π¦ β π)) |
64 | 49, 63 | syl5 34 |
. . . . . . . . . . . 12
β’ (((πΊβπ¦) < π β§ π¦ β Ο) β ((π΄ β β β§ π β π΄) β βπ β (β‘πΊ β π΄)π¦ β π)) |
65 | 64 | exp4b 432 |
. . . . . . . . . . 11
β’ ((πΊβπ¦) < π β (π¦ β Ο β (π΄ β β β (π β π΄ β βπ β (β‘πΊ β π΄)π¦ β π)))) |
66 | 65 | com4l 92 |
. . . . . . . . . 10
β’ (π¦ β Ο β (π΄ β β β (π β π΄ β ((πΊβπ¦) < π β βπ β (β‘πΊ β π΄)π¦ β π)))) |
67 | 66 | imp 408 |
. . . . . . . . 9
β’ ((π¦ β Ο β§ π΄ β β) β (π β π΄ β ((πΊβπ¦) < π β βπ β (β‘πΊ β π΄)π¦ β π))) |
68 | 67 | rexlimdv 3147 |
. . . . . . . 8
β’ ((π¦ β Ο β§ π΄ β β) β
(βπ β π΄ (πΊβπ¦) < π β βπ β (β‘πΊ β π΄)π¦ β π)) |
69 | 31, 68 | syld 47 |
. . . . . . 7
β’ ((π¦ β Ο β§ π΄ β β) β
(βπ β β
βπ β π΄ π < π β βπ β (β‘πΊ β π΄)π¦ β π)) |
70 | 69 | ex 414 |
. . . . . 6
β’ (π¦ β Ο β (π΄ β β β
(βπ β β
βπ β π΄ π < π β βπ β (β‘πΊ β π΄)π¦ β π))) |
71 | 70 | com3l 89 |
. . . . 5
β’ (π΄ β β β
(βπ β β
βπ β π΄ π < π β (π¦ β Ο β βπ β (β‘πΊ β π΄)π¦ β π))) |
72 | 71 | imp 408 |
. . . 4
β’ ((π΄ β β β§
βπ β β
βπ β π΄ π < π) β (π¦ β Ο β βπ β (β‘πΊ β π΄)π¦ β π)) |
73 | 72 | ralrimiv 3139 |
. . 3
β’ ((π΄ β β β§
βπ β β
βπ β π΄ π < π) β βπ¦ β Ο βπ β (β‘πΊ β π΄)π¦ β π) |
74 | | unbnn3 9600 |
. . 3
β’ (((β‘πΊ β π΄) β Ο β§ βπ¦ β Ο βπ β (β‘πΊ β π΄)π¦ β π) β (β‘πΊ β π΄) β Ο) |
75 | 24, 73, 74 | sylancr 588 |
. 2
β’ ((π΄ β β β§
βπ β β
βπ β π΄ π < π) β (β‘πΊ β π΄) β Ο) |
76 | | entr 8949 |
. 2
β’ ((π΄ β (β‘πΊ β π΄) β§ (β‘πΊ β π΄) β Ο) β π΄ β Ο) |
77 | 17, 75, 76 | syl2anc 585 |
1
β’ ((π΄ β β β§
βπ β β
βπ β π΄ π < π) β π΄ β Ο) |