Theorem rfovd

Description: Value of the operator, ( A O B ) , which maps between relations and functions for relations between base sets, A and B . (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 )
Assertion	rfovd	|- ( ph -> ( A O B ) = ( r e. ~P ( A X. B ) |-> ( 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	1	a1i	|- ( ph -> O = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> ( x e. a |-> { y e. b | x r y } ) ) ) )
5		xpeq12	|- ( ( a = A /\ b = B ) -> ( a X. b ) = ( A X. B ) )
6	5	pweqd	|- ( ( a = A /\ b = B ) -> ~P ( a X. b ) = ~P ( A X. B ) )
7		simpl	|- ( ( a = A /\ b = B ) -> a = A )
8		rabeq	|- ( b = B -> { y e. b | x r y } = { y e. B | x r y } )
9	8	adantl	|- ( ( a = A /\ b = B ) -> { y e. b | x r y } = { y e. B | x r y } )
10	7 9	mpteq12dv	|- ( ( a = A /\ b = B ) -> ( x e. a |-> { y e. b | x r y } ) = ( x e. A |-> { y e. B | x r y } ) )
11	6 10	mpteq12dv	|- ( ( a = A /\ b = B ) -> ( r e. ~P ( a X. b ) |-> ( x e. a |-> { y e. b | x r y } ) ) = ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) )
12	11	adantl	|- ( ( ph /\ ( a = A /\ b = B ) ) -> ( r e. ~P ( a X. b ) |-> ( x e. a |-> { y e. b | x r y } ) ) = ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) )
13	2	elexd	|- ( ph -> A e. _V )
14	3	elexd	|- ( ph -> B e. _V )
15	2 3	xpexd	|- ( ph -> ( A X. B ) e. _V )
16		pwexg	|- ( ( A X. B ) e. _V -> ~P ( A X. B ) e. _V )
17		mptexg	|- ( ~P ( A X. B ) e. _V -> ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) e. _V )
18	15 16 17	3syl	|- ( ph -> ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) e. _V )
19	4 12 13 14 18	ovmpod	|- ( ph -> ( A O B ) = ( r e. ~P ( A X. B ) |-> ( x e. A |-> { y e. B | x r y } ) ) )