| Step | Hyp | Ref
| Expression |
| 1 | | sxbrsiga.0 |
. . . . . 6
⊢ 𝐽 = (topGen‘ran
(,)) |
| 2 | | dya2ioc.1 |
. . . . . 6
⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
| 3 | | eqid 2737 |
. . . . . 6
⊢
(⌊‘(1 − (2 logb 𝑑))) = (⌊‘(1 − (2
logb 𝑑))) |
| 4 | 1, 2, 3 | dya2icoseg 34279 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑑 ∈ ℝ+)
→ ∃𝑏 ∈ ran
𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)))) |
| 5 | 4 | ralrimiva 3146 |
. . . 4
⊢ (𝑋 ∈ ℝ →
∀𝑑 ∈
ℝ+ ∃𝑏 ∈ ran 𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)))) |
| 6 | 5 | 3ad2ant1 1134 |
. . 3
⊢ ((𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸) → ∀𝑑 ∈ ℝ+ ∃𝑏 ∈ ran 𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)))) |
| 7 | | simp3 1139 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸) → 𝑋 ∈ 𝐸) |
| 8 | | iooex 13410 |
. . . . . . . . . 10
⊢ (,)
∈ V |
| 9 | 8 | rnex 7932 |
. . . . . . . . 9
⊢ ran (,)
∈ V |
| 10 | | bastg 22973 |
. . . . . . . . 9
⊢ (ran (,)
∈ V → ran (,) ⊆ (topGen‘ran (,))) |
| 11 | 9, 10 | ax-mp 5 |
. . . . . . . 8
⊢ ran (,)
⊆ (topGen‘ran (,)) |
| 12 | | simp2 1138 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸) → 𝐸 ∈ ran (,)) |
| 13 | 11, 12 | sselid 3981 |
. . . . . . 7
⊢ ((𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸) → 𝐸 ∈ (topGen‘ran
(,))) |
| 14 | 13, 1 | eleqtrrdi 2852 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸) → 𝐸 ∈ 𝐽) |
| 15 | | eqid 2737 |
. . . . . . . . 9
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
| 16 | 15 | rexmet 24812 |
. . . . . . . 8
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
| 17 | | recms 25414 |
. . . . . . . . . . 11
⊢
ℝfld ∈ CMetSp |
| 18 | | cmsms 25382 |
. . . . . . . . . . 11
⊢
(ℝfld ∈ CMetSp → ℝfld ∈
MetSp) |
| 19 | | msxms 24464 |
. . . . . . . . . . 11
⊢
(ℝfld ∈ MetSp → ℝfld ∈
∞MetSp) |
| 20 | 17, 18, 19 | mp2b 10 |
. . . . . . . . . 10
⊢
ℝfld ∈ ∞MetSp |
| 21 | | retopn 25413 |
. . . . . . . . . . . 12
⊢
(topGen‘ran (,)) =
(TopOpen‘ℝfld) |
| 22 | 1, 21 | eqtri 2765 |
. . . . . . . . . . 11
⊢ 𝐽 =
(TopOpen‘ℝfld) |
| 23 | | rebase 21624 |
. . . . . . . . . . 11
⊢ ℝ =
(Base‘ℝfld) |
| 24 | | reds 21634 |
. . . . . . . . . . . 12
⊢ (abs
∘ − ) = (dist‘ℝfld) |
| 25 | 24 | reseq1i 5993 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) =
((dist‘ℝfld) ↾ (ℝ ×
ℝ)) |
| 26 | 22, 23, 25 | xmstopn 24461 |
. . . . . . . . . 10
⊢
(ℝfld ∈ ∞MetSp → 𝐽 = (MetOpen‘((abs ∘ − )
↾ (ℝ × ℝ)))) |
| 27 | 20, 26 | ax-mp 5 |
. . . . . . . . 9
⊢ 𝐽 = (MetOpen‘((abs ∘
− ) ↾ (ℝ × ℝ))) |
| 28 | 27 | elmopn2 24455 |
. . . . . . . 8
⊢ (((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) → (𝐸 ∈ 𝐽 ↔ (𝐸 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐸 ∃𝑑 ∈ ℝ+ (𝑥(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑑) ⊆ 𝐸))) |
| 29 | 16, 28 | ax-mp 5 |
. . . . . . 7
⊢ (𝐸 ∈ 𝐽 ↔ (𝐸 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐸 ∃𝑑 ∈ ℝ+ (𝑥(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑑) ⊆ 𝐸)) |
| 30 | 29 | simprbi 496 |
. . . . . 6
⊢ (𝐸 ∈ 𝐽 → ∀𝑥 ∈ 𝐸 ∃𝑑 ∈ ℝ+ (𝑥(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑑) ⊆ 𝐸) |
| 31 | 14, 30 | syl 17 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸) → ∀𝑥 ∈ 𝐸 ∃𝑑 ∈ ℝ+ (𝑥(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑑) ⊆ 𝐸) |
| 32 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑑) = (𝑋(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑑)) |
| 33 | 32 | sseq1d 4015 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → ((𝑥(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑑) ⊆ 𝐸 ↔ (𝑋(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑑) ⊆ 𝐸)) |
| 34 | 33 | rexbidv 3179 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (∃𝑑 ∈ ℝ+ (𝑥(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑑) ⊆ 𝐸 ↔ ∃𝑑 ∈ ℝ+ (𝑋(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑑) ⊆ 𝐸)) |
| 35 | 34 | rspcva 3620 |
. . . . 5
⊢ ((𝑋 ∈ 𝐸 ∧ ∀𝑥 ∈ 𝐸 ∃𝑑 ∈ ℝ+ (𝑥(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑑) ⊆ 𝐸) → ∃𝑑 ∈ ℝ+ (𝑋(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑑) ⊆ 𝐸) |
| 36 | 7, 31, 35 | syl2anc 584 |
. . . 4
⊢ ((𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸) → ∃𝑑 ∈ ℝ+ (𝑋(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑑) ⊆ 𝐸) |
| 37 | | rpre 13043 |
. . . . . . 7
⊢ (𝑑 ∈ ℝ+
→ 𝑑 ∈
ℝ) |
| 38 | 15 | bl2ioo 24813 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑋(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑑) = ((𝑋 − 𝑑)(,)(𝑋 + 𝑑))) |
| 39 | 38 | sseq1d 4015 |
. . . . . . 7
⊢ ((𝑋 ∈ ℝ ∧ 𝑑 ∈ ℝ) → ((𝑋(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑑) ⊆ 𝐸 ↔ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ⊆ 𝐸)) |
| 40 | 37, 39 | sylan2 593 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ 𝑑 ∈ ℝ+)
→ ((𝑋(ball‘((abs
∘ − ) ↾ (ℝ × ℝ)))𝑑) ⊆ 𝐸 ↔ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ⊆ 𝐸)) |
| 41 | 40 | rexbidva 3177 |
. . . . 5
⊢ (𝑋 ∈ ℝ →
(∃𝑑 ∈
ℝ+ (𝑋(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑑) ⊆ 𝐸 ↔ ∃𝑑 ∈ ℝ+ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ⊆ 𝐸)) |
| 42 | 41 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸) → (∃𝑑 ∈ ℝ+ (𝑋(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑑) ⊆ 𝐸 ↔ ∃𝑑 ∈ ℝ+ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ⊆ 𝐸)) |
| 43 | 36, 42 | mpbid 232 |
. . 3
⊢ ((𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸) → ∃𝑑 ∈ ℝ+ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ⊆ 𝐸) |
| 44 | | r19.29 3114 |
. . 3
⊢
((∀𝑑 ∈
ℝ+ ∃𝑏 ∈ ran 𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑))) ∧ ∃𝑑 ∈ ℝ+ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ⊆ 𝐸) → ∃𝑑 ∈ ℝ+ (∃𝑏 ∈ ran 𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑))) ∧ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ⊆ 𝐸)) |
| 45 | 6, 43, 44 | syl2anc 584 |
. 2
⊢ ((𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸) → ∃𝑑 ∈ ℝ+ (∃𝑏 ∈ ran 𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑))) ∧ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ⊆ 𝐸)) |
| 46 | | r19.41v 3189 |
. . . 4
⊢
(∃𝑏 ∈ ran
𝐼((𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑))) ∧ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ⊆ 𝐸) ↔ (∃𝑏 ∈ ran 𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑))) ∧ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ⊆ 𝐸)) |
| 47 | | sstr 3992 |
. . . . . . 7
⊢ ((𝑏 ⊆ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ∧ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ⊆ 𝐸) → 𝑏 ⊆ 𝐸) |
| 48 | 47 | anim2i 617 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑏 ∧ (𝑏 ⊆ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ∧ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ⊆ 𝐸)) → (𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐸)) |
| 49 | 48 | anassrs 467 |
. . . . 5
⊢ (((𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑))) ∧ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ⊆ 𝐸) → (𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐸)) |
| 50 | 49 | reximi 3084 |
. . . 4
⊢
(∃𝑏 ∈ ran
𝐼((𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑))) ∧ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ⊆ 𝐸) → ∃𝑏 ∈ ran 𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐸)) |
| 51 | 46, 50 | sylbir 235 |
. . 3
⊢
((∃𝑏 ∈
ran 𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑))) ∧ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ⊆ 𝐸) → ∃𝑏 ∈ ran 𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐸)) |
| 52 | 51 | rexlimivw 3151 |
. 2
⊢
(∃𝑑 ∈
ℝ+ (∃𝑏 ∈ ran 𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑))) ∧ ((𝑋 − 𝑑)(,)(𝑋 + 𝑑)) ⊆ 𝐸) → ∃𝑏 ∈ ran 𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐸)) |
| 53 | 45, 52 | syl 17 |
1
⊢ ((𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸) → ∃𝑏 ∈ ran 𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐸)) |