Theorem bj-iminvval2

Description: Value of the functionalized inverse image. (Contributed by BJ, 23-May-2024)

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

Proof

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