Theorem rfovfvd

Description: Value of the operator, ( A O B ) , which maps between relations and functions for relations between base sets, A and B , and relation R . (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 )
Assertion	rfovfvd	|- ( ph -> ( F ` R ) = ( x e. A |-> { 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	1 2 3	rfovd	|- ( ph -> ( A O B ) = ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) )
7	5 6	eqtrid	|- ( ph -> F = ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) )
8		breq	|- ( r = R -> ( x r y <-> x R y ) )
9	8	rabbidv	|- ( r = R -> { y e. B | x r y } = { y e. B | x R y } )
10	9	mpteq2dv	|- ( r = R -> ( x e. A |-> { y e. B | x r y } ) = ( x e. A |-> { y e. B | x R y } ) )
11	10	adantl	|- ( ( ph /\ r = R ) -> ( x e. A |-> { y e. B | x r y } ) = ( x e. A |-> { y e. B | x R y } ) )
12	2	mptexd	|- ( ph -> ( x e. A |-> { y e. B | x R y } ) e. _V )
13	7 11 4 12	fvmptd	|- ( ph -> ( F ` R ) = ( x e. A |-> { y e. B | x R y } ) )