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