Metamath Proof Explorer


Theorem orrvcval4

Description: The value of the preimage mapping operator can be restricted to preimages of subsets of RR . (Contributed by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Hypotheses orrvccel.1 ( 𝜑𝑃 ∈ Prob )
orrvccel.2 ( 𝜑𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
orrvccel.4 ( 𝜑𝐴𝑉 )
Assertion orrvcval4 ( 𝜑 → ( 𝑋RV/𝑐 𝑅 𝐴 ) = ( 𝑋 “ { 𝑦 ∈ ℝ ∣ 𝑦 𝑅 𝐴 } ) )

Proof

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