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∈𝒫Sy≼ω∧Disjx∈yx→M⁡⋃y=∑*x∈yM⁡x
3 1 2 syl ⊢M∈measures⁡S→M∈measures⁡S↔M:S⟶0+∞∧M⁡∅=0∧∀y∈𝒫Sy≼ω∧Disjx∈yx→M⁡⋃y=∑*x∈yM⁡x
4 3 ibi ⊢M∈measures⁡S→M:S⟶0+∞∧M⁡∅=0∧∀y∈𝒫Sy≼ω∧Disjx∈yx→M⁡⋃y=∑*x∈yM⁡x
5 4 simp1d ⊢M∈measures⁡S→M:S⟶0+∞