This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ x ∈ ℕ 0 → x + 1 ∈ ℕ
4 nnm1nn0 ⊢ y ∈ ℕ → y − 1 ∈ ℕ 0
5 nncn ⊢ y ∈ ℕ → y ∈ ℂ
6 nn0cn ⊢ x ∈ ℕ 0 → x ∈ ℂ
7 ax-1cn ⊢ 1 ∈ ℂ
8 subadd ⊢ y ∈ ℂ ∧ 1 ∈ ℂ ∧ x ∈ ℂ → y − 1 = x ↔ 1 + x = y
9 7 8 mp3an2 ⊢ y ∈ ℂ ∧ x ∈ ℂ → y − 1 = x ↔ 1 + x = y
10 eqcom ⊢ x = y − 1 ↔ y − 1 = x
11 eqcom ⊢ y = 1 + x ↔ 1 + x = y
12 9 10 11 3bitr4g ⊢ y ∈ ℂ ∧ x ∈ ℂ → x = y − 1 ↔ y = 1 + x
13 addcom ⊢ 1 ∈ ℂ ∧ x ∈ ℂ → 1 + x = x + 1
14 7 13 mpan ⊢ x ∈ ℂ → 1 + x = x + 1
15 14 eqeq2d ⊢ x ∈ ℂ → y = 1 + x ↔ y = x + 1
16 15 adantl ⊢ y ∈ ℂ ∧ x ∈ ℂ → y = 1 + x ↔ y = x + 1
17 12 16 bitrd ⊢ y ∈ ℂ ∧ x ∈ ℂ → x = y − 1 ↔ y = x + 1
18 5 6 17 syl2anr ⊢ x ∈ ℕ 0 ∧ y ∈ ℕ → x = y − 1 ↔ y = x + 1
19 1 2 3 4 18 en3i ⊢ ℕ 0 ≈ ℕ