Metamath Proof Explorer

Theorem mbfdmssre

Description: The domain of a measurable function is a subset of the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021)

		Ref	Expression
	Assertion	mbfdmssre	$⊢ F \in MblFn \to dom F \subseteq ℝ$

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		elpmi2	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℝ) \to dom F \subseteq ℝ$
4	2 3	syl	$⊢ F \in MblFn \to dom F \subseteq ℝ$