Metamath Proof Explorer


Theorem rrvfn

Description: A real-valued random variable is a function over the universe. (Contributed by Thierry Arnoux, 25-Jan-2017)

Ref Expression
Hypotheses isrrvv.1
|- ( ph -> P e. Prob )
rrvvf.1
|- ( ph -> X e. ( rRndVar ` P ) )
Assertion rrvfn
|- ( ph -> X Fn U. dom P )

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 ffnd
 |-  ( ph -> X Fn U. dom P )