| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. . 3
⊢
Ⅎ𝑥 𝐴 ⊆
ℝ |
| 2 | | nfre1 3285 |
. . 3
⊢
Ⅎ𝑥∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 |
| 3 | | btwnz 12721 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ →
(∃𝑧 ∈ ℤ
𝑧 < 𝑥 ∧ ∃𝑧 ∈ ℤ 𝑥 < 𝑧)) |
| 4 | 3 | simpld 494 |
. . . . . 6
⊢ (𝑥 ∈ ℝ →
∃𝑧 ∈ ℤ
𝑧 < 𝑥) |
| 5 | | ssel2 3978 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ) |
| 6 | | zre 12617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℝ) |
| 7 | | ltleletr 11354 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑧 < 𝑥 ∧ 𝑥 ≤ 𝑦) → 𝑧 ≤ 𝑦)) |
| 8 | 6, 7 | syl3an1 1164 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑧 < 𝑥 ∧ 𝑥 ≤ 𝑦) → 𝑧 ≤ 𝑦)) |
| 9 | 8 | expd 415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧 < 𝑥 → (𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦))) |
| 10 | 9 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) → (𝑦 ∈ ℝ → (𝑧 < 𝑥 → (𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦)))) |
| 11 | 5, 10 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) → ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → (𝑧 < 𝑥 → (𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦)))) |
| 12 | 11 | expdimp 452 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) ∧ 𝐴 ⊆ ℝ) → (𝑦 ∈ 𝐴 → (𝑧 < 𝑥 → (𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦)))) |
| 13 | 12 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) ∧ 𝐴 ⊆ ℝ) → (𝑧 < 𝑥 → (𝑦 ∈ 𝐴 → (𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦)))) |
| 14 | 13 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) ∧ 𝐴 ⊆ ℝ) ∧ 𝑧 < 𝑥) → (𝑦 ∈ 𝐴 → (𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦))) |
| 15 | 14 | ralrimiv 3145 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) ∧ 𝐴 ⊆ ℝ) ∧ 𝑧 < 𝑥) → ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦)) |
| 16 | | ralim 3086 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑦 ∈
𝐴 (𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦) → (∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → ∀𝑦 ∈ 𝐴 𝑧 ≤ 𝑦)) |
| 17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) ∧ 𝐴 ⊆ ℝ) ∧ 𝑧 < 𝑥) → (∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → ∀𝑦 ∈ 𝐴 𝑧 ≤ 𝑦)) |
| 18 | 17 | ex 412 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℝ) ∧ 𝐴 ⊆ ℝ) → (𝑧 < 𝑥 → (∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → ∀𝑦 ∈ 𝐴 𝑧 ≤ 𝑦))) |
| 19 | 18 | anasss 466 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℤ ∧ (𝑥 ∈ ℝ ∧ 𝐴 ⊆ ℝ)) → (𝑧 < 𝑥 → (∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → ∀𝑦 ∈ 𝐴 𝑧 ≤ 𝑦))) |
| 20 | 19 | expcom 413 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑧 ∈ ℤ → (𝑧 < 𝑥 → (∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → ∀𝑦 ∈ 𝐴 𝑧 ≤ 𝑦)))) |
| 21 | 20 | com23 86 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑧 < 𝑥 → (𝑧 ∈ ℤ → (∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → ∀𝑦 ∈ 𝐴 𝑧 ≤ 𝑦)))) |
| 22 | 21 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑧 < 𝑥) → (𝑧 ∈ ℤ → (∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → ∀𝑦 ∈ 𝐴 𝑧 ≤ 𝑦))) |
| 23 | 22 | imdistand 570 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑧 < 𝑥) → ((𝑧 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (𝑧 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑧 ≤ 𝑦))) |
| 24 | | breq1 5146 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (𝑥 ≤ 𝑦 ↔ 𝑧 ≤ 𝑦)) |
| 25 | 24 | ralbidv 3178 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∀𝑦 ∈ 𝐴 𝑧 ≤ 𝑦)) |
| 26 | 25 | rspcev 3622 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℤ ∧
∀𝑦 ∈ 𝐴 𝑧 ≤ 𝑦) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) |
| 27 | 23, 26 | syl6 35 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ ∧ 𝐴 ⊆ ℝ) ∧ 𝑧 < 𝑥) → ((𝑧 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |
| 28 | 27 | ex 412 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑧 < 𝑥 → ((𝑧 ∈ ℤ ∧ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦))) |
| 29 | 28 | com23 86 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → ((𝑧 ∈ ℤ ∧
∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (𝑧 < 𝑥 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦))) |
| 30 | 29 | ancomsd 465 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ⊆ ℝ) →
((∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ 𝑧 ∈ ℤ) → (𝑧 < 𝑥 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦))) |
| 31 | 30 | expdimp 452 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝐴 ⊆ ℝ) ∧
∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (𝑧 ∈ ℤ → (𝑧 < 𝑥 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦))) |
| 32 | 31 | rexlimdv 3153 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝐴 ⊆ ℝ) ∧
∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (∃𝑧 ∈ ℤ 𝑧 < 𝑥 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |
| 33 | 32 | anasss 466 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧
∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) → (∃𝑧 ∈ ℤ 𝑧 < 𝑥 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |
| 34 | 33 | expcom 413 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧
∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (𝑥 ∈ ℝ → (∃𝑧 ∈ ℤ 𝑧 < 𝑥 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦))) |
| 35 | 4, 34 | mpdi 45 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧
∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (𝑥 ∈ ℝ → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |
| 36 | 35 | ex 412 |
. . . 4
⊢ (𝐴 ⊆ ℝ →
(∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → (𝑥 ∈ ℝ → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦))) |
| 37 | 36 | com23 86 |
. . 3
⊢ (𝐴 ⊆ ℝ → (𝑥 ∈ ℝ →
(∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦))) |
| 38 | 1, 2, 37 | rexlimd 3266 |
. 2
⊢ (𝐴 ⊆ ℝ →
(∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |
| 39 | | zssre 12620 |
. . 3
⊢ ℤ
⊆ ℝ |
| 40 | | ssrexv 4053 |
. . 3
⊢ (ℤ
⊆ ℝ → (∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |
| 41 | 39, 40 | ax-mp 5 |
. 2
⊢
(∃𝑥 ∈
ℤ ∀𝑦 ∈
𝐴 𝑥 ≤ 𝑦 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) |
| 42 | 38, 41 | impbid1 225 |
1
⊢ (𝐴 ⊆ ℝ →
(∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |