Metamath Proof Explorer

Theorem sxbrsigalem1

Description: The Borel algebra on ( RR X. RR ) is a subset of the sigma-algebra generated by the dyadic closed-below, open-above rectangular subsets of ( RR X. RR ) . This is a step of the proof of Proposition 1.1.5 of Cohn p. 4. (Contributed by Thierry Arnoux, 17-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 sxbrsigalem1 
|- ( sigaGen ` ( J tX J ) ) C_ ( 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 dya2iocucvr 
 |-  U. ran R = ( RR X. RR )
5 retop 
 |-  ( topGen ` ran (,) ) e. Top
6 1 5 eqeltri 
 |-  J e. Top
7 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
8 1 unieqi 
 |-  U. J = U. ( topGen ` ran (,) )
9 7 8 eqtr4i 
 |-  RR = U. J
10 6 6 9 9 txunii 
 |-  ( RR X. RR ) = U. ( J tX J )
11 4 10 eqtr2i 
 |-  U. ( J tX J ) = U. ran R
12 1 2 3 dya2iocuni 
 |-  ( x e. ( J tX J ) -> E. y e. ~P ran R U. y = x )
13 simpr 
 |-  ( ( y e. ~P ran R /\ U. y = x ) -> U. y = x )
14 1 2 3 dya2iocct 
 |-  ran R ~<_ _om
15 ctex 
 |-  ( ran R ~<_ _om -> ran R e. _V )
16 14 15 mp1i 
 |-  ( y e. ~P ran R -> ran R e. _V )
17 elpwi 
 |-  ( y e. ~P ran R -> y C_ ran R )
18 ssct 
 |-  ( ( y C_ ran R /\ ran R ~<_ _om ) -> y ~<_ _om )
19 17 14 18 sylancl 
 |-  ( y e. ~P ran R -> y ~<_ _om )
20 elsigagen2 
 |-  ( ( ran R e. _V /\ y C_ ran R /\ y ~<_ _om ) -> U. y e. ( sigaGen ` ran R ) )
21 16 17 19 20 syl3anc 
 |-  ( y e. ~P ran R -> U. y e. ( sigaGen ` ran R ) )
22 21 adantr 
 |-  ( ( y e. ~P ran R /\ U. y = x ) -> U. y e. ( sigaGen ` ran R ) )
23 13 22 eqeltrrd 
 |-  ( ( y e. ~P ran R /\ U. y = x ) -> x e. ( sigaGen ` ran R ) )
24 23 rexlimiva 
 |-  ( E. y e. ~P ran R U. y = x -> x e. ( sigaGen ` ran R ) )
25 12 24 syl 
 |-  ( x e. ( J tX J ) -> x e. ( sigaGen ` ran R ) )
26 25 ssriv 
 |-  ( J tX J ) C_ ( sigaGen ` ran R )
27 14 15 ax-mp 
 |-  ran R e. _V
28 sigagenss2 
 |-  ( ( U. ( J tX J ) = U. ran R /\ ( J tX J ) C_ ( sigaGen ` ran R ) /\ ran R e. _V ) -> ( sigaGen ` ( J tX J ) ) C_ ( sigaGen ` ran R ) )
29 11 26 27 28 mp3an 
 |-  ( sigaGen ` ( J tX J ) ) C_ ( sigaGen ` ran R )