Theorem domprobmeas

Description: A probability measure is a measure on its domain. (Contributed by Thierry Arnoux, 23-Dec-2016)

	Ref	Expression
Assertion	domprobmeas	$$⊢P\in \mathrm{Prob}\to P\in \mathrm{measures}\left(\mathrm{dom}P\right)$$

Proof

Step	Hyp	Ref	Expression
1		elprob	$$⊢P\in \mathrm{Prob}\leftrightarrow \left(P\in \bigcup \mathrm{ran}\mathrm{measures}\wedge P\left(\bigcup \mathrm{dom}P\right)=1\right)$$
2	1	simplbi	$$⊢P\in \mathrm{Prob}\to P\in \bigcup \mathrm{ran}\mathrm{measures}$$
3		measbasedom	$$⊢P\in \bigcup \mathrm{ran}\mathrm{measures}\leftrightarrow P\in \mathrm{measures}\left(\mathrm{dom}P\right)$$
4	2 3	sylib	$$⊢P\in \mathrm{Prob}\to P\in \mathrm{measures}\left(\mathrm{dom}P\right)$$