Metamath Proof Explorer

Theorem measvnul

Description: The measure of the empty set is always zero. (Contributed by Thierry Arnoux, 26-Dec-2016)

Ref Expression
Assertion measvnul ⊢M∈measures⁡S→M⁡∅=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 simp2d ⊢M∈measures⁡S→M⁡∅=0