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	⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ⊆ ℝ )

Proof

Step	Hyp	Ref	Expression
1		ismbf1	⊢ ( 𝐹 ∈ MblFn ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) )
2	1	simplbi	⊢ ( 𝐹 ∈ MblFn → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
3		elpmi2	⊢ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) → dom 𝐹 ⊆ ℝ )
4	2 3	syl	⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ⊆ ℝ )