Theorem i1fmbf

Description: Simple functions are measurable. (Contributed by Mario Carneiro, 18-Jun-2014)

	Ref	Expression
Assertion	i1fmbf	$$⊢F\in \mathrm{dom}{\int }^1\to F\in MblFn$$

Proof

Step	Hyp	Ref	Expression
1		isi1f	$$⊢F\in \mathrm{dom}{\int }^1\leftrightarrow \left(F\in MblFn\wedge \left(F:ℝ⟶ℝ\wedge \mathrm{ran}F\in \mathrm{Fin}\wedge vol\left(F^{-1}\left[ℝ\setminus \left\{0\right\}\right]\right)\in ℝ\right)\right)$$
2	1	simplbi	$$⊢F\in \mathrm{dom}{\int }^1\to F\in MblFn$$