Step |
Hyp |
Ref |
Expression |
1 |
|
oveq1 |
|- ( x = z -> ( x / ( 2 ^ y ) ) = ( z / ( 2 ^ y ) ) ) |
2 |
|
oveq1 |
|- ( x = z -> ( x + 1 ) = ( z + 1 ) ) |
3 |
2
|
oveq1d |
|- ( x = z -> ( ( x + 1 ) / ( 2 ^ y ) ) = ( ( z + 1 ) / ( 2 ^ y ) ) ) |
4 |
1 3
|
opeq12d |
|- ( x = z -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. = <. ( z / ( 2 ^ y ) ) , ( ( z + 1 ) / ( 2 ^ y ) ) >. ) |
5 |
|
oveq2 |
|- ( y = w -> ( 2 ^ y ) = ( 2 ^ w ) ) |
6 |
5
|
oveq2d |
|- ( y = w -> ( z / ( 2 ^ y ) ) = ( z / ( 2 ^ w ) ) ) |
7 |
5
|
oveq2d |
|- ( y = w -> ( ( z + 1 ) / ( 2 ^ y ) ) = ( ( z + 1 ) / ( 2 ^ w ) ) ) |
8 |
6 7
|
opeq12d |
|- ( y = w -> <. ( z / ( 2 ^ y ) ) , ( ( z + 1 ) / ( 2 ^ y ) ) >. = <. ( z / ( 2 ^ w ) ) , ( ( z + 1 ) / ( 2 ^ w ) ) >. ) |
9 |
4 8
|
cbvmpov |
|- ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) = ( z e. ZZ , w e. NN0 |-> <. ( z / ( 2 ^ w ) ) , ( ( z + 1 ) / ( 2 ^ w ) ) >. ) |
10 |
9
|
opnmbllem |
|- ( A e. ( topGen ` ran (,) ) -> A e. dom vol ) |