Metamath Proof Explorer

Theorem rrvfinvima

Description: For a real-value random variable X , any open interval in RR is the image of a measurable set. (Contributed by Thierry Arnoux, 25-Jan-2017)

Ref Expression
Hypotheses isrrvv.1 ⊢ φ → P ∈ Prob
rrvvf.1 ⊢ φ → X ∈ RndVar ℝ ⁡ P
Assertion rrvfinvima ⊢ φ → ∀ y ∈ 𝔅 ℝ X -1 y ∈ dom ⁡ P

Proof

Step Hyp Ref Expression
1 isrrvv.1 ⊢ φ → P ∈ Prob
2 rrvvf.1 ⊢ φ → X ∈ RndVar ℝ ⁡ P
3 1 isrrvv ⊢ φ → X ∈ RndVar ℝ ⁡ P ↔ X : ⋃ dom ⁡ P ⟶ ℝ ∧ ∀ y ∈ 𝔅 ℝ X -1 y ∈ dom ⁡ P
4 2 3 mpbid ⊢ φ → X : ⋃ dom ⁡ P ⟶ ℝ ∧ ∀ y ∈ 𝔅 ℝ X -1 y ∈ dom ⁡ P
5 4 simprd ⊢ φ → ∀ y ∈ 𝔅 ℝ X -1 y ∈ dom ⁡ P