Metamath Proof Explorer

Theorem dya2iocnrect

Description: For any point of an open rectangle in ( RR X. RR ) , there is a closed-below open-above dyadic rational square which contains that point and is included in the rectangle. (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 ) ) ) )
dya2ioc.2 
|- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )
dya2iocnrect.1 
|- B = ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) )
Assertion dya2iocnrect 
|- ( ( X e. ( RR X. RR ) /\ A e. B /\ 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 dya2iocnrect.1 
 |-  B = ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) )
5 4 eleq2i 
 |-  ( A e. B <-> A e. ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) ) )
6 eqid 
 |-  ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) ) = ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) )
7 vex 
 |-  e e. _V
8 vex 
 |-  f e. _V
9 7 8 xpex 
 |-  ( e X. f ) e. _V
10 6 9 elrnmpo 
 |-  ( A e. ran ( e e. ran (,) , f e. ran (,) |-> ( e X. f ) ) <-> E. e e. ran (,) E. f e. ran (,) A = ( e X. f ) )
11 5 10 sylbb 
 |-  ( A e. B -> E. e e. ran (,) E. f e. ran (,) A = ( e X. f ) )
12 11 3ad2ant2 
 |-  ( ( X e. ( RR X. RR ) /\ A e. B /\ X e. A ) -> E. e e. ran (,) E. f e. ran (,) A = ( e X. f ) )
13 simp1 
 |-  ( ( X e. ( RR X. RR ) /\ A e. B /\ X e. A ) -> X e. ( RR X. RR ) )
14 simp3 
 |-  ( ( X e. ( RR X. RR ) /\ A e. B /\ X e. A ) -> X e. A )
15 12 13 14 jca32 
 |-  ( ( X e. ( RR X. RR ) /\ A e. B /\ X e. A ) -> ( E. e e. ran (,) E. f e. ran (,) A = ( e X. f ) /\ ( X e. ( RR X. RR ) /\ X e. A ) ) )
16 r19.41vv 
 |-  ( E. e e. ran (,) E. f e. ran (,) ( A = ( e X. f ) /\ ( X e. ( RR X. RR ) /\ X e. A ) ) <-> ( E. e e. ran (,) E. f e. ran (,) A = ( e X. f ) /\ ( X e. ( RR X. RR ) /\ X e. A ) ) )
17 16 biimpri 
 |-  ( ( E. e e. ran (,) E. f e. ran (,) A = ( e X. f ) /\ ( X e. ( RR X. RR ) /\ X e. A ) ) -> E. e e. ran (,) E. f e. ran (,) ( A = ( e X. f ) /\ ( X e. ( RR X. RR ) /\ X e. A ) ) )
18 simprl 
 |-  ( ( A = ( e X. f ) /\ ( X e. ( RR X. RR ) /\ X e. A ) ) -> X e. ( RR X. RR ) )
19 simpl 
 |-  ( ( A = ( e X. f ) /\ ( X e. ( RR X. RR ) /\ X e. A ) ) -> A = ( e X. f ) )
20 simprr 
 |-  ( ( A = ( e X. f ) /\ ( X e. ( RR X. RR ) /\ X e. A ) ) -> X e. A )
21 20 19 eleqtrd 
 |-  ( ( A = ( e X. f ) /\ ( X e. ( RR X. RR ) /\ X e. A ) ) -> X e. ( e X. f ) )
22 18 19 21 3jca 
 |-  ( ( A = ( e X. f ) /\ ( X e. ( RR X. RR ) /\ X e. A ) ) -> ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) )
23 simpr 
 |-  ( ( ( e e. ran (,) /\ f e. ran (,) ) /\ ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) ) -> ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) )
24 xp1st 
 |-  ( X e. ( RR X. RR ) -> ( 1st ` X ) e. RR )
25 24 3ad2ant1 
 |-  ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) -> ( 1st ` X ) e. RR )
26 25 adantl 
 |-  ( ( ( e e. ran (,) /\ f e. ran (,) ) /\ ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) ) -> ( 1st ` X ) e. RR )
27 simpll 
 |-  ( ( ( e e. ran (,) /\ f e. ran (,) ) /\ ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) ) -> e e. ran (,) )
28 xp1st 
 |-  ( X e. ( e X. f ) -> ( 1st ` X ) e. e )
29 28 3ad2ant3 
 |-  ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) -> ( 1st ` X ) e. e )
30 29 adantl 
 |-  ( ( ( e e. ran (,) /\ f e. ran (,) ) /\ ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) ) -> ( 1st ` X ) e. e )
