Theorem probtotrnd

Description: The probability of the universe set is finite. (Contributed by Thierry Arnoux, 2-Feb-2017)

	Ref	Expression
Hypothesis	probmeasd.1	|- ( ph -> P e. Prob )
Assertion	probtotrnd	|- ( ph -> ( P ` U. dom P ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		probmeasd.1	|- ( ph -> P e. Prob )
2	1	unveldomd	|- ( ph -> U. dom P e. dom P )
3	1 2	probvalrnd	|- ( ph -> ( P ` U. dom P ) e. RR )