Theorem domprobsiga

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

	Ref	Expression
Assertion	domprobsiga	⊢ ( 𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra )

Proof

Step	Hyp	Ref	Expression
1		domprobmeas	⊢ ( 𝑃 ∈ Prob → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
2		measbase	⊢ ( 𝑃 ∈ ( measures ‘ dom 𝑃 ) → dom 𝑃 ∈ ∪ ran sigAlgebra )
3	1 2	syl	⊢ ( 𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra )