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 )