Metamath Proof Explorer

Theorem measfn

Description: A measure is a function on its base sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017)

Ref Expression
Assertion measfn 
|- ( M e. ( measures ` S ) -> M Fn S )

Proof

Step Hyp Ref Expression
1 measfrge0 
 |-  ( M e. ( measures ` S ) -> M : S --> ( 0 [,] +oo ) )
2 1 ffnd 
 |-  ( M e. ( measures ` S ) -> M Fn S )