Theorem probmeasd

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

	Ref	Expression
Hypothesis	probmeasd.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
Assertion	probmeasd	⊢ ( 𝜑 → 𝑃 ∈ ∪ ran measures )

Proof

Step	Hyp	Ref	Expression
1		probmeasd.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
2		domprobmeas	⊢ ( 𝑃 ∈ Prob → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
3	1 2	syl	⊢ ( 𝜑 → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
4		measbasedom	⊢ ( 𝑃 ∈ ∪ ran measures ↔ 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
5	3 4	sylibr	⊢ ( 𝜑 → 𝑃 ∈ ∪ ran measures )