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 ⊢ 𝐽 = ( 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 )