Metamath Proof Explorer


Theorem rfovcnvd

Description: Value of the converse of the operator, ( A O B ) , which maps between relations and functions for relations between base sets, A and B . (Contributed by RP, 27-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 )
rfovcnvf1od.f
|- F = ( A O B )
Assertion rfovcnvd
|- ( ph -> `' F = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) )

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 rfovcnvf1od.f
 |-  F = ( A O B )
5 1 2 3 4 rfovcnvf1od
 |-  ( ph -> ( F : ~P ( A X. B ) -1-1-onto-> ( ~P B ^m A ) /\ `' F = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) ) )
6 5 simprd
 |-  ( ph -> `' F = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) )