mbff

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

		Ref	Expression
	Assertion	mbff	$⊢ F \in MblFn \to F : dom F ⟶ ℂ$

Step	Hyp	Ref	Expression
1		ismbf1	$⊢ F \in MblFn \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land \forall x \in ran (.) ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol))$
2	1	simplbi	$⊢ F \in MblFn \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
3		cnex	$⊢ ℂ \in V$
4		reex	$⊢ ℝ \in V$
5	3 4	elpm2	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℝ) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq ℝ)$
6	5	simplbi	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℝ) \to F : dom F ⟶ ℂ$
7	2 6	syl	$⊢ F \in MblFn \to F : dom F ⟶ ℂ$

Metamath Proof Explorer