Metamath Proof Explorer

Theorem i1fmbf

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

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

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