Theorem nn0ennn

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

	Ref	Expression
Assertion	nn0ennn	⊢ ℕ0 ≈ ℕ

Proof

Step	Hyp	Ref	Expression
1		nn0ex	⊢ ℕ0 ∈ V
2		nnex	⊢ ℕ ∈ V
3		nn0p1nn	⊢ ( 𝑥 ∈ ℕ0 → ( 𝑥 + 1 ) ∈ ℕ )
4		nnm1nn0	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 − 1 ) ∈ ℕ0 )
5		nncn	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
6		nn0cn	⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℂ )
7		ax-1cn	⊢ 1 ∈ ℂ
8		subadd	⊢ ( ( 𝑦 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑦 − 1 ) = 𝑥 ↔ ( 1 + 𝑥 ) = 𝑦 ) )
9	7 8	mp3an2	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑦 − 1 ) = 𝑥 ↔ ( 1 + 𝑥 ) = 𝑦 ) )
10		eqcom	⊢ ( 𝑥 = ( 𝑦 − 1 ) ↔ ( 𝑦 − 1 ) = 𝑥 )
11		eqcom	⊢ ( 𝑦 = ( 1 + 𝑥 ) ↔ ( 1 + 𝑥 ) = 𝑦 )
12	9 10 11	3bitr4g	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 = ( 𝑦 − 1 ) ↔ 𝑦 = ( 1 + 𝑥 ) ) )
13		addcom	⊢ ( ( 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 1 + 𝑥 ) = ( 𝑥 + 1 ) )
14	7 13	mpan	⊢ ( 𝑥 ∈ ℂ → ( 1 + 𝑥 ) = ( 𝑥 + 1 ) )
15	14	eqeq2d	⊢ ( 𝑥 ∈ ℂ → ( 𝑦 = ( 1 + 𝑥 ) ↔ 𝑦 = ( 𝑥 + 1 ) ) )
16	15	adantl	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑦 = ( 1 + 𝑥 ) ↔ 𝑦 = ( 𝑥 + 1 ) ) )
17	12 16	bitrd	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 = ( 𝑦 − 1 ) ↔ 𝑦 = ( 𝑥 + 1 ) ) )
18	5 6 17	syl2anr	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ ) → ( 𝑥 = ( 𝑦 − 1 ) ↔ 𝑦 = ( 𝑥 + 1 ) ) )
19	1 2 3 4 18	en3i	⊢ ℕ0 ≈ ℕ