Metamath Proof Explorer

Theorem nnn1suc

Description: A positive integer that is not 1 is a successor of some other positive integer. (Contributed by Steven Nguyen, 19-Aug-2023)

Ref Expression
Assertion nnn1suc ⊢ A ∈ ℕ ∧ A ≠ 1 → ∃ x ∈ ℕ x + 1 = A

Proof

Step Hyp Ref Expression
1 neeq1 ⊢ y = 1 → y ≠ 1 ↔ 1 ≠ 1
2 eqeq2 ⊢ y = 1 → x + 1 = y ↔ x + 1 = 1
3 2 rexbidv ⊢ y = 1 → ∃ x ∈ ℕ x + 1 = y ↔ ∃ x ∈ ℕ x + 1 = 1
4 1 3 imbi12d ⊢ y = 1 → y ≠ 1 → ∃ x ∈ ℕ x + 1 = y ↔ 1 ≠ 1 → ∃ x ∈ ℕ x + 1 = 1
5 neeq1 ⊢ y = z → y ≠ 1 ↔ z ≠ 1
6 eqeq2 ⊢ y = z → x + 1 = y ↔ x + 1 = z
7 6 rexbidv ⊢ y = z → ∃ x ∈ ℕ x + 1 = y ↔ ∃ x ∈ ℕ x + 1 = z
8 5 7 imbi12d ⊢ y = z → y ≠ 1 → ∃ x ∈ ℕ x + 1 = y ↔ z ≠ 1 → ∃ x ∈ ℕ x + 1 = z
9 neeq1 ⊢ y = z + 1 → y ≠ 1 ↔ z + 1 ≠ 1
10 eqeq2 ⊢ y = z + 1 → x + 1 = y ↔ x + 1 = z + 1
11 10 rexbidv ⊢ y = z + 1 → ∃ x ∈ ℕ x + 1 = y ↔ ∃ x ∈ ℕ x + 1 = z + 1
12 9 11 imbi12d ⊢ y = z + 1 → y ≠ 1 → ∃ x ∈ ℕ x + 1 = y ↔ z + 1 ≠ 1 → ∃ x ∈ ℕ x + 1 = z + 1
13 neeq1 ⊢ y = A → y ≠ 1 ↔ A ≠ 1
14 eqeq2 ⊢ y = A → x + 1 = y ↔ x + 1 = A
15 14 rexbidv ⊢ y = A → ∃ x ∈ ℕ x + 1 = y ↔ ∃ x ∈ ℕ x + 1 = A
16 13 15 imbi12d ⊢ y = A → y ≠ 1 → ∃ x ∈ ℕ x + 1 = y ↔ A ≠ 1 → ∃ x ∈ ℕ x + 1 = A
17 df-ne ⊢ 1 ≠ 1 ↔ ¬ 1 = 1
18 eqid ⊢ 1 = 1
19 18 pm2.24i ⊢ ¬ 1 = 1 → ∃ x ∈ ℕ x + 1 = 1
20 17 19 sylbi ⊢ 1 ≠ 1 → ∃ x ∈ ℕ x + 1 = 1
21 id ⊢ z ∈ ℕ → z ∈ ℕ
22 oveq1 ⊢ x = z → x + 1 = z + 1
23 22 adantl ⊢ z ∈ ℕ ∧ x = z → x + 1 = z + 1
24 21 23 rspcedeq1vd ⊢ z ∈ ℕ → ∃ x ∈ ℕ x + 1 = z + 1
25 24 2a1d ⊢ z ∈ ℕ → z ≠ 1 → ∃ x ∈ ℕ x + 1 = z → z + 1 ≠ 1 → ∃ x ∈ ℕ x + 1 = z + 1
26 4 8 12 16 20 25 nnind ⊢ A ∈ ℕ → A ≠ 1 → ∃ x ∈ ℕ x + 1 = A
27 26 imp ⊢ A ∈ ℕ ∧ A ≠ 1 → ∃ x ∈ ℕ x + 1 = A