31 1 2 dya2icoseg2 
 |-  ( ( ( 1st ` X ) e. RR /\ e e. ran (,) /\ ( 1st ` X ) e. e ) -> E. s e. ran I ( ( 1st ` X ) e. s /\ s C_ e ) )
32 26 27 30 31 syl3anc 
 |-  ( ( ( e e. ran (,) /\ f e. ran (,) ) /\ ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) ) -> E. s e. ran I ( ( 1st ` X ) e. s /\ s C_ e ) )
33 xp2nd 
 |-  ( X e. ( RR X. RR ) -> ( 2nd ` X ) e. RR )
34 33 3ad2ant1 
 |-  ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) -> ( 2nd ` X ) e. RR )
35 34 adantl 
 |-  ( ( ( e e. ran (,) /\ f e. ran (,) ) /\ ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) ) -> ( 2nd ` X ) e. RR )
36 simplr 
 |-  ( ( ( e e. ran (,) /\ f e. ran (,) ) /\ ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) ) -> f e. ran (,) )
37 xp2nd 
 |-  ( X e. ( e X. f ) -> ( 2nd ` X ) e. f )
38 37 3ad2ant3 
 |-  ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) -> ( 2nd ` X ) e. f )
39 38 adantl 
 |-  ( ( ( e e. ran (,) /\ f e. ran (,) ) /\ ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) ) -> ( 2nd ` X ) e. f )
40 1 2 dya2icoseg2 
 |-  ( ( ( 2nd ` X ) e. RR /\ f e. ran (,) /\ ( 2nd ` X ) e. f ) -> E. t e. ran I ( ( 2nd ` X ) e. t /\ t C_ f ) )
41 35 36 39 40 syl3anc 
 |-  ( ( ( e e. ran (,) /\ f e. ran (,) ) /\ ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) ) -> E. t e. ran I ( ( 2nd ` X ) e. t /\ t C_ f ) )
42 reeanv 
 |-  ( E. s e. ran I E. t e. ran I ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) <-> ( E. s e. ran I ( ( 1st ` X ) e. s /\ s C_ e ) /\ E. t e. ran I ( ( 2nd ` X ) e. t /\ t C_ f ) ) )
43 32 41 42 sylanbrc 
 |-  ( ( ( e e. ran (,) /\ f e. ran (,) ) /\ ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) ) -> E. s e. ran I E. t e. ran I ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) )
44 eqid 
 |-  ( s X. t ) = ( s X. t )
45 xpeq1 
 |-  ( u = s -> ( u X. v ) = ( s X. v ) )
46 45 eqeq2d 
 |-  ( u = s -> ( ( s X. t ) = ( u X. v ) <-> ( s X. t ) = ( s X. v ) ) )
47 xpeq2 
 |-  ( v = t -> ( s X. v ) = ( s X. t ) )
48 47 eqeq2d 
 |-  ( v = t -> ( ( s X. t ) = ( s X. v ) <-> ( s X. t ) = ( s X. t ) ) )
49 46 48 rspc2ev 
 |-  ( ( s e. ran I /\ t e. ran I /\ ( s X. t ) = ( s X. t ) ) -> E. u e. ran I E. v e. ran I ( s X. t ) = ( u X. v ) )
50 44 49 mp3an3 
 |-  ( ( s e. ran I /\ t e. ran I ) -> E. u e. ran I E. v e. ran I ( s X. t ) = ( u X. v ) )
51 vex 
 |-  u e. _V
52 vex 
 |-  v e. _V
53 51 52 xpex 
 |-  ( u X. v ) e. _V
54 3 53 elrnmpo 
 |-  ( ( s X. t ) e. ran R <-> E. u e. ran I E. v e. ran I ( s X. t ) = ( u X. v ) )
55 50 54 sylibr 
 |-  ( ( s e. ran I /\ t e. ran I ) -> ( s X. t ) e. ran R )
56 55 ad2antrl 
 |-  ( ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) /\ ( ( s e. ran I /\ t e. ran I ) /\ ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) ) ) -> ( s X. t ) e. ran R )
57 xpss 
 |-  ( RR X. RR ) C_ ( _V X. _V )
58 simpl1 
 |-  ( ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) /\ ( ( s e. ran I /\ t e. ran I ) /\ ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) ) ) -> X e. ( RR X. RR ) )
59 57 58 sseldi 
 |-  ( ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) /\ ( ( s e. ran I /\ t e. ran I ) /\ ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) ) ) -> X e. ( _V X. _V ) )
60 simprrl 
 |-  ( ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) /\ ( ( s e. ran I /\ t e. ran I ) /\ ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) ) ) -> ( ( 1st ` X ) e. s /\ s C_ e ) )
61 60 simpld 
 |-  ( ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) /\ ( ( s e. ran I /\ t e. ran I ) /\ ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) ) ) -> ( 1st ` X ) e. s )
