Metamath Proof Explorer

Theorem mbff

Description: A measurable function is a function into the complex numbers. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion mbff ⊢ F ∈ MblFn → F : dom ⁡ F ⟶ ℂ

Proof

Step Hyp Ref Expression
1 ismbf1 ⊢ F ∈ MblFn ↔ F ∈ ℂ ↑ 𝑝𝑚 ℝ ∧ ∀ x ∈ ran ⁡ . ℜ ∘ F -1 x ∈ dom ⁡ vol ∧ ℑ ∘ F -1 x ∈ dom ⁡ vol
2 1 simplbi ⊢ F ∈ MblFn → F ∈ ℂ ↑ 𝑝𝑚 ℝ
3 cnex ⊢ ℂ ∈ V
4 reex ⊢ ℝ ∈ V
5 3 4 elpm2 ⊢ F ∈ ℂ ↑ 𝑝𝑚 ℝ ↔ F : dom ⁡ F ⟶ ℂ ∧ dom ⁡ F ⊆ ℝ
6 5 simplbi ⊢ F ∈ ℂ ↑ 𝑝𝑚 ℝ → F : dom ⁡ F ⟶ ℂ
7 2 6 syl ⊢ F ∈ MblFn → F : dom ⁡ F ⟶ ℂ