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 measures S M : S 0 +∞

Proof

Step Hyp Ref Expression
1 measbase M measures S S ran sigAlgebra
2 ismeas S ran sigAlgebra M measures S M : S 0 +∞ M = 0 y 𝒫 S y ω Disj x y x M y = * x y M x
3 1 2 syl M measures S M measures S M : S 0 +∞ M = 0 y 𝒫 S y ω Disj x y x M y = * x y M x
4 3 ibi M measures S M : S 0 +∞ M = 0 y 𝒫 S y ω Disj x y x M y = * x y M x
5 4 simp1d M measures S M : S 0 +∞