Metamath Proof Explorer

Theorem isrrvv

Description: Elementhood to the set of real-valued random variables with respect to the probability P . (Contributed by Thierry Arnoux, 25-Jan-2017)

Ref Expression
Hypothesis isrrvv.1 ⊢ φ → P ∈ Prob
Assertion isrrvv ⊢ φ → X ∈ RndVar ℝ ⁡ P ↔ X : ⋃ dom ⁡ P ⟶ ℝ ∧ ∀ y ∈ 𝔅 ℝ X -1 y ∈ dom ⁡ P

Proof

Step Hyp Ref Expression
1 isrrvv.1 ⊢ φ → P ∈ Prob
2 1 rrvmbfm ⊢ φ → X ∈ RndVar ℝ ⁡ P ↔ X ∈ dom ⁡ P MblFn μ 𝔅 ℝ
3 domprobsiga ⊢ P ∈ Prob → dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra
4 1 3 syl ⊢ φ → dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra
5 brsigarn ⊢ 𝔅 ℝ ∈ sigAlgebra ⁡ ℝ
6 elrnsiga ⊢ 𝔅 ℝ ∈ sigAlgebra ⁡ ℝ → 𝔅 ℝ ∈ ⋃ ran ⁡ sigAlgebra
7 5 6 mp1i ⊢ φ → 𝔅 ℝ ∈ ⋃ ran ⁡ sigAlgebra
8 4 7 ismbfm ⊢ φ → X ∈ dom ⁡ P MblFn μ 𝔅 ℝ ↔ X ∈ ⋃ 𝔅 ℝ ⋃ dom ⁡ P ∧ ∀ y ∈ 𝔅 ℝ X -1 y ∈ dom ⁡ P
9 unibrsiga ⊢ ⋃ 𝔅 ℝ = ℝ
10 9 oveq1i ⊢ ⋃ 𝔅 ℝ ⋃ dom ⁡ P = ℝ ⋃ dom ⁡ P
11 10 eleq2i ⊢ X ∈ ⋃ 𝔅 ℝ ⋃ dom ⁡ P ↔ X ∈ ℝ ⋃ dom ⁡ P
12 reex ⊢ ℝ ∈ V
13 4 uniexd ⊢ φ → ⋃ dom ⁡ P ∈ V
14 elmapg ⊢ ℝ ∈ V ∧ ⋃ dom ⁡ P ∈ V → X ∈ ℝ ⋃ dom ⁡ P ↔ X : ⋃ dom ⁡ P ⟶ ℝ
15 12 13 14 sylancr ⊢ φ → X ∈ ℝ ⋃ dom ⁡ P ↔ X : ⋃ dom ⁡ P ⟶ ℝ
16 11 15 syl5bb ⊢ φ → X ∈ ⋃ 𝔅 ℝ ⋃ dom ⁡ P ↔ X : ⋃ dom ⁡ P ⟶ ℝ
17 16 anbi1d ⊢ φ → X ∈ ⋃ 𝔅 ℝ ⋃ dom ⁡ P ∧ ∀ y ∈ 𝔅 ℝ X -1 y ∈ dom ⁡ P ↔ X : ⋃ dom ⁡ P ⟶ ℝ ∧ ∀ y ∈ 𝔅 ℝ X -1 y ∈ dom ⁡ P
18 2 8 17 3bitrd ⊢ φ → X ∈ RndVar ℝ ⁡ P ↔ X : ⋃ dom ⁡ P ⟶ ℝ ∧ ∀ y ∈ 𝔅 ℝ X -1 y ∈ dom ⁡ P