Metamath Proof Explorer

Theorem rfovcnvfvd

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 , evaluated at function G . (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 )
rfovcnvfv.g 
|- ( ph -> G e. ( ~P B ^m A ) )
Assertion rfovcnvfvd 
|- ( ph -> ( `' F ` G ) = { <. x , y >. | ( x e. A /\ y e. ( G ` 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 rfovcnvfv.g 
 |-  ( ph -> G e. ( ~P B ^m A ) )
6 1 2 3 4 rfovcnvd 
 |-  ( ph -> `' F = ( g e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( g ` x ) ) } ) )
7 fveq1 
 |-  ( g = G -> ( g ` x ) = ( G ` x ) )
8 7 eleq2d 
 |-  ( g = G -> ( y e. ( g ` x ) <-> y e. ( G ` x ) ) )
9 8 anbi2d 
 |-  ( g = G -> ( ( x e. A /\ y e. ( g ` x ) ) <-> ( x e. A /\ y e. ( G ` x ) ) ) )
10 9 opabbidv 
 |-  ( g = G -> { <. x , y >. | ( x e. A /\ y e. ( g ` x ) ) } = { <. x , y >. | ( x e. A /\ y e. ( G ` x ) ) } )
11 10 adantl 
 |-  ( ( ph /\ g = G ) -> { <. x , y >. | ( x e. A /\ y e. ( g ` x ) ) } = { <. x , y >. | ( x e. A /\ y e. ( G ` x ) ) } )
12 simprl 
 |-  ( ( ph /\ ( x e. A /\ y e. ( G ` x ) ) ) -> x e. A )
13 elmapi 
 |-  ( G e. ( ~P B ^m A ) -> G : A --> ~P B )
14 13 ffvelcdmda 
 |-  ( ( G e. ( ~P B ^m A ) /\ x e. A ) -> ( G ` x ) e. ~P B )
15 5 14 sylan 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) e. ~P B )
16 15 elpwid 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) C_ B )
17 16 sseld 
 |-  ( ( ph /\ x e. A ) -> ( y e. ( G ` x ) -> y e. B ) )
18 17 impr 
 |-  ( ( ph /\ ( x e. A /\ y e. ( G ` x ) ) ) -> y e. B )
19 2 3 12 18 opabex2 
 |-  ( ph -> { <. x , y >. | ( x e. A /\ y e. ( G ` x ) ) } e. _V )
20 6 11 5 19 fvmptd 
 |-  ( ph -> ( `' F ` G ) = { <. x , y >. | ( x e. A /\ y e. ( G ` x ) ) } )