Metamath Proof Explorer

Theorem dya2icoseg2

Description: For any point and any open interval of RR containing that point, there is a closed-below open-above dyadic rational interval which contains that point and is included in the original interval. (Contributed by Thierry Arnoux, 12-Oct-2017)

Ref Expression
Hypotheses sxbrsiga.0 ⊢ J = topGen ⁡ ran ⁡ .
dya2ioc.1 ⊢ I = x ∈ ℤ , n ∈ ℤ ⟼ x 2 n x + 1 2 n
Assertion dya2icoseg2 ⊢ X ∈ ℝ ∧ E ∈ ran ⁡ . ∧ X ∈ E → ∃ b ∈ ran ⁡ I X ∈ b ∧ b ⊆ E

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊢ J = topGen ⁡ ran ⁡ .
2 dya2ioc.1 ⊢ I = x ∈ ℤ , n ∈ ℤ ⟼ x 2 n x + 1 2 n
3 eqid ⊢ 1 − log 2 d = 1 − log 2 d
4 1 2 3 dya2icoseg ⊢ X ∈ ℝ ∧ d ∈ ℝ + → ∃ b ∈ ran ⁡ I X ∈ b ∧ b ⊆ X − d X + d
5 4 ralrimiva ⊢ X ∈ ℝ → ∀ d ∈ ℝ + ∃ b ∈ ran ⁡ I X ∈ b ∧ b ⊆ X − d X + d
6 5 3ad2ant1 ⊢ X ∈ ℝ ∧ E ∈ ran ⁡ . ∧ X ∈ E → ∀ d ∈ ℝ + ∃ b ∈ ran ⁡ I X ∈ b ∧ b ⊆ X − d X + d
7 simp3 ⊢ X ∈ ℝ ∧ E ∈ ran ⁡ . ∧ X ∈ E → X ∈ E
8 iooex ⊢ . ∈ V
9 8 rnex ⊢ ran ⁡ . ∈ V
10 bastg ⊢ ran ⁡ . ∈ V → ran ⁡ . ⊆ topGen ⁡ ran ⁡ .
11 9 10 ax-mp ⊢ ran ⁡ . ⊆ topGen ⁡ ran ⁡ .
12 simp2 ⊢ X ∈ ℝ ∧ E ∈ ran ⁡ . ∧ X ∈ E → E ∈ ran ⁡ .
13 11 12 sseldi ⊢ X ∈ ℝ ∧ E ∈ ran ⁡ . ∧ X ∈ E → E ∈ topGen ⁡ ran ⁡ .
14 13 1 eleqtrrdi ⊢ X ∈ ℝ ∧ E ∈ ran ⁡ . ∧ X ∈ E → E ∈ J
15 eqid ⊢ abs ∘ − ↾ ℝ 2 = abs ∘ − ↾ ℝ 2
16 15 rexmet ⊢ abs ∘ − ↾ ℝ 2 ∈ ∞Met ⁡ ℝ
17 recms ⊢ ℝ fld ∈ CMetSp
18 cmsms ⊢ ℝ fld ∈ CMetSp → ℝ fld ∈ MetSp
19 msxms ⊢ ℝ fld ∈ MetSp → ℝ fld ∈ ∞MetSp
20 17 18 19 mp2b ⊢ ℝ fld ∈ ∞MetSp
21 retopn ⊢ topGen ⁡ ran ⁡ . = TopOpen ⁡ ℝ fld
22 1 21 eqtri ⊢ J = TopOpen ⁡ ℝ fld
23 rebase ⊢ ℝ = Base ℝ fld
24 reds ⊢ abs ∘ − = dist ⁡ ℝ fld
25 24 reseq1i ⊢ abs ∘ − ↾ ℝ 2 = dist ⁡ ℝ fld ↾ ℝ 2
26 22 23 25 xmstopn ⊢ ℝ fld ∈ ∞MetSp → J = MetOpen ⁡ abs ∘ − ↾ ℝ 2
27 20 26 ax-mp ⊢ J = MetOpen ⁡ abs ∘ − ↾ ℝ 2
28 27 elmopn2 ⊢ abs ∘ − ↾ ℝ 2 ∈ ∞Met ⁡ ℝ → E ∈ J ↔ E ⊆ ℝ ∧ ∀ x ∈ E ∃ d ∈ ℝ + x ball ⁡ abs ∘ − ↾ ℝ 2 d ⊆ E
29 16 28 ax-mp ⊢ E ∈ J ↔ E ⊆ ℝ ∧ ∀ x ∈ E ∃ d ∈ ℝ + x ball ⁡ abs ∘ − ↾ ℝ 2 d ⊆ E
30 29 simprbi ⊢ E ∈ J → ∀ x ∈ E ∃ d ∈ ℝ + x ball ⁡ abs ∘ − ↾ ℝ 2 d ⊆ E
31 14 30 syl ⊢ X ∈ ℝ ∧ E ∈ ran ⁡ . ∧ X ∈ E → ∀ x ∈ E ∃ d ∈ ℝ + x ball ⁡ abs ∘ − ↾ ℝ 2 d ⊆ E
32 oveq1 ⊢ x = X → x ball ⁡ abs ∘ − ↾ ℝ 2 d = X ball ⁡ abs ∘ − ↾ ℝ 2 d
33 32 sseq1d ⊢ x = X → x ball ⁡ abs ∘ − ↾ ℝ 2 d ⊆ E ↔ X ball ⁡ abs ∘ − ↾ ℝ 2 d ⊆ E
34 33 rexbidv ⊢ x = X → ∃ d ∈ ℝ + x ball ⁡ abs ∘ − ↾ ℝ 2 d ⊆ E ↔ ∃ d ∈ ℝ + X ball ⁡ abs ∘ − ↾ ℝ 2 d ⊆ E
35 34 rspcva ⊢ X ∈ E ∧ ∀ x ∈ E ∃ d ∈ ℝ + x ball ⁡ abs ∘ − ↾ ℝ 2 d ⊆ E → ∃ d ∈ ℝ + X ball ⁡ abs ∘ − ↾ ℝ 2 d ⊆ E
36 7 31 35 syl2anc ⊢ X ∈ ℝ ∧ E ∈ ran ⁡ . ∧ X ∈ E → ∃ d ∈ ℝ + X ball ⁡ abs ∘ − ↾ ℝ 2 d ⊆ E
37 rpre ⊢ d ∈ ℝ + → d ∈ ℝ
38 15 bl2ioo ⊢ X ∈ ℝ ∧ d ∈ ℝ → X ball ⁡ abs ∘ − ↾ ℝ 2 d = X − d X + d
39 38 sseq1d ⊢ X ∈ ℝ ∧ d ∈ ℝ → X ball ⁡ abs ∘ − ↾ ℝ 2 d ⊆ E ↔ X − d X + d ⊆ E
40 37 39 sylan2 ⊢ X ∈ ℝ ∧ d ∈ ℝ + → X ball ⁡ abs ∘ − ↾ ℝ 2 d ⊆ E ↔ X − d X + d ⊆ E
41 40 rexbidva ⊢ X ∈ ℝ → ∃ d ∈ ℝ + X ball ⁡ abs ∘ − ↾ ℝ 2 d ⊆ E ↔ ∃ d ∈ ℝ + X − d X + d ⊆ E
42 41 3ad2ant1 ⊢ X ∈ ℝ ∧ E ∈ ran ⁡ . ∧ X ∈ E → ∃ d ∈ ℝ + X ball ⁡ abs ∘ − ↾ ℝ 2 d ⊆ E ↔ ∃ d ∈ ℝ + X − d X + d ⊆ E
43 36 42 mpbid ⊢ X ∈ ℝ ∧ E ∈ ran ⁡ . ∧ X ∈ E → ∃ d ∈ ℝ + X − d X + d ⊆ E
44 r19.29 ⊢ ∀ d ∈ ℝ + ∃ b ∈ ran ⁡ I X ∈ b ∧ b ⊆ X − d X + d ∧ ∃ d ∈ ℝ + X − d X + d ⊆ E → ∃ d ∈ ℝ + ∃ b ∈ ran ⁡ I X ∈ b ∧ b ⊆ X − d X + d ∧ X − d X + d ⊆ E
45 6 43 44 syl2anc ⊢ X ∈ ℝ ∧ E ∈ ran ⁡ . ∧ X ∈ E → ∃ d ∈ ℝ + ∃ b ∈ ran ⁡ I X ∈ b ∧ b ⊆ X − d X + d ∧ X − d X + d ⊆ E
46 r19.41v ⊢ ∃ b ∈ ran ⁡ I X ∈ b ∧ b ⊆ X − d X + d ∧ X − d X + d ⊆ E ↔ ∃ b ∈ ran ⁡ I X ∈ b ∧ b ⊆ X − d X + d ∧ X − d X + d ⊆ E
47 sstr ⊢ b ⊆ X − d X + d ∧ X − d X + d ⊆ E → b ⊆ E
48 47 anim2i ⊢ X ∈ b ∧ b ⊆ X − d X + d ∧ X − d X + d ⊆ E → X ∈ b ∧ b ⊆ E
49 48 anassrs ⊢ X ∈ b ∧ b ⊆ X − d X + d ∧ X − d X + d ⊆ E → X ∈ b ∧ b ⊆ E
50 49 reximi ⊢ ∃ b ∈ ran ⁡ I X ∈ b ∧ b ⊆ X − d X + d ∧ X − d X + d ⊆ E → ∃ b ∈ ran ⁡ I X ∈ b ∧ b ⊆ E
51 46 50 sylbir ⊢ ∃ b ∈ ran ⁡ I X ∈ b ∧ b ⊆ X − d X + d ∧ X − d X + d ⊆ E → ∃ b ∈ ran ⁡ I X ∈ b ∧ b ⊆ E
52 51 rexlimivw ⊢ ∃ d ∈ ℝ + ∃ b ∈ ran ⁡ I X ∈ b ∧ b ⊆ X − d X + d ∧ X − d X + d ⊆ E → ∃ b ∈ ran ⁡ I X ∈ b ∧ b ⊆ E
53 45 52 syl ⊢ X ∈ ℝ ∧ E ∈ ran ⁡ . ∧ X ∈ E → ∃ b ∈ ran ⁡ I X ∈ b ∧ b ⊆ E