Theorem orvcoel

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

	Ref	Expression
Hypotheses	orvccel.1	|- ( ph -> S e. U. ran sigAlgebra )
	orvccel.2	|- ( ph -> J e. Top )
	orvccel.3	|- ( ph -> X e. ( S MblFnM ( sigaGen ` J ) ) )
	orvccel.4	|- ( ph -> A e. V )
	orvcoel.5	|- ( ph -> { y e. U. J | y R A } e. J )
Assertion	orvcoel	|- ( ph -> ( X oRVC R A ) e. S )

Proof

Step	Hyp	Ref	Expression
1		orvccel.1	|- ( ph -> S e. U. ran sigAlgebra )
2		orvccel.2	|- ( ph -> J e. Top )
3		orvccel.3	|- ( ph -> X e. ( S MblFnM ( sigaGen ` J ) ) )
4		orvccel.4	|- ( ph -> A e. V )
5		orvcoel.5	|- ( ph -> { y e. U. J | y R A } e. J )
6	1 2 3 4	orvcval4	|- ( ph -> ( X oRVC R A ) = ( `' X " { y e. U. J | y R A } ) )
7	2	sgsiga	|- ( ph -> ( sigaGen ` J ) e. U. ran sigAlgebra )
8		sssigagen	|- ( J e. Top -> J C_ ( sigaGen ` J ) )
9	2 8	syl	|- ( ph -> J C_ ( sigaGen ` J ) )
10	9 5	sseldd	|- ( ph -> { y e. U. J | y R A } e. ( sigaGen ` J ) )
11	1 7 3 10	mbfmcnvima	|- ( ph -> ( `' X " { y e. U. J | y R A } ) e. S )
12	6 11	eqeltrd	|- ( ph -> ( X oRVC R A ) e. S )