Theorem bj-iminvval2

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

	Ref	Expression
Hypotheses	bj-iminvval2.exa	$$⊢\phi \to A\in U$$
	bj-iminvval2.exb	$$⊢\phi \to B\in V$$
	bj-iminvval2.arg	$$⊢\phi \to R\subseteq A\times B$$
Assertion	bj-iminvval2	Could not format assertion : No typesetting found for |- ( ph -> ( ( A ~P^* B ) ` R ) = { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ x = ( `' R " y ) ) } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bj-iminvval2.exa	$$⊢\phi \to A\in U$$
2		bj-iminvval2.exb	$$⊢\phi \to B\in V$$
3		bj-iminvval2.arg	$$⊢\phi \to R\subseteq A\times B$$
4	1 2	bj-iminvval	Could not format ( ph -> ( A ~P^* B ) = ( r e. ~P ( A X. B ) |-> { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ x = ( `' r " y ) ) } ) ) : No typesetting found for |- ( ph -> ( A ~P^* B ) = ( r e. ~P ( A X. B ) |-> { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ x = ( `' r " y ) ) } ) ) with typecode |-
5		simpr	$$⊢\left(\phi \wedge r=R\right)\to r=R$$
6	5	cnveqd	$$⊢\left(\phi \wedge r=R\right)\to r^{-1}=R^{-1}$$
7	6	imaeq1d	$$⊢\left(\phi \wedge r=R\right)\to r^{-1}\left[y\right]=R^{-1}\left[y\right]$$
8	7	eqeq2d	$$⊢\left(\phi \wedge r=R\right)\to \left(x=r^{-1}\left[y\right]\leftrightarrow x=R^{-1}\left[y\right]\right)$$
9	8	anbi2d	$$⊢\left(\phi \wedge r=R\right)\to \left(\left(\left(x\subseteq A\wedge y\subseteq B\right)\wedge x=r^{-1}\left[y\right]\right)\leftrightarrow \left(\left(x\subseteq A\wedge y\subseteq B\right)\wedge x=R^{-1}\left[y\right]\right)\right)$$
10	9	opabbidv	$$⊢\left(\phi \wedge r=R\right)\to \left\{⟨x,y⟩|\left(\left(x\subseteq A\wedge y\subseteq B\right)\wedge x=r^{-1}\left[y\right]\right)\right\}=\left\{⟨x,y⟩|\left(\left(x\subseteq A\wedge y\subseteq B\right)\wedge x=R^{-1}\left[y\right]\right)\right\}$$
11	1 2	xpexd	$$⊢\phi \to A\times B\in \mathrm{V}$$
12	11 3	sselpwd	$$⊢\phi \to R\in 𝒫\left(A\times B\right)$$
13	1 2	bj-imdirval2lem	$$⊢\phi \to \left\{⟨x,y⟩|\left(\left(x\subseteq A\wedge y\subseteq B\right)\wedge x=R^{-1}\left[y\right]\right)\right\}\in \mathrm{V}$$
14	4 10 12 13	fvmptd	Could not format ( ph -> ( ( A ~P^* B ) ` R ) = { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ x = ( `' R " y ) ) } ) : No typesetting found for |- ( ph -> ( ( A ~P^* B ) ` R ) = { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ x = ( `' R " y ) ) } ) with typecode |-