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