Theorem bj-imdirval2

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

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

Proof

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