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	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
Assertion	hashgf1o	⊢ 𝐺 : ω –1-1-onto→ ℕ0

Proof

Step	Hyp	Ref	Expression
1		fzennn.1	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
2		0z	⊢ 0 ∈ ℤ
3	2 1	om2uzf1oi	⊢ 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 0 )
4		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
5		f1oeq3	⊢ ( ℕ0 = ( ℤ≥ ‘ 0 ) → ( 𝐺 : ω –1-1-onto→ ℕ0 ↔ 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 0 ) ) )
6	4 5	ax-mp	⊢ ( 𝐺 : ω –1-1-onto→ ℕ0 ↔ 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 0 ) )
7	3 6	mpbir	⊢ 𝐺 : ω –1-1-onto→ ℕ0