Step | Hyp | Ref
| Expression |
1 | | frfnom 8382 |
. . . . . . 7
β’
(rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) Fn Ο |
2 | | hashgval.1 |
. . . . . . . 8
β’ πΊ = (rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) |
3 | 2 | fneq1i 6600 |
. . . . . . 7
β’ (πΊ Fn Ο β (rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) Fn
Ο) |
4 | 1, 3 | mpbir 230 |
. . . . . 6
β’ πΊ Fn Ο |
5 | | fnfun 6603 |
. . . . . 6
β’ (πΊ Fn Ο β Fun πΊ) |
6 | 4, 5 | ax-mp 5 |
. . . . 5
β’ Fun πΊ |
7 | | cardf2 9880 |
. . . . . 6
β’
card:{π¦ β£
βπ₯ β On π₯ β π¦}βΆOn |
8 | | ffun 6672 |
. . . . . 6
β’
(card:{π¦ β£
βπ₯ β On π₯ β π¦}βΆOn β Fun card) |
9 | 7, 8 | ax-mp 5 |
. . . . 5
β’ Fun
card |
10 | | funco 6542 |
. . . . 5
β’ ((Fun
πΊ β§ Fun card) β
Fun (πΊ β
card)) |
11 | 6, 9, 10 | mp2an 691 |
. . . 4
β’ Fun
(πΊ β
card) |
12 | | dmco 6207 |
. . . . 5
β’ dom
(πΊ β card) = (β‘card β dom πΊ) |
13 | 4 | fndmi 6607 |
. . . . . 6
β’ dom πΊ = Ο |
14 | 13 | imaeq2i 6012 |
. . . . 5
β’ (β‘card β dom πΊ) = (β‘card β Ο) |
15 | | funfn 6532 |
. . . . . . . . 9
β’ (Fun card
β card Fn dom card) |
16 | 9, 15 | mpbi 229 |
. . . . . . . 8
β’ card Fn
dom card |
17 | | elpreima 7009 |
. . . . . . . 8
β’ (card Fn
dom card β (π¦ β
(β‘card β Ο) β (π¦ β dom card β§
(cardβπ¦) β
Ο))) |
18 | 16, 17 | ax-mp 5 |
. . . . . . 7
β’ (π¦ β (β‘card β Ο) β (π¦ β dom card β§
(cardβπ¦) β
Ο)) |
19 | | id 22 |
. . . . . . . . . 10
β’
((cardβπ¦)
β Ο β (cardβπ¦) β Ο) |
20 | | cardid2 9890 |
. . . . . . . . . . 11
β’ (π¦ β dom card β
(cardβπ¦) β
π¦) |
21 | 20 | ensymd 8946 |
. . . . . . . . . 10
β’ (π¦ β dom card β π¦ β (cardβπ¦)) |
22 | | breq2 5110 |
. . . . . . . . . . 11
β’ (π₯ = (cardβπ¦) β (π¦ β π₯ β π¦ β (cardβπ¦))) |
23 | 22 | rspcev 3582 |
. . . . . . . . . 10
β’
(((cardβπ¦)
β Ο β§ π¦
β (cardβπ¦))
β βπ₯ β
Ο π¦ β π₯) |
24 | 19, 21, 23 | syl2anr 598 |
. . . . . . . . 9
β’ ((π¦ β dom card β§
(cardβπ¦) β
Ο) β βπ₯
β Ο π¦ β
π₯) |
25 | | isfi 8917 |
. . . . . . . . 9
β’ (π¦ β Fin β βπ₯ β Ο π¦ β π₯) |
26 | 24, 25 | sylibr 233 |
. . . . . . . 8
β’ ((π¦ β dom card β§
(cardβπ¦) β
Ο) β π¦ β
Fin) |
27 | | finnum 9885 |
. . . . . . . . 9
β’ (π¦ β Fin β π¦ β dom
card) |
28 | | ficardom 9898 |
. . . . . . . . 9
β’ (π¦ β Fin β
(cardβπ¦) β
Ο) |
29 | 27, 28 | jca 513 |
. . . . . . . 8
β’ (π¦ β Fin β (π¦ β dom card β§
(cardβπ¦) β
Ο)) |
30 | 26, 29 | impbii 208 |
. . . . . . 7
β’ ((π¦ β dom card β§
(cardβπ¦) β
Ο) β π¦ β
Fin) |
31 | 18, 30 | bitri 275 |
. . . . . 6
β’ (π¦ β (β‘card β Ο) β π¦ β Fin) |
32 | 31 | eqriv 2734 |
. . . . 5
β’ (β‘card β Ο) = Fin |
33 | 12, 14, 32 | 3eqtri 2769 |
. . . 4
β’ dom
(πΊ β card) =
Fin |
34 | | df-fn 6500 |
. . . 4
β’ ((πΊ β card) Fn Fin β
(Fun (πΊ β card) β§
dom (πΊ β card) =
Fin)) |
35 | 11, 33, 34 | mpbir2an 710 |
. . 3
β’ (πΊ β card) Fn
Fin |
36 | | hashkf.2 |
. . . 4
β’ πΎ = (πΊ β card) |
37 | 36 | fneq1i 6600 |
. . 3
β’ (πΎ Fn Fin β (πΊ β card) Fn
Fin) |
38 | 35, 37 | mpbir 230 |
. 2
β’ πΎ Fn Fin |
39 | 36 | fveq1i 6844 |
. . . . 5
β’ (πΎβπ¦) = ((πΊ β card)βπ¦) |
40 | | fvco 6940 |
. . . . . 6
β’ ((Fun
card β§ π¦ β dom
card) β ((πΊ β
card)βπ¦) = (πΊβ(cardβπ¦))) |
41 | 9, 27, 40 | sylancr 588 |
. . . . 5
β’ (π¦ β Fin β ((πΊ β card)βπ¦) = (πΊβ(cardβπ¦))) |
42 | 39, 41 | eqtrid 2789 |
. . . 4
β’ (π¦ β Fin β (πΎβπ¦) = (πΊβ(cardβπ¦))) |
43 | 2 | hashgf1o 13877 |
. . . . . . 7
β’ πΊ:Οβ1-1-ontoββ0 |
44 | | f1of 6785 |
. . . . . . 7
β’ (πΊ:Οβ1-1-ontoββ0 β πΊ:ΟβΆβ0) |
45 | 43, 44 | ax-mp 5 |
. . . . . 6
β’ πΊ:ΟβΆβ0 |
46 | 45 | ffvelcdmi 7035 |
. . . . 5
β’
((cardβπ¦)
β Ο β (πΊβ(cardβπ¦)) β
β0) |
47 | 28, 46 | syl 17 |
. . . 4
β’ (π¦ β Fin β (πΊβ(cardβπ¦)) β
β0) |
48 | 42, 47 | eqeltrd 2838 |
. . 3
β’ (π¦ β Fin β (πΎβπ¦) β
β0) |
49 | 48 | rgen 3067 |
. 2
β’
βπ¦ β Fin
(πΎβπ¦) β β0 |
50 | | ffnfv 7067 |
. 2
β’ (πΎ:FinβΆβ0
β (πΎ Fn Fin β§
βπ¦ β Fin (πΎβπ¦) β
β0)) |
51 | 38, 49, 50 | mpbir2an 710 |
1
β’ πΎ:FinβΆβ0 |