Metamath Proof Explorer


Theorem hashginv

Description: The converse of G maps the size function's value to card . (Contributed by Paul Chapman, 22-Jun-2011) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Hypothesis hashgval.1 G = rec x V x + 1 0 ω
Assertion hashginv A Fin G -1 A = card A

Proof

Step Hyp Ref Expression
1 hashgval.1 G = rec x V x + 1 0 ω
2 ficardom A Fin card A ω
3 1 hashgval A Fin G card A = A
4 1 hashgf1o G : ω 1-1 onto 0
5 f1ocnvfv G : ω 1-1 onto 0 card A ω G card A = A G -1 A = card A
6 4 5 mpan card A ω G card A = A G -1 A = card A
7 2 3 6 sylc A Fin G -1 A = card A