62 simprrr 
 |-  ( ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) /\ ( ( s e. ran I /\ t e. ran I ) /\ ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) ) ) -> ( ( 2nd ` X ) e. t /\ t C_ f ) )
63 62 simpld 
 |-  ( ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) /\ ( ( s e. ran I /\ t e. ran I ) /\ ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) ) ) -> ( 2nd ` X ) e. t )
64 elxp7 
 |-  ( X e. ( s X. t ) <-> ( X e. ( _V X. _V ) /\ ( ( 1st ` X ) e. s /\ ( 2nd ` X ) e. t ) ) )
65 64 biimpri 
 |-  ( ( X e. ( _V X. _V ) /\ ( ( 1st ` X ) e. s /\ ( 2nd ` X ) e. t ) ) -> X e. ( s X. t ) )
66 59 61 63 65 syl12anc 
 |-  ( ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) /\ ( ( s e. ran I /\ t e. ran I ) /\ ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) ) ) -> X e. ( s X. t ) )
67 60 simprd 
 |-  ( ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) /\ ( ( s e. ran I /\ t e. ran I ) /\ ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) ) ) -> s C_ e )
68 62 simprd 
 |-  ( ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) /\ ( ( s e. ran I /\ t e. ran I ) /\ ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) ) ) -> t C_ f )
69 xpss12 
 |-  ( ( s C_ e /\ t C_ f ) -> ( s X. t ) C_ ( e X. f ) )
70 67 68 69 syl2anc 
 |-  ( ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) /\ ( ( s e. ran I /\ t e. ran I ) /\ ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) ) ) -> ( s X. t ) C_ ( e X. f ) )
71 simpl2 
 |-  ( ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) /\ ( ( s e. ran I /\ t e. ran I ) /\ ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) ) ) -> A = ( e X. f ) )
72 70 71 sseqtrrd 
 |-  ( ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) /\ ( ( s e. ran I /\ t e. ran I ) /\ ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) ) ) -> ( s X. t ) C_ A )
73 eleq2 
 |-  ( b = ( s X. t ) -> ( X e. b <-> X e. ( s X. t ) ) )
74 sseq1 
 |-  ( b = ( s X. t ) -> ( b C_ A <-> ( s X. t ) C_ A ) )
75 73 74 anbi12d 
 |-  ( b = ( s X. t ) -> ( ( X e. b /\ b C_ A ) <-> ( X e. ( s X. t ) /\ ( s X. t ) C_ A ) ) )
76 75 rspcev 
 |-  ( ( ( s X. t ) e. ran R /\ ( X e. ( s X. t ) /\ ( s X. t ) C_ A ) ) -> E. b e. ran R ( X e. b /\ b C_ A ) )
77 56 66 72 76 syl12anc 
 |-  ( ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) /\ ( ( s e. ran I /\ t e. ran I ) /\ ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) ) ) -> E. b e. ran R ( X e. b /\ b C_ A ) )
78 77 exp32 
 |-  ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) -> ( ( s e. ran I /\ t e. ran I ) -> ( ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) -> E. b e. ran R ( X e. b /\ b C_ A ) ) ) )
79 78 rexlimdvv 
 |-  ( ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) -> ( E. s e. ran I E. t e. ran I ( ( ( 1st ` X ) e. s /\ s C_ e ) /\ ( ( 2nd ` X ) e. t /\ t C_ f ) ) -> E. b e. ran R ( X e. b /\ b C_ A ) ) )
80 23 43 79 sylc 
 |-  ( ( ( e e. ran (,) /\ f e. ran (,) ) /\ ( X e. ( RR X. RR ) /\ A = ( e X. f ) /\ X e. ( e X. f ) ) ) -> E. b e. ran R ( X e. b /\ b C_ A ) )
81 22 80 sylan2 
 |-  ( ( ( e e. ran (,) /\ f e. ran (,) ) /\ ( A = ( e X. f ) /\ ( X e. ( RR X. RR ) /\ X e. A ) ) ) -> E. b e. ran R ( X e. b /\ b C_ A ) )
82 81 ex 
 |-  ( ( e e. ran (,) /\ f e. ran (,) ) -> ( ( A = ( e X. f ) /\ ( X e. ( RR X. RR ) /\ X e. A ) ) -> E. b e. ran R ( X e. b /\ b C_ A ) ) )
83 82 rexlimivv 
 |-  ( E. e e. ran (,) E. f e. ran (,) ( A = ( e X. f ) /\ ( X e. ( RR X. RR ) /\ X e. A ) ) -> E. b e. ran R ( X e. b /\ b C_ A ) )
84 15 17 83 3syl 
 |-  ( ( X e. ( RR X. RR ) /\ A e. B /\ X e. A ) -> E. b e. ran R ( X e. b /\ b C_ A ) )