Metamath Proof Explorer

Theorem mea0

Description: The measure of the empty set is always 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis mea0.1 ⊢ φ → M ∈ Meas
Assertion mea0 ⊢ φ → M ⁡ ∅ = 0

Proof

Step Hyp Ref Expression
1 mea0.1 ⊢ φ → M ∈ Meas
2 ismea ⊢ M ∈ Meas ↔ M : dom ⁡ M ⟶ 0 +∞ ∧ dom ⁡ M ∈ SAlg ∧ M ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 dom ⁡ M x ≼ ω ∧ Disj y ∈ x y → M ⁡ ⋃ x = sum^ ⁡ M ↾ x
3 1 2 sylib ⊢ φ → M : dom ⁡ M ⟶ 0 +∞ ∧ dom ⁡ M ∈ SAlg ∧ M ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 dom ⁡ M x ≼ ω ∧ Disj y ∈ x y → M ⁡ ⋃ x = sum^ ⁡ M ↾ x
4 3 simplrd ⊢ φ → M ⁡ ∅ = 0