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 )