Metamath Proof Explorer


Theorem rrvrnss

Description: The range of a random variable as a subset of RR . (Contributed by Thierry Arnoux, 6-Feb-2017)

Ref Expression
Hypotheses isrrvv.1
|- ( ph -> P e. Prob )
rrvvf.1
|- ( ph -> X e. ( rRndVar ` P ) )
Assertion rrvrnss
|- ( ph -> ran X C_ RR )

Proof

Step Hyp Ref Expression
1 isrrvv.1
 |-  ( ph -> P e. Prob )
2 rrvvf.1
 |-  ( ph -> X e. ( rRndVar ` P ) )
3 1 2 rrvvf
 |-  ( ph -> X : U. dom P --> RR )
4 3 frnd
 |-  ( ph -> ran X C_ RR )