Theorem probtotrnd

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

	Ref	Expression
Hypothesis	probmeasd.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
Assertion	probtotrnd	⊢ ( 𝜑 → ( 𝑃 ‘ ∪ dom 𝑃 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		probmeasd.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
2	1	unveldomd	⊢ ( 𝜑 → ∪ dom 𝑃 ∈ dom 𝑃 )
3	1 2	probvalrnd	⊢ ( 𝜑 → ( 𝑃 ‘ ∪ dom 𝑃 ) ∈ ℝ )