Theorem probmeasd

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

	Ref	Expression
Hypothesis	probmeasd.1	|- ( ph -> P e. Prob )
Assertion	probmeasd	|- ( ph -> P e. U. ran measures )

Proof

Step	Hyp	Ref	Expression
1		probmeasd.1	|- ( ph -> P e. Prob )
2		domprobmeas	|- ( P e. Prob -> P e. ( measures ` dom P ) )
3	1 2	syl	|- ( ph -> P e. ( measures ` dom P ) )
4		measbasedom	|- ( P e. U. ran measures <-> P e. ( measures ` dom P ) )
5	3 4	sylibr	|- ( ph -> P e. U. ran measures )