Metamath Proof Explorer
Description: A real-valued random variable is a function over the universe.
(Contributed by Thierry Arnoux, 25-Jan-2017)
|
|
Ref |
Expression |
|
Hypotheses |
isrrvv.1 |
⊢ ( 𝜑 → 𝑃 ∈ Prob ) |
|
|
rrvvf.1 |
⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ) |
|
Assertion |
rrvfn |
⊢ ( 𝜑 → 𝑋 Fn ∪ dom 𝑃 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
isrrvv.1 |
⊢ ( 𝜑 → 𝑃 ∈ Prob ) |
2 |
|
rrvvf.1 |
⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ) |
3 |
1 2
|
rrvvf |
⊢ ( 𝜑 → 𝑋 : ∪ dom 𝑃 ⟶ ℝ ) |
4 |
3
|
ffnd |
⊢ ( 𝜑 → 𝑋 Fn ∪ dom 𝑃 ) |