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

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 ( ( 𝐴 ∈ ℕ ∧ 𝐴 ≠ 1 ) → ∃ 𝑥 ∈ ℕ ( 𝑥 + 1 ) = 𝐴 )

Proof

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