Metamath Proof Explorer


Theorem i1fmbf

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

Ref Expression
Assertion i1fmbf
|- ( F e. dom S.1 -> F e. MblFn )

Proof

Step Hyp Ref Expression
1 isi1f
 |-  ( F e. dom S.1 <-> ( F e. MblFn /\ ( F : RR --> RR /\ ran F e. Fin /\ ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) ) )
2 1 simplbi
 |-  ( F e. dom S.1 -> F e. MblFn )