Metamath Proof Explorer


Theorem rrvvf

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

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

Proof

Step Hyp Ref Expression
1 isrrvv.1
 |-  ( ph -> P e. Prob )
2 rrvvf.1
 |-  ( ph -> X e. ( rRndVar ` P ) )
3 1 isrrvv
 |-  ( ph -> ( X e. ( rRndVar ` P ) <-> ( X : U. dom P --> RR /\ A. y e. BrSiga ( `' X " y ) e. dom P ) ) )
4 2 3 mpbid
 |-  ( ph -> ( X : U. dom P --> RR /\ A. y e. BrSiga ( `' X " y ) e. dom P ) )
5 4 simpld
 |-  ( ph -> X : U. dom P --> RR )