Theorem orvccel

Description: If the relation produces closed 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 )
	orvccel.5	|- ( ph -> { y e. U. J | y R A } e. ( Clsd ` J ) )
Assertion	orvccel	|- ( 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		orvccel.5	|- ( ph -> { y e. U. J | y R A } e. ( Clsd ` 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		cldssbrsiga	|- ( J e. Top -> ( Clsd ` J ) C_ ( sigaGen ` J ) )
9	2 8	syl	|- ( ph -> ( Clsd ` 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 )