Step | Hyp | Ref
| Expression |
1 | | pm3.24 406 |
. . . 4
⊢ ¬
(∀𝑦 ∈ ℕ
¬ 𝑥 < 𝑦 ∧ ¬ ∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦) |
2 | | peano2rem 11170 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈
ℝ) |
3 | | ltm1 11699 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → (𝑥 − 1) < 𝑥) |
4 | | ovex 7265 |
. . . . . . . . . . . . 13
⊢ (𝑥 − 1) ∈
V |
5 | | eleq1 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 − 1) → (𝑦 ∈ ℝ ↔ (𝑥 − 1) ∈ ℝ)) |
6 | | breq1 5071 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 − 1) → (𝑦 < 𝑥 ↔ (𝑥 − 1) < 𝑥)) |
7 | | breq1 5071 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑥 − 1) → (𝑦 < 𝑧 ↔ (𝑥 − 1) < 𝑧)) |
8 | 7 | rexbidv 3224 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 − 1) → (∃𝑧 ∈ ℕ 𝑦 < 𝑧 ↔ ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧)) |
9 | 6, 8 | imbi12d 348 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 − 1) → ((𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧) ↔ ((𝑥 − 1) < 𝑥 → ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧))) |
10 | 5, 9 | imbi12d 348 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 − 1) → ((𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) ↔ ((𝑥 − 1) ∈ ℝ → ((𝑥 − 1) < 𝑥 → ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧)))) |
11 | 4, 10 | spcv 3533 |
. . . . . . . . . . . 12
⊢
(∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → ((𝑥 − 1) ∈ ℝ → ((𝑥 − 1) < 𝑥 → ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧))) |
12 | 3, 11 | syl7 74 |
. . . . . . . . . . 11
⊢
(∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → ((𝑥 − 1) ∈ ℝ → (𝑥 ∈ ℝ →
∃𝑧 ∈ ℕ
(𝑥 − 1) < 𝑧))) |
13 | 2, 12 | syl5 34 |
. . . . . . . . . 10
⊢
(∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → (𝑥 ∈ ℝ → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧))) |
14 | 13 | pm2.43d 53 |
. . . . . . . . 9
⊢
(∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧)) |
15 | | df-rex 3068 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
ℕ (𝑥 − 1) <
𝑧 ↔ ∃𝑧(𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧)) |
16 | 14, 15 | syl6ib 254 |
. . . . . . . 8
⊢
(∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → (𝑥 ∈ ℝ → ∃𝑧(𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧))) |
17 | 16 | com12 32 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ →
(∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → ∃𝑧(𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧))) |
18 | | nnre 11862 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℝ) |
19 | | 1re 10858 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
20 | | ltsubadd 11327 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝑧 ∈
ℝ) → ((𝑥 −
1) < 𝑧 ↔ 𝑥 < (𝑧 + 1))) |
21 | 19, 20 | mp3an2 1451 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 − 1) < 𝑧 ↔ 𝑥 < (𝑧 + 1))) |
22 | 18, 21 | sylan2 596 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℕ) → ((𝑥 − 1) < 𝑧 ↔ 𝑥 < (𝑧 + 1))) |
23 | 22 | pm5.32da 582 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → ((𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧) ↔ (𝑧 ∈ ℕ ∧ 𝑥 < (𝑧 + 1)))) |
24 | 23 | exbidv 1929 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ →
(∃𝑧(𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧) ↔ ∃𝑧(𝑧 ∈ ℕ ∧ 𝑥 < (𝑧 + 1)))) |
25 | | peano2nn 11867 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℕ → (𝑧 + 1) ∈
ℕ) |
26 | | ovex 7265 |
. . . . . . . . . . 11
⊢ (𝑧 + 1) ∈ V |
27 | | eleq1 2826 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑧 + 1) → (𝑦 ∈ ℕ ↔ (𝑧 + 1) ∈ ℕ)) |
28 | | breq2 5072 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑧 + 1) → (𝑥 < 𝑦 ↔ 𝑥 < (𝑧 + 1))) |
29 | 27, 28 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑧 + 1) → ((𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) ↔ ((𝑧 + 1) ∈ ℕ ∧ 𝑥 < (𝑧 + 1)))) |
30 | 26, 29 | spcev 3534 |
. . . . . . . . . 10
⊢ (((𝑧 + 1) ∈ ℕ ∧ 𝑥 < (𝑧 + 1)) → ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦)) |
31 | 25, 30 | sylan 583 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℕ ∧ 𝑥 < (𝑧 + 1)) → ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦)) |
32 | 31 | exlimiv 1938 |
. . . . . . . 8
⊢
(∃𝑧(𝑧 ∈ ℕ ∧ 𝑥 < (𝑧 + 1)) → ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦)) |
33 | 24, 32 | syl6bi 256 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ →
(∃𝑧(𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧) → ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦))) |
34 | 17, 33 | syld 47 |
. . . . . 6
⊢ (𝑥 ∈ ℝ →
(∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦))) |
35 | | df-ral 3067 |
. . . . . 6
⊢
(∀𝑦 ∈
ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧) ↔ ∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧))) |
36 | | df-ral 3067 |
. . . . . . . 8
⊢
(∀𝑦 ∈
ℕ ¬ 𝑥 < 𝑦 ↔ ∀𝑦(𝑦 ∈ ℕ → ¬ 𝑥 < 𝑦)) |
37 | | alinexa 1850 |
. . . . . . . 8
⊢
(∀𝑦(𝑦 ∈ ℕ → ¬
𝑥 < 𝑦) ↔ ¬ ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦)) |
38 | 36, 37 | bitr2i 279 |
. . . . . . 7
⊢ (¬
∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) ↔ ∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦) |
39 | 38 | con1bii 360 |
. . . . . 6
⊢ (¬
∀𝑦 ∈ ℕ
¬ 𝑥 < 𝑦 ↔ ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦)) |
40 | 34, 35, 39 | 3imtr4g 299 |
. . . . 5
⊢ (𝑥 ∈ ℝ →
(∀𝑦 ∈ ℝ
(𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧) → ¬ ∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦)) |
41 | 40 | anim2d 615 |
. . . 4
⊢ (𝑥 ∈ ℝ →
((∀𝑦 ∈ ℕ
¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → (∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦 ∧ ¬ ∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦))) |
42 | 1, 41 | mtoi 202 |
. . 3
⊢ (𝑥 ∈ ℝ → ¬
(∀𝑦 ∈ ℕ
¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧))) |
43 | 42 | nrex 3195 |
. 2
⊢ ¬
∃𝑥 ∈ ℝ
(∀𝑦 ∈ ℕ
¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) |
44 | | nnssre 11859 |
. . 3
⊢ ℕ
⊆ ℝ |
45 | | 1nn 11866 |
. . . 4
⊢ 1 ∈
ℕ |
46 | 45 | ne0ii 4267 |
. . 3
⊢ ℕ
≠ ∅ |
47 | | sup2 11813 |
. . 3
⊢ ((ℕ
⊆ ℝ ∧ ℕ ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℕ (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧))) |
48 | 44, 46, 47 | mp3an12 1453 |
. 2
⊢
(∃𝑥 ∈
ℝ ∀𝑦 ∈
ℕ (𝑦 < 𝑥 ∨ 𝑦 = 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧))) |
49 | 43, 48 | mto 200 |
1
⊢ ¬
∃𝑥 ∈ ℝ
∀𝑦 ∈ ℕ
(𝑦 < 𝑥 ∨ 𝑦 = 𝑥) |