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	|- ( ph -> P e. Prob )
	orrvccel.2	|- ( ph -> X e. ( rRndVar ` P ) )
	orrvccel.4	|- ( ph -> A e. V )
	orrvcoel.5	|- ( ph -> { y e. RR | y R A } e. ( topGen ` ran (,) ) )
Assertion	orrvcoel	|- ( 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		orrvcoel.5	|- ( ph -> { y e. RR | y R A } e. ( 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. ( topGen ` ran (,) ) )
18	6 8 13 3 17	orvcoel	|- ( ph -> ( X oRVC R A ) e. dom P )