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 e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
Assertion dya2icoseg2 
|- ( ( X e. RR /\ E e. ran (,) /\ X e. E ) -> E. b e. ran I ( X e. b /\ b C_ E ) )

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 
 |-  J = ( topGen ` ran (,) )
2 dya2ioc.1 
 |-  I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
3 eqid 
 |-  ( |_ ` ( 1 - ( 2 logb d ) ) ) = ( |_ ` ( 1 - ( 2 logb d ) ) )
4 1 2 3 dya2icoseg 
 |-  ( ( X e. RR /\ d e. RR+ ) -> E. b e. ran I ( X e. b /\ b C_ ( ( X - d ) (,) ( X + d ) ) ) )
5 4 ralrimiva 
 |-  ( X e. RR -> A. d e. RR+ E. b e. ran I ( X e. b /\ b C_ ( ( X - d ) (,) ( X + d ) ) ) )
6 5 3ad2ant1 
 |-  ( ( X e. RR /\ E e. ran (,) /\ X e. E ) -> A. d e. RR+ E. b e. ran I ( X e. b /\ b C_ ( ( X - d ) (,) ( X + d ) ) ) )
7 simp3 
 |-  ( ( X e. RR /\ E e. ran (,) /\ X e. E ) -> X e. E )
8 iooex 
 |-  (,) e. _V
9 8 rnex 
 |-  ran (,) e. _V
10 bastg 
 |-  ( ran (,) e. _V -> ran (,) C_ ( topGen ` ran (,) ) )
11 9 10 ax-mp 
 |-  ran (,) C_ ( topGen ` ran (,) )
12 simp2 
 |-  ( ( X e. RR /\ E e. ran (,) /\ X e. E ) -> E e. ran (,) )
13 11 12 sseldi 
 |-  ( ( X e. RR /\ E e. ran (,) /\ X e. E ) -> E e. ( topGen ` ran (,) ) )
14 13 1 eleqtrrdi 
 |-  ( ( X e. RR /\ E e. ran (,) /\ X e. E ) -> E e. J )
15 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
16 15 rexmet 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
17 recms 
 |-  RRfld e. CMetSp
18 cmsms 
 |-  ( RRfld e. CMetSp -> RRfld e. MetSp )
19 msxms 
 |-  ( RRfld e. MetSp -> RRfld e. *MetSp )
20 17 18 19 mp2b 
 |-  RRfld e. *MetSp
21 retopn 
 |-  ( topGen ` ran (,) ) = ( TopOpen ` RRfld )
22 1 21 eqtri 
 |-  J = ( TopOpen ` RRfld )
23 rebase 
 |-  RR = ( Base ` RRfld )
