Metamath Proof Explorer
Description: The range of a random variable as a subset of RR . (Contributed by Thierry Arnoux, 6-Feb-2017)
|
|
Ref |
Expression |
|
Hypotheses |
isrrvv.1 |
⊢ ( 𝜑 → 𝑃 ∈ Prob ) |
|
|
rrvvf.1 |
⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ) |
|
Assertion |
rrvrnss |
⊢ ( 𝜑 → ran 𝑋 ⊆ ℝ ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
isrrvv.1 |
⊢ ( 𝜑 → 𝑃 ∈ Prob ) |
2 |
|
rrvvf.1 |
⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ) |
3 |
1 2
|
rrvvf |
⊢ ( 𝜑 → 𝑋 : ∪ dom 𝑃 ⟶ ℝ ) |
4 |
3
|
frnd |
⊢ ( 𝜑 → ran 𝑋 ⊆ ℝ ) |