Description: The set of positive integers (as a subset of complex numbers) is equinumerous to omega (the set of finite ordinal numbers). (Contributed by NM, 31-Jul-2004) (Revised by Mario Carneiro, 15-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | nnenom | ⊢ ℕ ≈ ω |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | omex | ⊢ ω ∈ V | |
2 | nn0ex | ⊢ ℕ_{0} ∈ V | |
3 | eqid | ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) | |
4 | 3 | hashgf1o | ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) : ω –1-1-onto→ ℕ_{0} |
5 | f1oen2g | ⊢ ( ( ω ∈ V ∧ ℕ_{0} ∈ V ∧ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) : ω –1-1-onto→ ℕ_{0} ) → ω ≈ ℕ_{0} ) | |
6 | 1 2 4 5 | mp3an | ⊢ ω ≈ ℕ_{0} |
7 | nn0ennn | ⊢ ℕ_{0} ≈ ℕ | |
8 | 6 7 | entr2i | ⊢ ℕ ≈ ω |