Description: A real-valued random variable is a measurable function from its sample space to the Borel sigma-algebra. (Contributed by Thierry Arnoux, 25-Jan-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | isrrvv.1 | |- ( ph -> P e. Prob ) |
|
| Assertion | rrvmbfm | |- ( ph -> ( X e. ( rRndVar ` P ) <-> X e. ( dom P MblFnM BrSiga ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | isrrvv.1 | |- ( ph -> P e. Prob ) |
|
| 2 | dmeq | |- ( p = P -> dom p = dom P ) |
|
| 3 | 2 | oveq1d | |- ( p = P -> ( dom p MblFnM BrSiga ) = ( dom P MblFnM BrSiga ) ) |
| 4 | df-rrv | |- rRndVar = ( p e. Prob |-> ( dom p MblFnM BrSiga ) ) |
|
| 5 | ovex | |- ( dom P MblFnM BrSiga ) e. _V |
|
| 6 | 3 4 5 | fvmpt | |- ( P e. Prob -> ( rRndVar ` P ) = ( dom P MblFnM BrSiga ) ) |
| 7 | 1 6 | syl | |- ( ph -> ( rRndVar ` P ) = ( dom P MblFnM BrSiga ) ) |
| 8 | 7 | eleq2d | |- ( ph -> ( X e. ( rRndVar ` P ) <-> X e. ( dom P MblFnM BrSiga ) ) ) |