24 reds 
 |-  ( abs o. - ) = ( dist ` RRfld )
25 24 reseq1i 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( dist ` RRfld ) |` ( RR X. RR ) )
26 22 23 25 xmstopn 
 |-  ( RRfld e. *MetSp -> J = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) )
27 20 26 ax-mp 
 |-  J = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
28 27 elmopn2 
 |-  ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) -> ( E e. J <-> ( E C_ RR /\ A. x e. E E. d e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) C_ E ) ) )
29 16 28 ax-mp 
 |-  ( E e. J <-> ( E C_ RR /\ A. x e. E E. d e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) C_ E ) )
30 29 simprbi 
 |-  ( E e. J -> A. x e. E E. d e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) C_ E )
31 14 30 syl 
 |-  ( ( X e. RR /\ E e. ran (,) /\ X e. E ) -> A. x e. E E. d e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) C_ E )
32 oveq1 
 |-  ( x = X -> ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) = ( X ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) )
33 32 sseq1d 
 |-  ( x = X -> ( ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) C_ E <-> ( X ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) C_ E ) )
34 33 rexbidv 
 |-  ( x = X -> ( E. d e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) C_ E <-> E. d e. RR+ ( X ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) C_ E ) )
35 34 rspcva 
 |-  ( ( X e. E /\ A. x e. E E. d e. RR+ ( x ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) C_ E ) -> E. d e. RR+ ( X ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) C_ E )
36 7 31 35 syl2anc 
 |-  ( ( X e. RR /\ E e. ran (,) /\ X e. E ) -> E. d e. RR+ ( X ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) C_ E )
37 rpre 
 |-  ( d e. RR+ -> d e. RR )
38 15 bl2ioo 
 |-  ( ( X e. RR /\ d e. RR ) -> ( X ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) = ( ( X - d ) (,) ( X + d ) ) )
39 38 sseq1d 
 |-  ( ( X e. RR /\ d e. RR ) -> ( ( X ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) C_ E <-> ( ( X - d ) (,) ( X + d ) ) C_ E ) )
40 37 39 sylan2 
 |-  ( ( X e. RR /\ d e. RR+ ) -> ( ( X ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) C_ E <-> ( ( X - d ) (,) ( X + d ) ) C_ E ) )
41 40 rexbidva 
 |-  ( X e. RR -> ( E. d e. RR+ ( X ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) C_ E <-> E. d e. RR+ ( ( X - d ) (,) ( X + d ) ) C_ E ) )
42 41 3ad2ant1 
 |-  ( ( X e. RR /\ E e. ran (,) /\ X e. E ) -> ( E. d e. RR+ ( X ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) d ) C_ E <-> E. d e. RR+ ( ( X - d ) (,) ( X + d ) ) C_ E ) )
43 36 42 mpbid 
 |-  ( ( X e. RR /\ E e. ran (,) /\ X e. E ) -> E. d e. RR+ ( ( X - d ) (,) ( X + d ) ) C_ E )
44 r19.29 
 |-  ( ( A. d e. RR+ E. b e. ran I ( X e. b /\ b C_ ( ( X - d ) (,) ( X + d ) ) ) /\ E. d e. RR+ ( ( X - d ) (,) ( X + d ) ) C_ E ) -> E. d e. RR+ ( E. b e. ran I ( X e. b /\ b C_ ( ( X - d ) (,) ( X + d ) ) ) /\ ( ( X - d ) (,) ( X + d ) ) C_ E ) )
45 6 43 44 syl2anc 
 |-  ( ( X e. RR /\ E e. ran (,) /\ X e. E ) -> E. d e. RR+ ( E. b e. ran I ( X e. b /\ b C_ ( ( X - d ) (,) ( X + d ) ) ) /\ ( ( X - d ) (,) ( X + d ) ) C_ E ) )
46 r19.41v 
 |-  ( E. b e. ran I ( ( X e. b /\ b C_ ( ( X - d ) (,) ( X + d ) ) ) /\ ( ( X - d ) (,) ( X + d ) ) C_ E ) <-> ( E. b e. ran I ( X e. b /\ b C_ ( ( X - d ) (,) ( X + d ) ) ) /\ ( ( X - d ) (,) ( X + d ) ) C_ E ) )
47 sstr 
 |-  ( ( b C_ ( ( X - d ) (,) ( X + d ) ) /\ ( ( X - d ) (,) ( X + d ) ) C_ E ) -> b C_ E )
48 47 anim2i 
 |-  ( ( X e. b /\ ( b C_ ( ( X - d ) (,) ( X + d ) ) /\ ( ( X - d ) (,) ( X + d ) ) C_ E ) ) -> ( X e. b /\ b C_ E ) )
49 48 anassrs 
 |-  ( ( ( X e. b /\ b C_ ( ( X - d ) (,) ( X + d ) ) ) /\ ( ( X - d ) (,) ( X + d ) ) C_ E ) -> ( X e. b /\ b C_ E ) )
50 49 reximi 
 |-  ( E. b e. ran I ( ( X e. b /\ b C_ ( ( X - d ) (,) ( X + d ) ) ) /\ ( ( X - d ) (,) ( X + d ) ) C_ E ) -> E. b e. ran I ( X e. b /\ b C_ E ) )
51 46 50 sylbir 
 |-  ( ( E. b e. ran I ( X e. b /\ b C_ ( ( X - d ) (,) ( X + d ) ) ) /\ ( ( X - d ) (,) ( X + d ) ) C_ E ) -> E. b e. ran I ( X e. b /\ b C_ E ) )
52 51 rexlimivw 
 |-  ( E. d e. RR+ ( E. b e. ran I ( X e. b /\ b C_ ( ( X - d ) (,) ( X + d ) ) ) /\ ( ( X - d ) (,) ( X + d ) ) C_ E ) -> E. b e. ran I ( X e. b /\ b C_ E ) )
53 45 52 syl 
 |-  ( ( X e. RR /\ E e. ran (,) /\ X e. E ) -> E. b e. ran I ( X e. b /\ b C_ E ) )