Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . 3
β’
(rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) = (rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο) |
2 | 1 | hashgval 14240 |
. 2
β’ (π΄ β Fin β ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ΄)) = (β―βπ΄)) |
3 | | ficardom 9904 |
. . 3
β’ (π΄ β Fin β
(cardβπ΄) β
Ο) |
4 | 1 | hashgf1o 13883 |
. . . . 5
β’
(rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο):Οβ1-1-ontoββ0 |
5 | | f1of 6789 |
. . . . 5
β’
((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο):Οβ1-1-ontoββ0 β (rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο):ΟβΆβ0) |
6 | 4, 5 | ax-mp 5 |
. . . 4
β’
(rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο):ΟβΆβ0 |
7 | 6 | ffvelcdmi 7039 |
. . 3
β’
((cardβπ΄)
β Ο β ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ΄)) β
β0) |
8 | 3, 7 | syl 17 |
. 2
β’ (π΄ β Fin β ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ
Ο)β(cardβπ΄)) β
β0) |
9 | 2, 8 | eqeltrrd 2839 |
1
β’ (π΄ β Fin β
(β―βπ΄) β
β0) |