Metamath Proof Explorer


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