Metamath Proof Explorer

Theorem dya2iocbrsiga

Description: Dyadic intervals are Borel sets of RR . (Contributed by Thierry Arnoux, 22-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 ) ) ) )
Assertion dya2iocbrsiga 
|- ( ( N e. ZZ /\ X e. ZZ ) -> ( X I N ) e. 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 1 2 dya2iocival 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( X I N ) = ( ( X / ( 2 ^ N ) ) [,) ( ( X + 1 ) / ( 2 ^ N ) ) ) )
4 mnfxr 
 |-  -oo e. RR*
5 4 a1i 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> -oo e. RR* )
6 simpr 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> X e. ZZ )
7 6 zred 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> X e. RR )
8 2rp 
 |-  2 e. RR+
9 8 a1i 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> 2 e. RR+ )
10 simpl 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> N e. ZZ )
11 9 10 rpexpcld 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( 2 ^ N ) e. RR+ )
12 7 11 rerpdivcld 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( X / ( 2 ^ N ) ) e. RR )
13 12 rexrd 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( X / ( 2 ^ N ) ) e. RR* )
14 1red 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> 1 e. RR )
15 7 14 readdcld 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( X + 1 ) e. RR )
16 15 11 rerpdivcld 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( ( X + 1 ) / ( 2 ^ N ) ) e. RR )
17 16 rexrd 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( ( X + 1 ) / ( 2 ^ N ) ) e. RR* )
18 mnflt 
 |-  ( ( X / ( 2 ^ N ) ) e. RR -> -oo < ( X / ( 2 ^ N ) ) )
19 12 18 syl 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> -oo < ( X / ( 2 ^ N ) ) )
20 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 ) ) ) )
21 5 13 17 19 20 syl31anc 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( ( -oo (,) ( ( X + 1 ) / ( 2 ^ N ) ) ) \ ( -oo (,) ( X / ( 2 ^ N ) ) ) ) = ( ( X / ( 2 ^ N ) ) [,) ( ( X + 1 ) / ( 2 ^ N ) ) ) )
22 brsigarn 
 |-  BrSiga e. ( sigAlgebra ` RR )
23 elrnsiga 
 |-  ( BrSiga e. ( sigAlgebra ` RR ) -> BrSiga e. U. ran sigAlgebra )
24 22 23 ax-mp 
 |-  BrSiga e. U. ran sigAlgebra
25 retop 
 |-  ( topGen ` ran (,) ) e. Top
26 iooretop 
 |-  ( -oo (,) ( ( X + 1 ) / ( 2 ^ N ) ) ) e. ( topGen ` ran (,) )
27 elsigagen 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( -oo (,) ( ( X + 1 ) / ( 2 ^ N ) ) ) e. ( topGen ` ran (,) ) ) -> ( -oo (,) ( ( X + 1 ) / ( 2 ^ N ) ) ) e. ( sigaGen ` ( topGen ` ran (,) ) ) )
28 25 26 27 mp2an 
 |-  ( -oo (,) ( ( X + 1 ) / ( 2 ^ N ) ) ) e. ( sigaGen ` ( topGen ` ran (,) ) )
29 df-brsiga 
 |-  BrSiga = ( sigaGen ` ( topGen ` ran (,) ) )
30 28 29 eleqtrri 
 |-  ( -oo (,) ( ( X + 1 ) / ( 2 ^ N ) ) ) e. BrSiga
31 iooretop 
 |-  ( -oo (,) ( X / ( 2 ^ N ) ) ) e. ( topGen ` ran (,) )
32 elsigagen 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( -oo (,) ( X / ( 2 ^ N ) ) ) e. ( topGen ` ran (,) ) ) -> ( -oo (,) ( X / ( 2 ^ N ) ) ) e. ( sigaGen ` ( topGen ` ran (,) ) ) )
33 25 31 32 mp2an 
 |-  ( -oo (,) ( X / ( 2 ^ N ) ) ) e. ( sigaGen ` ( topGen ` ran (,) ) )
34 33 29 eleqtrri 
 |-  ( -oo (,) ( X / ( 2 ^ N ) ) ) e. BrSiga
35 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 )
36 24 30 34 35 mp3an 
 |-  ( ( -oo (,) ( ( X + 1 ) / ( 2 ^ N ) ) ) \ ( -oo (,) ( X / ( 2 ^ N ) ) ) ) e. BrSiga
37 21 36 eqeltrrdi 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( ( X / ( 2 ^ N ) ) [,) ( ( X + 1 ) / ( 2 ^ N ) ) ) e. BrSiga )
38 3 37 eqeltrd 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( X I N ) e. BrSiga )