Metamath Proof Explorer

Theorem dya2icobrsiga

Description: Dyadic intervals are Borel sets of RR . (Contributed by Thierry Arnoux, 22-Sep-2017) (Revised by Thierry Arnoux, 13-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 dya2icobrsiga 
|- ran I C_ BrSiga

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 ovex 
 |-  ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) e. _V
4 2 3 elrnmpo 
 |-  ( d e. ran I <-> E. x e. ZZ E. n e. ZZ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
5 simpr 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
6 mnfxr 
 |-  -oo e. RR*
7 6 a1i 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> -oo e. RR* )
8 simpl 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> x e. ZZ )
9 8 zred 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> x e. RR )
10 2rp 
 |-  2 e. RR+
11 10 a1i 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> 2 e. RR+ )
12 simpr 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> n e. ZZ )
13 11 12 rpexpcld 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> ( 2 ^ n ) e. RR+ )
14 9 13 rerpdivcld 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> ( x / ( 2 ^ n ) ) e. RR )
15 14 rexrd 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> ( x / ( 2 ^ n ) ) e. RR* )
16 1red 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> 1 e. RR )
17 9 16 readdcld 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> ( x + 1 ) e. RR )
18 17 13 rerpdivcld 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> ( ( x + 1 ) / ( 2 ^ n ) ) e. RR )
19 18 rexrd 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> ( ( x + 1 ) / ( 2 ^ n ) ) e. RR* )
20 mnflt 
 |-  ( ( x / ( 2 ^ n ) ) e. RR -> -oo < ( x / ( 2 ^ n ) ) )
21 14 20 syl 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> -oo < ( x / ( 2 ^ n ) ) )
22 difioo 
 |-  ( ( ( -oo e. RR* /\ ( x / ( 2 ^ n ) ) e. RR* /\ ( ( x + 1 ) / ( 2 ^ n ) ) e. RR* ) /\ -oo < ( x / ( 2 ^ n ) ) ) -> ( ( -oo (,) ( ( x + 1 ) / ( 2 ^ n ) ) ) \ ( -oo (,) ( x / ( 2 ^ n ) ) ) ) = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
23 7 15 19 21 22 syl31anc 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> ( ( -oo (,) ( ( x + 1 ) / ( 2 ^ n ) ) ) \ ( -oo (,) ( x / ( 2 ^ n ) ) ) ) = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
24 brsigarn 
 |-  BrSiga e. ( sigAlgebra ` RR )
25 elrnsiga 
 |-  ( BrSiga e. ( sigAlgebra ` RR ) -> BrSiga e. U. ran sigAlgebra )
26 24 25 ax-mp 
 |-  BrSiga e. U. ran sigAlgebra
27 retop 
 |-  ( topGen ` ran (,) ) e. Top
28 iooretop 
 |-  ( -oo (,) ( ( x + 1 ) / ( 2 ^ n ) ) ) e. ( topGen ` ran (,) )
29 elsigagen 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( -oo (,) ( ( x + 1 ) / ( 2 ^ n ) ) ) e. ( topGen ` ran (,) ) ) -> ( -oo (,) ( ( x + 1 ) / ( 2 ^ n ) ) ) e. ( sigaGen ` ( topGen ` ran (,) ) ) )
30 27 28 29 mp2an 
 |-  ( -oo (,) ( ( x + 1 ) / ( 2 ^ n ) ) ) e. ( sigaGen ` ( topGen ` ran (,) ) )
31 df-brsiga 
 |-  BrSiga = ( sigaGen ` ( topGen ` ran (,) ) )
32 30 31 eleqtrri 
 |-  ( -oo (,) ( ( x + 1 ) / ( 2 ^ n ) ) ) e. BrSiga
33 iooretop 
 |-  ( -oo (,) ( x / ( 2 ^ n ) ) ) e. ( topGen ` ran (,) )
34 elsigagen 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( -oo (,) ( x / ( 2 ^ n ) ) ) e. ( topGen ` ran (,) ) ) -> ( -oo (,) ( x / ( 2 ^ n ) ) ) e. ( sigaGen ` ( topGen ` ran (,) ) ) )
35 27 33 34 mp2an 
 |-  ( -oo (,) ( x / ( 2 ^ n ) ) ) e. ( sigaGen ` ( topGen ` ran (,) ) )
36 35 31 eleqtrri 
 |-  ( -oo (,) ( x / ( 2 ^ n ) ) ) e. BrSiga
37 difelsiga 
 |-  ( ( BrSiga e. U. ran sigAlgebra /\ ( -oo (,) ( ( x + 1 ) / ( 2 ^ n ) ) ) e. BrSiga /\ ( -oo (,) ( x / ( 2 ^ n ) ) ) e. BrSiga ) -> ( ( -oo (,) ( ( x + 1 ) / ( 2 ^ n ) ) ) \ ( -oo (,) ( x / ( 2 ^ n ) ) ) ) e. BrSiga )
38 26 32 36 37 mp3an 
 |-  ( ( -oo (,) ( ( x + 1 ) / ( 2 ^ n ) ) ) \ ( -oo (,) ( x / ( 2 ^ n ) ) ) ) e. BrSiga
39 23 38 eqeltrrdi 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) e. BrSiga )
40 39 adantr 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) e. BrSiga )
41 5 40 eqeltrd 
 |-  ( ( ( x e. ZZ /\ n e. ZZ ) /\ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) -> d e. BrSiga )
42 41 ex 
 |-  ( ( x e. ZZ /\ n e. ZZ ) -> ( d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) -> d e. BrSiga ) )
43 42 rexlimivv 
 |-  ( E. x e. ZZ E. n e. ZZ d = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) -> d e. BrSiga )
44 4 43 sylbi 
 |-  ( d e. ran I -> d e. BrSiga )
45 44 ssriv 
 |-  ran I C_ BrSiga