Metamath Proof Explorer


Theorem bj-imdirval

Description: Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023)

Ref Expression
Hypotheses bj-imdirval.1
|- ( ph -> A e. U )
bj-imdirval.2
|- ( ph -> B e. V )
Assertion bj-imdirval
|- ( ph -> ( A ~P_* B ) = ( r e. ~P ( A X. B ) |-> { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ( r " x ) = y ) } ) )

Proof

Step Hyp Ref Expression
1 bj-imdirval.1
 |-  ( ph -> A e. U )
2 bj-imdirval.2
 |-  ( ph -> B e. V )
3 df-imdir
 |-  ~P_* = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ ( r " x ) = y ) } ) )
4 1 2 3 bj-imdirvallem
 |-  ( ph -> ( A ~P_* B ) = ( r e. ~P ( A X. B ) |-> { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ( r " x ) = y ) } ) )