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 ( 𝜑𝑃 ∈ Prob )
Assertion isrrvv ( 𝜑 → ( 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ↔ ( 𝑋 : dom 𝑃 ⟶ ℝ ∧ ∀ 𝑦 ∈ 𝔅 ( 𝑋𝑦 ) ∈ dom 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 isrrvv.1 ( 𝜑𝑃 ∈ Prob )
2 1 rrvmbfm ( 𝜑 → ( 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ↔ 𝑋 ∈ ( dom 𝑃 MblFnM 𝔅 ) ) )
3 domprobsiga ( 𝑃 ∈ Prob → dom 𝑃 ran sigAlgebra )
4 1 3 syl ( 𝜑 → dom 𝑃 ran sigAlgebra )
5 brsigarn 𝔅 ∈ ( sigAlgebra ‘ ℝ )
6 elrnsiga ( 𝔅 ∈ ( sigAlgebra ‘ ℝ ) → 𝔅 ran sigAlgebra )
7 5 6 mp1i ( 𝜑 → 𝔅 ran sigAlgebra )
8 4 7 ismbfm ( 𝜑 → ( 𝑋 ∈ ( dom 𝑃 MblFnM 𝔅 ) ↔ ( 𝑋 ∈ ( 𝔅m dom 𝑃 ) ∧ ∀ 𝑦 ∈ 𝔅 ( 𝑋𝑦 ) ∈ dom 𝑃 ) ) )
9 unibrsiga 𝔅 = ℝ
10 9 oveq1i ( 𝔅m dom 𝑃 ) = ( ℝ ↑m dom 𝑃 )
11 10 eleq2i ( 𝑋 ∈ ( 𝔅m dom 𝑃 ) ↔ 𝑋 ∈ ( ℝ ↑m dom 𝑃 ) )
12 reex ℝ ∈ V
13 4 uniexd ( 𝜑 dom 𝑃 ∈ V )
14 elmapg ( ( ℝ ∈ V ∧ dom 𝑃 ∈ V ) → ( 𝑋 ∈ ( ℝ ↑m dom 𝑃 ) ↔ 𝑋 : dom 𝑃 ⟶ ℝ ) )
15 12 13 14 sylancr ( 𝜑 → ( 𝑋 ∈ ( ℝ ↑m dom 𝑃 ) ↔ 𝑋 : dom 𝑃 ⟶ ℝ ) )
16 11 15 syl5bb ( 𝜑 → ( 𝑋 ∈ ( 𝔅m dom 𝑃 ) ↔ 𝑋 : dom 𝑃 ⟶ ℝ ) )
17 16 anbi1d ( 𝜑 → ( ( 𝑋 ∈ ( 𝔅m dom 𝑃 ) ∧ ∀ 𝑦 ∈ 𝔅 ( 𝑋𝑦 ) ∈ dom 𝑃 ) ↔ ( 𝑋 : dom 𝑃 ⟶ ℝ ∧ ∀ 𝑦 ∈ 𝔅 ( 𝑋𝑦 ) ∈ dom 𝑃 ) ) )
18 2 8 17 3bitrd ( 𝜑 → ( 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ↔ ( 𝑋 : dom 𝑃 ⟶ ℝ ∧ ∀ 𝑦 ∈ 𝔅 ( 𝑋𝑦 ) ∈ dom 𝑃 ) ) )