Theorem probvalrnd

Description: The value of a probability is a real number. (Contributed by Thierry Arnoux, 2-Feb-2017)

	Ref	Expression
Hypotheses	probmeasd.1	$$⊢\phi \to P\in \mathrm{Prob}$$
	probvalrnd.1	$$⊢\phi \to A\in \mathrm{dom}P$$
Assertion	probvalrnd	$$⊢\phi \to P\left(A\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		probmeasd.1	$$⊢\phi \to P\in \mathrm{Prob}$$
2		probvalrnd.1	$$⊢\phi \to A\in \mathrm{dom}P$$
3		unitssre	$$⊢\left[0,1\right]\subseteq ℝ$$
4		prob01	$$⊢\left(P\in \mathrm{Prob}\wedge A\in \mathrm{dom}P\right)\to P\left(A\right)\in \left[0,1\right]$$
5	1 2 4	syl2anc	$$⊢\phi \to P\left(A\right)\in \left[0,1\right]$$
6	3 5	sselid	$$⊢\phi \to P\left(A\right)\in ℝ$$