Theorem hashginv

Description: ` ``' 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={\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}$$
Assertion	hashginv	$$⊢A\in \mathrm{Fin}\to G^{-1}\left(\left|A\right|\right)=\mathrm{card}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		hashgval.1	$$⊢G={\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}$$
2		ficardom	$$⊢A\in \mathrm{Fin}\to \mathrm{card}\left(A\right)\in \mathrm{\omega }$$
3	1	hashgval	$$⊢A\in \mathrm{Fin}\to G\left(\mathrm{card}\left(A\right)\right)=\left|A\right|$$
4	1	hashgf1o	$$⊢G:\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
5		f1ocnvfv	$$⊢\left(G:\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\wedge \mathrm{card}\left(A\right)\in \mathrm{\omega }\right)\to \left(G\left(\mathrm{card}\left(A\right)\right)=\left|A\right|\to G^{-1}\left(\left|A\right|\right)=\mathrm{card}\left(A\right)\right)$$
6	4 5	mpan	$$⊢\mathrm{card}\left(A\right)\in \mathrm{\omega }\to \left(G\left(\mathrm{card}\left(A\right)\right)=\left|A\right|\to G^{-1}\left(\left|A\right|\right)=\mathrm{card}\left(A\right)\right)$$
7	2 3 6	sylc	$$⊢A\in \mathrm{Fin}\to G^{-1}\left(\left|A\right|\right)=\mathrm{card}\left(A\right)$$