This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opnmbl

Description: All open sets are measurable. This proof, via dyadmbl and uniioombl , shows that it is possible to avoid choice for measurability of open sets and hence continuous functions, which extends the choice-free consequences of Lebesgue measure considerably farther than would otherwise be possible. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Assertion opnmbl 
|- ( A e. ( topGen ` ran (,) ) -> A e. dom vol )

Proof

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 )