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 ( 𝑀 ran measures → dom 𝑀 ran sigAlgebra )

Proof

Step Hyp Ref Expression
1 isrnmeas ( 𝑀 ran measures → ( dom 𝑀 ran sigAlgebra ∧ ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 ) → ( 𝑀 𝑥 ) = Σ* 𝑦𝑥 ( 𝑀𝑦 ) ) ) ) )
2 1 simpld ( 𝑀 ran measures → dom 𝑀 ran sigAlgebra )