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 eqeq1d ⊢x=z→x+1=z+1↔z+1=z+1
24 23 adantl ⊢z∈ℕ∧x=z→x+1=z+1↔z+1=z+1
25 eqidd ⊢z∈ℕ→z+1=z+1
26 21 24 25 rspcedvd ⊢z∈ℕ→∃x∈ℕx+1=z+1
27 26 2a1d ⊢z∈ℕ→z≠1→∃x∈ℕx+1=z→z+1≠1→∃x∈ℕx+1=z+1
28 4 8 12 16 20 27 nnind ⊢A∈ℕ→A≠1→∃x∈ℕx+1=A
29 28 imp ⊢A∈ℕ∧A≠1→∃x∈ℕx+1=A