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 ∈ 𝒫 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 simp2d ⊢ M ∈ measures ⁡ S → M ⁡ ∅ = 0