Theorem probtotrnd

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

	Ref	Expression
Hypothesis	probmeasd.1	$$⊢\phi \to P\in \mathrm{Prob}$$
Assertion	probtotrnd	$$⊢\phi \to P\left(\bigcup \mathrm{dom}P\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		probmeasd.1	$$⊢\phi \to P\in \mathrm{Prob}$$
2	1	unveldomd	$$⊢\phi \to \bigcup \mathrm{dom}P\in \mathrm{dom}P$$
3	1 2	probvalrnd	$$⊢\phi \to P\left(\bigcup \mathrm{dom}P\right)\in ℝ$$