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	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion	mbfimaopn	⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) → ( ◡ 𝐹 “ 𝐴 ) ∈ dom vol )

Proof

Step	Hyp	Ref	Expression
1		mbfimaopn.1	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		oveq1	⊢ ( 𝑡 = 𝑥 → ( 𝑡 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑤 ) ) )
3		oveq2	⊢ ( 𝑤 = 𝑦 → ( i · 𝑤 ) = ( i · 𝑦 ) )
4	3	oveq2d	⊢ ( 𝑤 = 𝑦 → ( 𝑥 + ( i · 𝑤 ) ) = ( 𝑥 + ( i · 𝑦 ) ) )
5	2 4	cbvmpov	⊢ ( 𝑡 ∈ ℝ , 𝑤 ∈ ℝ ↦ ( 𝑡 + ( i · 𝑤 ) ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) )
6		eqid	⊢ ( (,) “ ( ℚ × ℚ ) ) = ( (,) “ ( ℚ × ℚ ) )
7		eqid	⊢ ran ( 𝑥 ∈ ( (,) “ ( ℚ × ℚ ) ) , 𝑦 ∈ ( (,) “ ( ℚ × ℚ ) ) ↦ ( 𝑥 × 𝑦 ) ) = ran ( 𝑥 ∈ ( (,) “ ( ℚ × ℚ ) ) , 𝑦 ∈ ( (,) “ ( ℚ × ℚ ) ) ↦ ( 𝑥 × 𝑦 ) )
8	1 5 6 7	mbfimaopnlem	⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽 ) → ( ◡ 𝐹 “ 𝐴 ) ∈ dom vol )