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 |
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 |