Metamath Proof Explorer

Theorem dmmeas

Description: The domain of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 19-Feb-2018)

Ref Expression
Assertion dmmeas ⊢M∈⋃ran⁡measures→dom⁡M∈⋃ran⁡sigAlgebra

Proof

Step Hyp Ref Expression
1 isrnmeas ⊢M∈⋃ran⁡measures→dom⁡M∈⋃ran⁡sigAlgebra∧M:dom⁡M⟶0+∞∧M⁡∅=0∧∀x∈𝒫dom⁡Mx≼ω∧Disjy∈xy→M⁡⋃x=∑*y∈xM⁡y
2 1 simpld ⊢M∈⋃ran⁡measures→dom⁡M∈⋃ran⁡sigAlgebra