Theorem probmeasd

Description: A probability measure is a measure. (Contributed by Thierry Arnoux, 2-Feb-2017)

	Ref	Expression
Hypothesis	probmeasd.1	$$⊢\phi \to P\in \mathrm{Prob}$$
Assertion	probmeasd	$$⊢\phi \to P\in \bigcup \mathrm{ran}\mathrm{measures}$$

Proof

Step	Hyp	Ref	Expression
1		probmeasd.1	$$⊢\phi \to P\in \mathrm{Prob}$$
2		domprobmeas	$$⊢P\in \mathrm{Prob}\to P\in \mathrm{measures}\left(\mathrm{dom}P\right)$$
3	1 2	syl	$$⊢\phi \to P\in \mathrm{measures}\left(\mathrm{dom}P\right)$$
4		measbasedom	$$⊢P\in \bigcup \mathrm{ran}\mathrm{measures}\leftrightarrow P\in \mathrm{measures}\left(\mathrm{dom}P\right)$$
5	3 4	sylibr	$$⊢\phi \to P\in \bigcup \mathrm{ran}\mathrm{measures}$$