Metamath Proof Explorer

Theorem measfrge0

Description: A measure is a function over its base to the positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016)

Ref Expression
Assertion measfrge0 
|- ( M e. ( measures ` S ) -> M : S --> ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 measbase 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
2 ismeas 
 |-  ( S e. U. ran sigAlgebra -> ( M e. ( measures ` S ) <-> ( M : S --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ _om /\ Disj_ x e. y x ) -> ( M ` U. y ) = sum* x e. y ( M ` x ) ) ) ) )
3 1 2 syl 
 |-  ( M e. ( measures ` S ) -> ( M e. ( measures ` S ) <-> ( M : S --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ _om /\ Disj_ x e. y x ) -> ( M ` U. y ) = sum* x e. y ( M ` x ) ) ) ) )
4 3 ibi 
 |-  ( M e. ( measures ` S ) -> ( M : S --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ _om /\ Disj_ x e. y x ) -> ( M ` U. y ) = sum* x e. y ( M ` x ) ) ) )
5 4 simp1d 
 |-  ( M e. ( measures ` S ) -> M : S --> ( 0 [,] +oo ) )