Metamath Proof Explorer

Theorem domprobsiga

Description: The domain of a probability measure is a sigma-algebra. (Contributed by Thierry Arnoux, 23-Dec-2016)

Ref Expression
Assertion domprobsiga ⊢ P ∈ Prob → dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra

Proof

Step Hyp Ref Expression
1 domprobmeas ⊢ P ∈ Prob → P ∈ measures ⁡ dom ⁡ P
2 measbase ⊢ P ∈ measures ⁡ dom ⁡ P → dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra
3 1 2 syl ⊢ P ∈ Prob → dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra