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 = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
Assertion	hashgf1o	|- G : _om -1-1-onto-> NN0

Proof

Step	Hyp	Ref	Expression
1		fzennn.1	|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
2		0z	|- 0 e. ZZ
3	2 1	om2uzf1oi	|- G : _om -1-1-onto-> ( ZZ>= ` 0 )
4		nn0uz	|- NN0 = ( ZZ>= ` 0 )
5		f1oeq3	|- ( NN0 = ( ZZ>= ` 0 ) -> ( G : _om -1-1-onto-> NN0 <-> G : _om -1-1-onto-> ( ZZ>= ` 0 ) ) )
6	4 5	ax-mp	|- ( G : _om -1-1-onto-> NN0 <-> G : _om -1-1-onto-> ( ZZ>= ` 0 ) )
7	3 6	mpbir	|- G : _om -1-1-onto-> NN0