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

Metamath Proof Explorer

Theorem mbfimaopn

Description: The preimage of any open set (in the complex topology) under a measurable function is measurable. (See also cncombf , which explains why A e. dom vol is too weak a condition for this theorem.) (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypothesis mbfimaopn.1 
|- J = ( TopOpen ` CCfld )
Assertion mbfimaopn 
|- ( ( F e. MblFn /\ A e. J ) -> ( `' F " A ) e. dom vol )

Proof

Step Hyp Ref Expression
1 mbfimaopn.1 
 |-  J = ( TopOpen ` CCfld )
2 oveq1 
 |-  ( t = x -> ( t + ( _i x. w ) ) = ( x + ( _i x. w ) ) )
3 oveq2 
 |-  ( w = y -> ( _i x. w ) = ( _i x. y ) )
4 3 oveq2d 
 |-  ( w = y -> ( x + ( _i x. w ) ) = ( x + ( _i x. y ) ) )
5 2 4 cbvmpov 
 |-  ( t e. RR , w e. RR |-> ( t + ( _i x. w ) ) ) = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )
6 eqid 
 |-  ( (,) " ( QQ X. QQ ) ) = ( (,) " ( QQ X. QQ ) )
7 eqid 
 |-  ran ( x e. ( (,) " ( QQ X. QQ ) ) , y e. ( (,) " ( QQ X. QQ ) ) |-> ( x X. y ) ) = ran ( x e. ( (,) " ( QQ X. QQ ) ) , y e. ( (,) " ( QQ X. QQ ) ) |-> ( x X. y ) )
8 1 5 6 7 mbfimaopnlem 
 |-  ( ( F e. MblFn /\ A e. J ) -> ( `' F " A ) e. dom vol )