Theorem mbff

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

	Ref	Expression
Assertion	mbff	⊢ ( 𝐹 ∈ MblFn → 𝐹 : dom 𝐹 ⟶ ℂ )

Proof

Step	Hyp	Ref	Expression
1		ismbf1	⊢ ( 𝐹 ∈ MblFn ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) )
2	1	simplbi	⊢ ( 𝐹 ∈ MblFn → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
3		cnex	⊢ ℂ ∈ V
4		reex	⊢ ℝ ∈ V
5	3 4	elpm2	⊢ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℝ ) )
6	5	simplbi	⊢ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) → 𝐹 : dom 𝐹 ⟶ ℂ )
7	2 6	syl	⊢ ( 𝐹 ∈ MblFn → 𝐹 : dom 𝐹 ⟶ ℂ )