Metamath Proof Explorer

Theorem probtot

Description: The probability of the universe set is 1. Second axiom of Kolmogorov. (Contributed by Thierry Arnoux, 8-Dec-2016)

Ref Expression
Assertion probtot 
|- ( P e. Prob -> ( P ` U. dom P ) = 1 )

Proof

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