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 e. Prob -> dom P e. U. ran sigAlgebra )

Proof

Step Hyp Ref Expression
1 domprobmeas 
 |-  ( P e. Prob -> P e. ( measures ` dom P ) )
2 measbase 
 |-  ( P e. ( measures ` dom P ) -> dom P e. U. ran sigAlgebra )
3 1 2 syl 
 |-  ( P e. Prob -> dom P e. U. ran sigAlgebra )