Theorem rfovfvfvd

Description: Value of the operator, ( A O B ) , which maps between relations and functions for relations between base sets, A and B , relation R , and left element X . (Contributed by RP, 25-Apr-2021)

	Ref	Expression
Hypotheses	rfovd.rf	|- O = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> ( x e. a |-> { y e. b | x r y } ) ) )
	rfovd.a	|- ( ph -> A e. V )
	rfovd.b	|- ( ph -> B e. W )
	rfovfvd.r	|- ( ph -> R e. ~P ( A X. B ) )
	rfovfvd.f	|- F = ( A O B )
	rfovfvfvd.x	|- ( ph -> X e. A )
	rfovfvfvd.g	|- G = ( F ` R )
Assertion	rfovfvfvd	|- ( ph -> ( G ` X ) = { y e. B | X R y } )

Proof

Step	Hyp	Ref	Expression
1		rfovd.rf	|- O = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> ( x e. a |-> { y e. b | x r y } ) ) )
2		rfovd.a	|- ( ph -> A e. V )
3		rfovd.b	|- ( ph -> B e. W )
4		rfovfvd.r	|- ( ph -> R e. ~P ( A X. B ) )
5		rfovfvd.f	|- F = ( A O B )
6		rfovfvfvd.x	|- ( ph -> X e. A )
7		rfovfvfvd.g	|- G = ( F ` R )
8	1 2 3 4 5	rfovfvd	|- ( ph -> ( F ` R ) = ( x e. A |-> { y e. B | x R y } ) )
9	7 8	syl5eq	|- ( ph -> G = ( x e. A |-> { y e. B | x R y } ) )
10		breq1	|- ( x = X -> ( x R y <-> X R y ) )
11	10	rabbidv	|- ( x = X -> { y e. B | x R y } = { y e. B | X R y } )
12	11	adantl	|- ( ( ph /\ x = X ) -> { y e. B | x R y } = { y e. B | X R y } )
13		rabexg	|- ( B e. W -> { y e. B | X R y } e. _V )
14	3 13	syl	|- ( ph -> { y e. B | X R y } e. _V )
15	9 12 6 14	fvmptd	|- ( ph -> ( G ` X ) = { y e. B | X R y } )