Theorem orvcval4

Description: The value of the preimage mapping operator can be restricted to preimages in the base set of the topology. Cf. orvcval . (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 )
Assertion	orvcval4	|- ( ph -> ( X oRVC R A ) = ( `' X " { y e. U. J | y R A } ) )

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	3	isanmbfm	|- ( ph -> X e. U. ran MblFnM )
6	5	mbfmfun	|- ( ph -> Fun X )
7	2	sgsiga	|- ( ph -> ( sigaGen ` J ) e. U. ran sigAlgebra )
8	1 7 3	mbfmf	|- ( ph -> X : U. S --> U. ( sigaGen ` J ) )
9		elex	|- ( J e. Top -> J e. _V )
10		unisg	|- ( J e. _V -> U. ( sigaGen ` J ) = U. J )
11	2 9 10	3syl	|- ( ph -> U. ( sigaGen ` J ) = U. J )
12	11	feq3d	|- ( ph -> ( X : U. S --> U. ( sigaGen ` J ) <-> X : U. S --> U. J ) )
13	8 12	mpbid	|- ( ph -> X : U. S --> U. J )
14	13	frnd	|- ( ph -> ran X C_ U. J )
15		fimacnvinrn2	|- ( ( Fun X /\ ran X C_ U. J ) -> ( `' X " { y | y R A } ) = ( `' X " ( { y | y R A } i^i U. J ) ) )
16	6 14 15	syl2anc	|- ( ph -> ( `' X " { y | y R A } ) = ( `' X " ( { y | y R A } i^i U. J ) ) )
17	6 3 4	orvcval	|- ( ph -> ( X oRVC R A ) = ( `' X " { y | y R A } ) )
18		dfrab2	|- { y e. U. J | y R A } = ( { y | y R A } i^i U. J )
19	18	a1i	|- ( ph -> { y e. U. J | y R A } = ( { y | y R A } i^i U. J ) )
20	19	imaeq2d	|- ( ph -> ( `' X " { y e. U. J | y R A } ) = ( `' X " ( { y | y R A } i^i U. J ) ) )
21	16 17 20	3eqtr4d	|- ( ph -> ( X oRVC R A ) = ( `' X " { y e. U. J | y R A } ) )