Metamath Proof Explorer

Theorem sxbrsigalem6

Description: First direction for sxbrsiga , same as sxbrsigalem6, dealing with the antecedents. (Contributed by Thierry Arnoux, 10-Oct-2017)

Ref Expression
Hypothesis sxbrsiga.0 
|- J = ( topGen ` ran (,) )
Assertion sxbrsigalem6 
|- ( sigaGen ` ( J tX J ) ) C_ ( BrSiga sX BrSiga )

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 
 |-  J = ( topGen ` ran (,) )
2 oveq1 
 |-  ( a = x -> ( a / ( 2 ^ m ) ) = ( x / ( 2 ^ m ) ) )
3 oveq1 
 |-  ( a = x -> ( a + 1 ) = ( x + 1 ) )
4 3 oveq1d 
 |-  ( a = x -> ( ( a + 1 ) / ( 2 ^ m ) ) = ( ( x + 1 ) / ( 2 ^ m ) ) )
5 2 4 oveq12d 
 |-  ( a = x -> ( ( a / ( 2 ^ m ) ) [,) ( ( a + 1 ) / ( 2 ^ m ) ) ) = ( ( x / ( 2 ^ m ) ) [,) ( ( x + 1 ) / ( 2 ^ m ) ) ) )
6 oveq2 
 |-  ( m = n -> ( 2 ^ m ) = ( 2 ^ n ) )
7 6 oveq2d 
 |-  ( m = n -> ( x / ( 2 ^ m ) ) = ( x / ( 2 ^ n ) ) )
8 6 oveq2d 
 |-  ( m = n -> ( ( x + 1 ) / ( 2 ^ m ) ) = ( ( x + 1 ) / ( 2 ^ n ) ) )
9 7 8 oveq12d 
 |-  ( m = n -> ( ( x / ( 2 ^ m ) ) [,) ( ( x + 1 ) / ( 2 ^ m ) ) ) = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
10 5 9 cbvmpov 
 |-  ( a e. ZZ , m e. ZZ |-> ( ( a / ( 2 ^ m ) ) [,) ( ( a + 1 ) / ( 2 ^ m ) ) ) ) = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
11 eqid 
 |-  ( u e. ran ( a e. ZZ , m e. ZZ |-> ( ( a / ( 2 ^ m ) ) [,) ( ( a + 1 ) / ( 2 ^ m ) ) ) ) , v e. ran ( a e. ZZ , m e. ZZ |-> ( ( a / ( 2 ^ m ) ) [,) ( ( a + 1 ) / ( 2 ^ m ) ) ) ) |-> ( u X. v ) ) = ( u e. ran ( a e. ZZ , m e. ZZ |-> ( ( a / ( 2 ^ m ) ) [,) ( ( a + 1 ) / ( 2 ^ m ) ) ) ) , v e. ran ( a e. ZZ , m e. ZZ |-> ( ( a / ( 2 ^ m ) ) [,) ( ( a + 1 ) / ( 2 ^ m ) ) ) ) |-> ( u X. v ) )
12 1 10 11 sxbrsigalem5 
 |-  ( sigaGen ` ( J tX J ) ) C_ ( BrSiga sX BrSiga )