Metamath Proof Explorer

Theorem domprobmeas

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

Ref Expression
Assertion domprobmeas 
|- ( P e. Prob -> P e. ( measures ` dom P ) )

Proof

Step Hyp Ref Expression
1 elprob 
 |-  ( P e. Prob <-> ( P e. U. ran measures /\ ( P ` U. dom P ) = 1 ) )
2 1 simplbi 
 |-  ( P e. Prob -> P e. U. ran measures )
3 measbasedom 
 |-  ( P e. U. ran measures <-> P e. ( measures ` dom P ) )
4 2 3 sylib 
 |-  ( P e. Prob -> P e. ( measures ` dom P ) )