Theorem bj-imdirval2

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

	Ref	Expression
Hypotheses	bj-imdirval2.exa	|- ( ph -> A e. U )
	bj-imdirval2.exb	|- ( ph -> B e. V )
	bj-imdirval2.arg	|- ( ph -> R C_ ( A X. B ) )
Assertion	bj-imdirval2	|- ( ph -> ( ( A ~P_* B ) ` R ) = { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) } )

Proof

Step	Hyp	Ref	Expression
1		bj-imdirval2.exa	|- ( ph -> A e. U )
2		bj-imdirval2.exb	|- ( ph -> B e. V )
3		bj-imdirval2.arg	|- ( ph -> R C_ ( A X. B ) )
4	1 2	bj-imdirval	|- ( ph -> ( A ~P_* B ) = ( r e. ~P ( A X. B ) |-> { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ( r " x ) = y ) } ) )
5		simpr	|- ( ( ph /\ r = R ) -> r = R )
6	5	imaeq1d	|- ( ( ph /\ r = R ) -> ( r " x ) = ( R " x ) )
7	6	eqeq1d	|- ( ( ph /\ r = R ) -> ( ( r " x ) = y <-> ( R " x ) = y ) )
8	7	anbi2d	|- ( ( ph /\ r = R ) -> ( ( ( x C_ A /\ y C_ B ) /\ ( r " x ) = y ) <-> ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) ) )
9	8	opabbidv	|- ( ( ph /\ r = R ) -> { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ( r " x ) = y ) } = { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) } )
10	1 2	xpexd	|- ( ph -> ( A X. B ) e. _V )
11	10 3	sselpwd	|- ( ph -> R e. ~P ( A X. B ) )
12	1 2	bj-imdirval2lem	|- ( ph -> { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) } e. _V )
13	4 9 11 12	fvmptd	|- ( ph -> ( ( A ~P_* B ) ` R ) = { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) } )