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 \in Prob \to dom P \in ⋃ ran sigAlgebra$

Step	Hyp	Ref	Expression
1		domprobmeas	$⊢ P \in Prob \to P \in measures (dom P)$
2		measbase	$⊢ P \in measures (dom P) \to dom P \in ⋃ ran sigAlgebra$
3	1 2	syl	$⊢ P \in Prob \to dom P \in ⋃ ran sigAlgebra$