Step |
Hyp |
Ref |
Expression |
1 |
|
hashgval.1 |
|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) |
2 |
|
ficardom |
|- ( A e. Fin -> ( card ` A ) e. _om ) |
3 |
1
|
hashgval |
|- ( A e. Fin -> ( G ` ( card ` A ) ) = ( # ` A ) ) |
4 |
1
|
hashgf1o |
|- G : _om -1-1-onto-> NN0 |
5 |
|
f1ocnvfv |
|- ( ( G : _om -1-1-onto-> NN0 /\ ( card ` A ) e. _om ) -> ( ( G ` ( card ` A ) ) = ( # ` A ) -> ( `' G ` ( # ` A ) ) = ( card ` A ) ) ) |
6 |
4 5
|
mpan |
|- ( ( card ` A ) e. _om -> ( ( G ` ( card ` A ) ) = ( # ` A ) -> ( `' G ` ( # ` A ) ) = ( card ` A ) ) ) |
7 |
2 3 6
|
sylc |
|- ( A e. Fin -> ( `' G ` ( # ` A ) ) = ( card ` A ) ) |