Metamath Proof Explorer


Theorem orrvccel

Description: If the relation produces closed sets, preimage maps are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Hypotheses orrvccel.1
|- ( ph -> P e. Prob )
orrvccel.2
|- ( ph -> X e. ( rRndVar ` P ) )
orrvccel.4
|- ( ph -> A e. V )
orrvccel.5
|- ( ph -> { y e. RR | y R A } e. ( Clsd ` ( topGen ` ran (,) ) ) )
Assertion orrvccel
|- ( ph -> ( X oRVC R A ) e. dom P )

Proof

Step Hyp Ref Expression
1 orrvccel.1
 |-  ( ph -> P e. Prob )
2 orrvccel.2
 |-  ( ph -> X e. ( rRndVar ` P ) )
3 orrvccel.4
 |-  ( ph -> A e. V )
4 orrvccel.5
 |-  ( ph -> { y e. RR | y R A } e. ( Clsd ` ( topGen ` ran (,) ) ) )
5 domprobsiga
 |-  ( P e. Prob -> dom P e. U. ran sigAlgebra )
6 1 5 syl
 |-  ( ph -> dom P e. U. ran sigAlgebra )
7 retop
 |-  ( topGen ` ran (,) ) e. Top
8 7 a1i
 |-  ( ph -> ( topGen ` ran (,) ) e. Top )
9 1 rrvmbfm
 |-  ( ph -> ( X e. ( rRndVar ` P ) <-> X e. ( dom P MblFnM BrSiga ) ) )
10 2 9 mpbid
 |-  ( ph -> X e. ( dom P MblFnM BrSiga ) )
11 df-brsiga
 |-  BrSiga = ( sigaGen ` ( topGen ` ran (,) ) )
12 11 oveq2i
 |-  ( dom P MblFnM BrSiga ) = ( dom P MblFnM ( sigaGen ` ( topGen ` ran (,) ) ) )
13 10 12 eleqtrdi
 |-  ( ph -> X e. ( dom P MblFnM ( sigaGen ` ( topGen ` ran (,) ) ) ) )
14 uniretop
 |-  RR = U. ( topGen ` ran (,) )
15 rabeq
 |-  ( RR = U. ( topGen ` ran (,) ) -> { y e. RR | y R A } = { y e. U. ( topGen ` ran (,) ) | y R A } )
16 14 15 ax-mp
 |-  { y e. RR | y R A } = { y e. U. ( topGen ` ran (,) ) | y R A }
17 16 4 eqeltrrid
 |-  ( ph -> { y e. U. ( topGen ` ran (,) ) | y R A } e. ( Clsd ` ( topGen ` ran (,) ) ) )
18 6 8 13 3 17 orvccel
 |-  ( ph -> ( X oRVC R A ) e. dom P )