Metamath Proof Explorer

Theorem dya2iocnei

Description: For any point of an open set of the usual topology on ( RR X. RR ) there is a closed-below open-above dyadic rational square which contains that point and is entirely in the open set. (Contributed by Thierry Arnoux, 21-Sep-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 ) ) ) )
dya2ioc.2 
|- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )
Assertion dya2iocnei 
|- ( ( A e. ( J tX J ) /\ X e. A ) -> E. b e. ran R ( X e. b /\ b C_ A ) )

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 dya2ioc.2 
 |-  R = ( u e. ran I , v e. ran I |-> ( u X. v ) )
4 elunii 
 |-  ( ( X e. A /\ A e. ( J tX J ) ) -> X e. U. ( J tX J ) )
5 4 ancoms 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> X e. U. ( J tX J ) )
6 1 tpr2uni 
 |-  U. ( J tX J ) = ( RR X. RR )
7 5 6 eleqtrdi 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> X e. ( RR X. RR ) )
8 eqid 
 |-  ( u e. RR , v e. RR |-> ( u + ( _i x. v ) ) ) = ( u e. RR , v e. RR |-> ( u + ( _i x. v ) ) )
9 eqid 
 |-  ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) ) = ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) )
10 1 8 9 tpr2rico 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> E. r e. ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) ) ( X e. r /\ r C_ A ) )
11 anass 
 |-  ( ( ( r e. ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) ) /\ X e. r ) /\ r C_ A ) <-> ( r e. ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) ) /\ ( X e. r /\ r C_ A ) ) )
12 1 2 3 9 dya2iocnrect 
 |-  ( ( X e. ( RR X. RR ) /\ r e. ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) ) /\ X e. r ) -> E. b e. ran R ( X e. b /\ b C_ r ) )
13 12 3expb 
 |-  ( ( X e. ( RR X. RR ) /\ ( r e. ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) ) /\ X e. r ) ) -> E. b e. ran R ( X e. b /\ b C_ r ) )
14 13 anim1i 
 |-  ( ( ( X e. ( RR X. RR ) /\ ( r e. ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) ) /\ X e. r ) ) /\ r C_ A ) -> ( E. b e. ran R ( X e. b /\ b C_ r ) /\ r C_ A ) )
15 14 anasss 
 |-  ( ( X e. ( RR X. RR ) /\ ( ( r e. ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) ) /\ X e. r ) /\ r C_ A ) ) -> ( E. b e. ran R ( X e. b /\ b C_ r ) /\ r C_ A ) )
16 11 15 sylan2br 
 |-  ( ( X e. ( RR X. RR ) /\ ( r e. ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) ) /\ ( X e. r /\ r C_ A ) ) ) -> ( E. b e. ran R ( X e. b /\ b C_ r ) /\ r C_ A ) )
17 r19.41v 
 |-  ( E. b e. ran R ( ( X e. b /\ b C_ r ) /\ r C_ A ) <-> ( E. b e. ran R ( X e. b /\ b C_ r ) /\ r C_ A ) )
18 simpll 
 |-  ( ( ( X e. b /\ b C_ r ) /\ r C_ A ) -> X e. b )
19 simplr 
 |-  ( ( ( X e. b /\ b C_ r ) /\ r C_ A ) -> b C_ r )
20 simpr 
 |-  ( ( ( X e. b /\ b C_ r ) /\ r C_ A ) -> r C_ A )
21 19 20 sstrd 
 |-  ( ( ( X e. b /\ b C_ r ) /\ r C_ A ) -> b C_ A )
22 18 21 jca 
 |-  ( ( ( X e. b /\ b C_ r ) /\ r C_ A ) -> ( X e. b /\ b C_ A ) )
23 22 reximi 
 |-  ( E. b e. ran R ( ( X e. b /\ b C_ r ) /\ r C_ A ) -> E. b e. ran R ( X e. b /\ b C_ A ) )
24 17 23 sylbir 
 |-  ( ( E. b e. ran R ( X e. b /\ b C_ r ) /\ r C_ A ) -> E. b e. ran R ( X e. b /\ b C_ A ) )
25 16 24 syl 
 |-  ( ( X e. ( RR X. RR ) /\ ( r e. ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) ) /\ ( X e. r /\ r C_ A ) ) ) -> E. b e. ran R ( X e. b /\ b C_ A ) )
26 25 rexlimdvaa 
 |-  ( X e. ( RR X. RR ) -> ( E. r e. ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) ) ( X e. r /\ r C_ A ) -> E. b e. ran R ( X e. b /\ b C_ A ) ) )
27 7 10 26 sylc 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> E. b e. ran R ( X e. b /\ b C_ A ) )