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	$⊢ ℕ \approx ω$

Proof

Step	Hyp	Ref	Expression
1		omex	$⊢ ω \in V$
2		nn0ex	$⊢ ℕ_{0} \in V$
3		eqid	$⊢ {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω} = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
4	3	hashgf1o	$⊢ ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ℕ_{0}$
5		f1oen2g	$⊢ (ω \in V \land ℕ_{0} \in V \land ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) : ω \underset{1-1 onto}{⟶} ℕ_{0}) \to ω \approx ℕ_{0}$
6	1 2 4 5	mp3an	$⊢ ω \approx ℕ_{0}$
7		nn0ennn	$⊢ ℕ_{0} \approx ℕ$
8	6 7	entr2i	$⊢ ℕ \approx ω$

Metamath Proof Explorer

Theorem nnenom

Proof