Metamath Proof Explorer

Theorem sxbrsigalem5

Description: First direction for sxbrsiga . (Contributed by Thierry Arnoux, 22-Sep-2017) (Revised by Thierry Arnoux, 11-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 ) ) ) )
dya2ioc.2 
|- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )
Assertion sxbrsigalem5 
|- ( sigaGen ` ( J tX J ) ) C_ ( BrSiga sX 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 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 br2base 
 |-  U. ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) = ( RR X. RR )
6 4 5 eqtr4i 
 |-  U. ran R = U. ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) )
7 brsigarn 
 |-  BrSiga e. ( sigAlgebra ` RR )
8 7 elexi 
 |-  BrSiga e. _V
9 8 8 mpoex 
 |-  ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) e. _V
10 9 rnex 
 |-  ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) e. _V
11 1 2 dya2icobrsiga 
 |-  ran I C_ BrSiga
12 11 sseli 
 |-  ( u e. ran I -> u e. BrSiga )
13 11 sseli 
 |-  ( v e. ran I -> v e. BrSiga )
14 12 13 anim12i 
 |-  ( ( u e. ran I /\ v e. ran I ) -> ( u e. BrSiga /\ v e. BrSiga ) )
15 14 anim1i 
 |-  ( ( ( u e. ran I /\ v e. ran I ) /\ g = ( u X. v ) ) -> ( ( u e. BrSiga /\ v e. BrSiga ) /\ g = ( u X. v ) ) )
16 15 ssoprab2i 
 |-  { <. <. u , v >. , g >. | ( ( u e. ran I /\ v e. ran I ) /\ g = ( u X. v ) ) } C_ { <. <. u , v >. , g >. | ( ( u e. BrSiga /\ v e. BrSiga ) /\ g = ( u X. v ) ) }
17 df-mpo 
 |-  ( u e. ran I , v e. ran I |-> ( u X. v ) ) = { <. <. u , v >. , g >. | ( ( u e. ran I /\ v e. ran I ) /\ g = ( u X. v ) ) }
18 3 17 eqtri 
 |-  R = { <. <. u , v >. , g >. | ( ( u e. ran I /\ v e. ran I ) /\ g = ( u X. v ) ) }
19 xpeq1 
 |-  ( e = u -> ( e X. f ) = ( u X. f ) )
20 xpeq2 
 |-  ( f = v -> ( u X. f ) = ( u X. v ) )
21 19 20 cbvmpov 
 |-  ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) = ( u e. BrSiga , v e. BrSiga |-> ( u X. v ) )
22 df-mpo 
 |-  ( u e. BrSiga , v e. BrSiga |-> ( u X. v ) ) = { <. <. u , v >. , g >. | ( ( u e. BrSiga /\ v e. BrSiga ) /\ g = ( u X. v ) ) }
23 21 22 eqtri 
 |-  ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) = { <. <. u , v >. , g >. | ( ( u e. BrSiga /\ v e. BrSiga ) /\ g = ( u X. v ) ) }
24 16 18 23 3sstr4i 
 |-  R C_ ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) )
25 rnss 
 |-  ( R C_ ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) -> ran R C_ ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) )
26 24 25 ax-mp 
 |-  ran R C_ ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) )
27 sssigagen2 
 |-  ( ( ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) e. _V /\ ran R C_ ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) ) -> ran R C_ ( sigaGen ` ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) ) )
28 10 26 27 mp2an 
 |-  ran R C_ ( sigaGen ` ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) )
29 sigagenss2 
 |-  ( ( U. ran R = U. ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) /\ ran R C_ ( sigaGen ` ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) ) /\ ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) e. _V ) -> ( sigaGen ` ran R ) C_ ( sigaGen ` ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) ) )
30 6 28 10 29 mp3an 
 |-  ( sigaGen ` ran R ) C_ ( sigaGen ` ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) )
31 1 2 3 sxbrsigalem4 
 |-  ( sigaGen ` ( J tX J ) ) = ( sigaGen ` ran R )
32 eqid 
 |-  ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) = ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) )
33 32 sxval 
 |-  ( ( BrSiga e. ( sigAlgebra ` RR ) /\ BrSiga e. ( sigAlgebra ` RR ) ) -> ( BrSiga sX BrSiga ) = ( sigaGen ` ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) ) )
34 7 7 33 mp2an 
 |-  ( BrSiga sX BrSiga ) = ( sigaGen ` ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) )
35 30 31 34 3sstr4i 
 |-  ( sigaGen ` ( J tX J ) ) C_ ( BrSiga sX BrSiga )