Theorem nnenom

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	⊢ ℕ ≈ ω

Proof

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	⊢ ℕ ≈ ω