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	|- ( ph -> P e. Prob )
	orrvccel.2	|- ( ph -> X e. ( rRndVar ` P ) )
	orrvccel.4	|- ( ph -> A e. V )
Assertion	orrvcval4	|- ( ph -> ( X oRVC R A ) = ( `' X " { y e. RR | y R A } ) )

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		domprobsiga	|- ( P e. Prob -> dom P e. U. ran sigAlgebra )
5	1 4	syl	|- ( ph -> dom P e. U. ran sigAlgebra )
6		retop	|- ( topGen ` ran (,) ) e. Top
7	6	a1i	|- ( ph -> ( topGen ` ran (,) ) e. Top )
8	1	rrvmbfm	|- ( ph -> ( X e. ( rRndVar ` P ) <-> X e. ( dom P MblFnM BrSiga ) ) )
9	2 8	mpbid	|- ( ph -> X e. ( dom P MblFnM BrSiga ) )
10		df-brsiga	|- BrSiga = ( sigaGen ` ( topGen ` ran (,) ) )
11	10	oveq2i	|- ( dom P MblFnM BrSiga ) = ( dom P MblFnM ( sigaGen ` ( topGen ` ran (,) ) ) )
12	9 11	eleqtrdi	|- ( ph -> X e. ( dom P MblFnM ( sigaGen ` ( topGen ` ran (,) ) ) ) )
13	5 7 12 3	orvcval4	|- ( ph -> ( X oRVC R A ) = ( `' X " { y e. U. ( topGen ` ran (,) ) | y R A } ) )
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	imaeq2i	|- ( `' X " { y e. RR | y R A } ) = ( `' X " { y e. U. ( topGen ` ran (,) ) | y R A } )
18	13 17	eqtr4di	|- ( ph -> ( X oRVC R A ) = ( `' X " { y e. RR | y R A } ) )