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 ⊒ 𝐽 = ( topGen β€˜ ran (,) )
dya2ioc.1 ⊒ 𝐼 = ( π‘₯ ∈ β„€ , 𝑛 ∈ β„€ ↦ ( ( π‘₯ / ( 2 ↑ 𝑛 ) ) [,) ( ( π‘₯ + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
Assertion dya2icoseg2 ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) β†’ βˆƒ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† 𝐸 ) )

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊒ 𝐽 = ( topGen β€˜ ran (,) )
2 dya2ioc.1 ⊒ 𝐼 = ( π‘₯ ∈ β„€ , 𝑛 ∈ β„€ ↦ ( ( π‘₯ / ( 2 ↑ 𝑛 ) ) [,) ( ( π‘₯ + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
3 eqid ⊒ ( ⌊ β€˜ ( 1 βˆ’ ( 2 logb 𝑑 ) ) ) = ( ⌊ β€˜ ( 1 βˆ’ ( 2 logb 𝑑 ) ) )
4 1 2 3 dya2icoseg ⊒ ( ( 𝑋 ∈ ℝ ∧ 𝑑 ∈ ℝ+ ) β†’ βˆƒ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) )
5 4 ralrimiva ⊒ ( 𝑋 ∈ ℝ β†’ βˆ€ 𝑑 ∈ ℝ+ βˆƒ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) )
6 5 3ad2ant1 ⊒ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) β†’ βˆ€ 𝑑 ∈ ℝ+ βˆƒ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) )
7 simp3 ⊒ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) β†’ 𝑋 ∈ 𝐸 )
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 ⊒ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) β†’ 𝐸 ∈ ran (,) )
13 11 12 sselid ⊒ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) β†’ 𝐸 ∈ ( topGen β€˜ ran (,) ) )
14 13 1 eleqtrrdi ⊒ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) β†’ 𝐸 ∈ 𝐽 )
15 eqid ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) = ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) )
16 15 rexmet ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞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 ⊒ 𝐽 = ( TopOpen β€˜ ℝfld )
23 rebase ⊒ ℝ = ( Base β€˜ ℝfld )
24 reds ⊒ ( abs ∘ βˆ’ ) = ( dist β€˜ ℝfld )
25 24 reseq1i ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) = ( ( dist β€˜ ℝfld ) β†Ύ ( ℝ Γ— ℝ ) )
26 22 23 25 xmstopn ⊒ ( ℝfld ∈ ∞MetSp β†’ 𝐽 = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) )
27 20 26 ax-mp ⊒ 𝐽 = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) )
28 27 elmopn2 ⊒ ( ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ∈ ( ∞Met β€˜ ℝ ) β†’ ( 𝐸 ∈ 𝐽 ↔ ( 𝐸 βŠ† ℝ ∧ βˆ€ π‘₯ ∈ 𝐸 βˆƒ 𝑑 ∈ ℝ+ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) βŠ† 𝐸 ) ) )
29 16 28 ax-mp ⊒ ( 𝐸 ∈ 𝐽 ↔ ( 𝐸 βŠ† ℝ ∧ βˆ€ π‘₯ ∈ 𝐸 βˆƒ 𝑑 ∈ ℝ+ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) βŠ† 𝐸 ) )
30 29 simprbi ⊒ ( 𝐸 ∈ 𝐽 β†’ βˆ€ π‘₯ ∈ 𝐸 βˆƒ 𝑑 ∈ ℝ+ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) βŠ† 𝐸 )
31 14 30 syl ⊒ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) β†’ βˆ€ π‘₯ ∈ 𝐸 βˆƒ 𝑑 ∈ ℝ+ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) βŠ† 𝐸 )
32 oveq1 ⊒ ( π‘₯ = 𝑋 β†’ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) = ( 𝑋 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) )
33 32 sseq1d ⊒ ( π‘₯ = 𝑋 β†’ ( ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) βŠ† 𝐸 ↔ ( 𝑋 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) βŠ† 𝐸 ) )
34 33 rexbidv ⊒ ( π‘₯ = 𝑋 β†’ ( βˆƒ 𝑑 ∈ ℝ+ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) βŠ† 𝐸 ↔ βˆƒ 𝑑 ∈ ℝ+ ( 𝑋 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) βŠ† 𝐸 ) )
35 34 rspcva ⊒ ( ( 𝑋 ∈ 𝐸 ∧ βˆ€ π‘₯ ∈ 𝐸 βˆƒ 𝑑 ∈ ℝ+ ( π‘₯ ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) βŠ† 𝐸 ) β†’ βˆƒ 𝑑 ∈ ℝ+ ( 𝑋 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) βŠ† 𝐸 )
36 7 31 35 syl2anc ⊒ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) β†’ βˆƒ 𝑑 ∈ ℝ+ ( 𝑋 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) βŠ† 𝐸 )
37 rpre ⊒ ( 𝑑 ∈ ℝ+ β†’ 𝑑 ∈ ℝ )
38 15 bl2ioo ⊒ ( ( 𝑋 ∈ ℝ ∧ 𝑑 ∈ ℝ ) β†’ ( 𝑋 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) = ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) )
39 38 sseq1d ⊒ ( ( 𝑋 ∈ ℝ ∧ 𝑑 ∈ ℝ ) β†’ ( ( 𝑋 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) βŠ† 𝐸 ↔ ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) βŠ† 𝐸 ) )
40 37 39 sylan2 ⊒ ( ( 𝑋 ∈ ℝ ∧ 𝑑 ∈ ℝ+ ) β†’ ( ( 𝑋 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) βŠ† 𝐸 ↔ ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) βŠ† 𝐸 ) )
41 40 rexbidva ⊒ ( 𝑋 ∈ ℝ β†’ ( βˆƒ 𝑑 ∈ ℝ+ ( 𝑋 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) βŠ† 𝐸 ↔ βˆƒ 𝑑 ∈ ℝ+ ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) βŠ† 𝐸 ) )
42 41 3ad2ant1 ⊒ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) β†’ ( βˆƒ 𝑑 ∈ ℝ+ ( 𝑋 ( ball β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) ) ) 𝑑 ) βŠ† 𝐸 ↔ βˆƒ 𝑑 ∈ ℝ+ ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) βŠ† 𝐸 ) )
43 36 42 mpbid ⊒ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) β†’ βˆƒ 𝑑 ∈ ℝ+ ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) βŠ† 𝐸 )
44 r19.29 ⊒ ( ( βˆ€ 𝑑 ∈ ℝ+ βˆƒ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ βˆƒ 𝑑 ∈ ℝ+ ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) βŠ† 𝐸 ) β†’ βˆƒ 𝑑 ∈ ℝ+ ( βˆƒ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) βŠ† 𝐸 ) )
45 6 43 44 syl2anc ⊒ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) β†’ βˆƒ 𝑑 ∈ ℝ+ ( βˆƒ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) βŠ† 𝐸 ) )
46 r19.41v ⊒ ( βˆƒ 𝑏 ∈ ran 𝐼 ( ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) βŠ† 𝐸 ) ↔ ( βˆƒ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) βŠ† 𝐸 ) )
47 sstr ⊒ ( ( 𝑏 βŠ† ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ∧ ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) βŠ† 𝐸 ) β†’ 𝑏 βŠ† 𝐸 )
48 47 anim2i ⊒ ( ( 𝑋 ∈ 𝑏 ∧ ( 𝑏 βŠ† ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ∧ ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) βŠ† 𝐸 ) ) β†’ ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† 𝐸 ) )
49 48 anassrs ⊒ ( ( ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) βŠ† 𝐸 ) β†’ ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† 𝐸 ) )
50 49 reximi ⊒ ( βˆƒ 𝑏 ∈ ran 𝐼 ( ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) βŠ† 𝐸 ) β†’ βˆƒ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† 𝐸 ) )
51 46 50 sylbir ⊒ ( ( βˆƒ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) βŠ† 𝐸 ) β†’ βˆƒ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† 𝐸 ) )
52 51 rexlimivw ⊒ ( βˆƒ 𝑑 ∈ ℝ+ ( βˆƒ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ( ( 𝑋 βˆ’ 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) βŠ† 𝐸 ) β†’ βˆƒ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† 𝐸 ) )
53 45 52 syl ⊒ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) β†’ βˆƒ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 βŠ† 𝐸 ) )