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 )