Metamath Proof Explorer

Theorem sxbrsigalem4

Description: The Borel algebra on ( RR X. RR ) is generated by the dyadic closed-below, open-above rectangular subsets of ( RR X. RR ) . Proposition 1.1.5 of Cohn p. 4 . Note that the interval used in this formalization are closed-below, open-above instead of open-below, closed-above in the proof as they are ultimately generated by the floor function. (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 sxbrsigalem4 
|- ( sigaGen ` ( J tX J ) ) = ( sigaGen ` ran R )

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 1 2 3 sxbrsigalem1 
 |-  ( sigaGen ` ( J tX J ) ) C_ ( sigaGen ` ran R )
5 1 2 3 sxbrsigalem2 
 |-  ( sigaGen ` ran R ) C_ ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) )
6 1 sxbrsigalem3 
 |-  ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) C_ ( sigaGen ` ( Clsd ` ( J tX J ) ) )
7 5 6 sstri 
 |-  ( sigaGen ` ran R ) C_ ( sigaGen ` ( Clsd ` ( J tX J ) ) )
8 1 tpr2tp 
 |-  ( J tX J ) e. ( TopOn ` ( RR X. RR ) )
9 8 topontopi 
 |-  ( J tX J ) e. Top
10 eqid 
 |-  U. ( J tX J ) = U. ( J tX J )
11 9 10 unicls 
 |-  U. ( Clsd ` ( J tX J ) ) = U. ( J tX J )
12 cldssbrsiga 
 |-  ( ( J tX J ) e. Top -> ( Clsd ` ( J tX J ) ) C_ ( sigaGen ` ( J tX J ) ) )
13 9 12 ax-mp 
 |-  ( Clsd ` ( J tX J ) ) C_ ( sigaGen ` ( J tX J ) )
14 sigagenss2 
 |-  ( ( U. ( Clsd ` ( J tX J ) ) = U. ( J tX J ) /\ ( Clsd ` ( J tX J ) ) C_ ( sigaGen ` ( J tX J ) ) /\ ( J tX J ) e. Top ) -> ( sigaGen ` ( Clsd ` ( J tX J ) ) ) C_ ( sigaGen ` ( J tX J ) ) )
15 11 13 9 14 mp3an 
 |-  ( sigaGen ` ( Clsd ` ( J tX J ) ) ) C_ ( sigaGen ` ( J tX J ) )
16 7 15 sstri 
 |-  ( sigaGen ` ran R ) C_ ( sigaGen ` ( J tX J ) )
17 4 16 eqssi 
 |-  ( sigaGen ` ( J tX J ) ) = ( sigaGen ` ran R )