Theorem nn0ennn

Description: The nonnegative integers are equinumerous to the positive integers. (Contributed by NM, 19-Jul-2004)

	Ref	Expression
Assertion	nn0ennn	$$⊢{\mathbb{N}}_0\approx \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
2		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
3		nn0p1nn	$$⊢x\in {\mathbb{N}}_0\to x+1\in \mathbb{N}$$
4		nnm1nn0	$$⊢y\in \mathbb{N}\to y-1\in {\mathbb{N}}_0$$
5		nncn	$$⊢y\in \mathbb{N}\to y\in ℂ$$
6		nn0cn	$$⊢x\in {\mathbb{N}}_0\to x\in ℂ$$
7		ax-1cn	$$⊢1\in ℂ$$
8		subadd	$$⊢\left(y\in ℂ\wedge 1\in ℂ\wedge x\in ℂ\right)\to \left(y-1=x\leftrightarrow 1+x=y\right)$$
9	7 8	mp3an2	$$⊢\left(y\in ℂ\wedge x\in ℂ\right)\to \left(y-1=x\leftrightarrow 1+x=y\right)$$
10		eqcom	$$⊢x=y-1\leftrightarrow y-1=x$$
11		eqcom	$$⊢y=1+x\leftrightarrow 1+x=y$$
12	9 10 11	3bitr4g	$$⊢\left(y\in ℂ\wedge x\in ℂ\right)\to \left(x=y-1\leftrightarrow y=1+x\right)$$
13		addcom	$$⊢\left(1\in ℂ\wedge x\in ℂ\right)\to 1+x=x+1$$
14	7 13	mpan	$$⊢x\in ℂ\to 1+x=x+1$$
15	14	eqeq2d	$$⊢x\in ℂ\to \left(y=1+x\leftrightarrow y=x+1\right)$$
16	15	adantl	$$⊢\left(y\in ℂ\wedge x\in ℂ\right)\to \left(y=1+x\leftrightarrow y=x+1\right)$$
17	12 16	bitrd	$$⊢\left(y\in ℂ\wedge x\in ℂ\right)\to \left(x=y-1\leftrightarrow y=x+1\right)$$
18	5 6 17	syl2anr	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in \mathbb{N}\right)\to \left(x=y-1\leftrightarrow y=x+1\right)$$
19	1 2 3 4 18	en3i	$$⊢{\mathbb{N}}_0\approx \mathbb{N}$$