Metamath Proof Explorer


Theorem orrvcoel

Description: If the relation produces open sets, preimage maps of a random variable are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Hypotheses orrvccel.1 ( 𝜑𝑃 ∈ Prob )
orrvccel.2 ( 𝜑𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
orrvccel.4 ( 𝜑𝐴𝑉 )
orrvcoel.5 ( 𝜑 → { 𝑦 ∈ ℝ ∣ 𝑦 𝑅 𝐴 } ∈ ( topGen ‘ ran (,) ) )
Assertion orrvcoel ( 𝜑 → ( 𝑋RV/𝑐 𝑅 𝐴 ) ∈ dom 𝑃 )

Proof

Step Hyp Ref Expression
1 orrvccel.1 ( 𝜑𝑃 ∈ Prob )
2 orrvccel.2 ( 𝜑𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3 orrvccel.4 ( 𝜑𝐴𝑉 )
4 orrvcoel.5 ( 𝜑 → { 𝑦 ∈ ℝ ∣ 𝑦 𝑅 𝐴 } ∈ ( topGen ‘ ran (,) ) )
5 domprobsiga ( 𝑃 ∈ Prob → dom 𝑃 ran sigAlgebra )
6 1 5 syl ( 𝜑 → dom 𝑃 ran sigAlgebra )
7 retop ( topGen ‘ ran (,) ) ∈ Top
8 7 a1i ( 𝜑 → ( topGen ‘ ran (,) ) ∈ Top )
9 1 rrvmbfm ( 𝜑 → ( 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ↔ 𝑋 ∈ ( dom 𝑃 MblFnM 𝔅 ) ) )
10 2 9 mpbid ( 𝜑𝑋 ∈ ( dom 𝑃 MblFnM 𝔅 ) )
11 df-brsiga 𝔅 = ( sigaGen ‘ ( topGen ‘ ran (,) ) )
12 11 oveq2i ( dom 𝑃 MblFnM 𝔅 ) = ( dom 𝑃 MblFnM ( sigaGen ‘ ( topGen ‘ ran (,) ) ) )
13 10 12 eleqtrdi ( 𝜑𝑋 ∈ ( dom 𝑃 MblFnM ( sigaGen ‘ ( topGen ‘ ran (,) ) ) ) )
14 uniretop ℝ = ( topGen ‘ ran (,) )
15 rabeq ( ℝ = ( topGen ‘ ran (,) ) → { 𝑦 ∈ ℝ ∣ 𝑦 𝑅 𝐴 } = { 𝑦 ( topGen ‘ ran (,) ) ∣ 𝑦 𝑅 𝐴 } )
16 14 15 ax-mp { 𝑦 ∈ ℝ ∣ 𝑦 𝑅 𝐴 } = { 𝑦 ( topGen ‘ ran (,) ) ∣ 𝑦 𝑅 𝐴 }
17 16 4 eqeltrrid ( 𝜑 → { 𝑦 ( topGen ‘ ran (,) ) ∣ 𝑦 𝑅 𝐴 } ∈ ( topGen ‘ ran (,) ) )
18 6 8 13 3 17 orvcoel ( 𝜑 → ( 𝑋RV/𝑐 𝑅 𝐴 ) ∈ dom 𝑃 )