Theorem hashgf1o

Description: G maps _om one-to-one onto NN0 . (Contributed by Paul Chapman, 22-Jun-2011) (Revised by Mario Carneiro, 13-Sep-2013)

	Ref	Expression
Hypothesis	fzennn.1	$$⊢G={\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}$$
Assertion	hashgf1o	$$⊢G:\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		fzennn.1	$$⊢G={\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}$$
2		0z	$$⊢0\in \mathbb{Z}$$
3	2 1	om2uzf1oi	$$⊢G:\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{Z}}_{\ge 0}$$
4		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
5		f1oeq3	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}\to \left(G:\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\leftrightarrow G:\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{Z}}_{\ge 0}\right)$$
6	4 5	ax-mp	$$⊢G:\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\leftrightarrow G:\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{Z}}_{\ge 0}$$
7	3 6	mpbir	$$⊢G:\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$