Metamath Proof Explorer

Theorem dya2iocucvr

Description: The dyadic rectangular set collection covers ( RR X. RR ) . (Contributed by Thierry Arnoux, 18-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 dya2iocucvr 
|- U. ran R = ( RR X. RR )

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 unissb 
 |-  ( U. ran R C_ ( RR X. RR ) <-> A. d e. ran R d C_ ( RR X. RR ) )
5 vex 
 |-  u e. _V
6 vex 
 |-  v e. _V
7 5 6 xpex 
 |-  ( u X. v ) e. _V
8 3 7 elrnmpo 
 |-  ( d e. ran R <-> E. u e. ran I E. v e. ran I d = ( u X. v ) )
9 simpr 
 |-  ( ( ( u e. ran I /\ v e. ran I ) /\ d = ( u X. v ) ) -> d = ( u X. v ) )
10 pwssb 
 |-  ( ran I C_ ~P RR <-> A. d e. ran I d C_ RR )
11 ovex 
 |-  ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) e. _V
12 2 11 elrnmpo 
 |-  ( d e. ran I <-> E. x e. ZZ E. n e. ZZ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
13 simpr 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
14 simpll 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> x e. ZZ )
15 14 zred 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> x e. RR )
16 2re 
 |-  2 e. RR
17 16 a1i 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> 2 e. RR )
18 2ne0 
 |-  2 =/= 0
19 18 a1i 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> 2 =/= 0 )
20 simplr 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> n e. ZZ )
21 17 19 20 reexpclzd 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> ( 2 ^ n ) e. RR )
22 2cnd 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> 2 e. CC )
23 22 19 20 expne0d 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> ( 2 ^ n ) =/= 0 )
24 15 21 23 redivcld 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> ( x / ( 2 ^ n ) ) e. RR )
25 1red 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> 1 e. RR )
26 15 25 readdcld 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> ( x + 1 ) e. RR )
27 26 21 23 redivcld 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> ( ( x + 1 ) / ( 2 ^ n ) ) e. RR )
28 27 rexrd 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> ( ( x + 1 ) / ( 2 ^ n ) ) e. RR* )
29 icossre 
 |-  ( ( ( x / ( 2 ^ n ) ) e. RR /\ ( ( x + 1 ) / ( 2 ^ n ) ) e. RR* ) -> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) C_ RR )
30 24 28 29 syl2anc 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) C_ RR )
31 13 30 eqsstrd 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> d C_ RR )
32 31 ex 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> ( d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) -> d C_ RR ) )
33 32 rexlimivv 
 |-  ( E. x e. ZZ E. n e. ZZ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) -> d C_ RR )
34 12 33 sylbi 
 |-  ( d e. ran I -> d C_ RR )
35 10 34 mprgbir 
 |-  ran I C_ ~P RR
36 35 sseli 
 |-  ( u e. ran I -> u e. ~P RR )
37 36 elpwid 
 |-  ( u e. ran I -> u C_ RR )
38 35 sseli 
 |-  ( v e. ran I -> v e. ~P RR )
39 38 elpwid 
 |-  ( v e. ran I -> v C_ RR )
40 xpss12 
 |-  ( ( u C_ RR /\ v C_ RR ) -> ( u X. v ) C_ ( RR X. RR ) )
41 37 39 40 syl2an 
 |-  ( ( u e. ran I /\ v e. ran I ) -> ( u X. v ) C_ ( RR X. RR ) )
42 41 adantr 
 |-  ( ( ( u e. ran I /\ v e. ran I ) /\ d = ( u X. v ) ) -> ( u X. v ) C_ ( RR X. RR ) )
43 9 42 eqsstrd 
 |-  ( ( ( u e. ran I /\ v e. ran I ) /\ d = ( u X. v ) ) -> d C_ ( RR X. RR ) )
44 43 ex 
 |-  ( ( u e. ran I /\ v e. ran I ) -> ( d = ( u X. v ) -> d C_ ( RR X. RR ) ) )
45 44 rexlimivv 
 |-  ( E. u e. ran I E. v e. ran I d = ( u X. v ) -> d C_ ( RR X. RR ) )
46 8 45 sylbi 
 |-  ( d e. ran R -> d C_ ( RR X. RR ) )
47 4 46 mprgbir 
 |-  U. ran R C_ ( RR X. RR )
48 retop 
 |-  ( topGen ` ran (,) ) e. Top
49 1 48 eqeltri 
 |-  J e. Top
50 49 49 txtopi 
 |-  ( J tX J ) e. Top
51 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
52 1 unieqi 
 |-  U. J = U. ( topGen ` ran (,) )
53 51 52 eqtr4i 
 |-  RR = U. J
54 49 49 53 53 txunii 
 |-  ( RR X. RR ) = U. ( J tX J )
55 54 topopn 
 |-  ( ( J tX J ) e. Top -> ( RR X. RR ) e. ( J tX J ) )
56 1 2 3 dya2iocuni 
 |-  ( ( RR X. RR ) e. ( J tX J ) -> E. c e. ~P ran R U. c = ( RR X. RR ) )
57 50 55 56 mp2b 
 |-  E. c e. ~P ran R U. c = ( RR X. RR )
58 simpr 
 |-  ( ( c e. ~P ran R /\ U. c = ( RR X. RR ) ) -> U. c = ( RR X. RR ) )
59 elpwi 
 |-  ( c e. ~P ran R -> c C_ ran R )
60 59 adantr 
 |-  ( ( c e. ~P ran R /\ U. c = ( RR X. RR ) ) -> c C_ ran R )
61 60 unissd 
 |-  ( ( c e. ~P ran R /\ U. c = ( RR X. RR ) ) -> U. c C_ U. ran R )
62 58 61 eqsstrrd 
 |-  ( ( c e. ~P ran R /\ U. c = ( RR X. RR ) ) -> ( RR X. RR ) C_ U. ran R )
63 62 rexlimiva 
 |-  ( E. c e. ~P ran R U. c = ( RR X. RR ) -> ( RR X. RR ) C_ U. ran R )
64 57 63 ax-mp 
 |-  ( RR X. RR ) C_ U. ran R
65 47 64 eqssi 
 |-  U. ran R = ( RR X. RR )