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 ⁡ M x ≼ ω ∧ Disj y ∈ x y → M ⁡ ⋃ x = ∑ * y ∈ x M ⁡ y
2 1 simpld ⊢ M ∈ ⋃ ran ⁡ measures → dom ⁡ M ∈ ⋃ ran ⁡ sigAlgebra