Theorem domprobmeas

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

	Ref	Expression
Assertion	domprobmeas	⊢ ( 𝑃 ∈ Prob → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		elprob	⊢ ( 𝑃 ∈ Prob ↔ ( 𝑃 ∈ ∪ ran measures ∧ ( 𝑃 ‘ ∪ dom 𝑃 ) = 1 ) )
2	1	simplbi	⊢ ( 𝑃 ∈ Prob → 𝑃 ∈ ∪ ran measures )
3		measbasedom	⊢ ( 𝑃 ∈ ∪ ran measures ↔ 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
4	2 3	sylib	⊢ ( 𝑃 ∈ Prob → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )