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	$$⊢\mathbb{N}\approx \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
2		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
3		eqid	$$⊢{\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}={\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}$$
4	3	hashgf1o	$$⊢\left({\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
5		f1oen2g	$$⊢\left(\mathrm{\omega }\in \mathrm{V}\wedge {\mathbb{N}}_0\in \mathrm{V}\wedge \left({\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\right)\to \mathrm{\omega }\approx {\mathbb{N}}_0$$
6	1 2 4 5	mp3an	$$⊢\mathrm{\omega }\approx {\mathbb{N}}_0$$
7		nn0ennn	$$⊢{\mathbb{N}}_0\approx \mathbb{N}$$
8	6 7	entr2i	$$⊢\mathbb{N}\approx \mathrm{\omega }$$