Theorem bj-imdirval3

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

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

Proof

Step	Hyp	Ref	Expression
1		bj-imdirval3.exa	$$⊢\phi \to A\in U$$
2		bj-imdirval3.exb	$$⊢\phi \to B\in V$$
3		bj-imdirval3.arg	$$⊢\phi \to R\subseteq A\times B$$
4	1 2 3	bj-imdirval2	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 |-
5	4	breqd	Could not format ( ph -> ( X ( ( A ~P_* B ) ` R ) Y <-> X { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) } Y ) ) : No typesetting found for |- ( ph -> ( X ( ( A ~P_* B ) ` R ) Y <-> X { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) } Y ) ) with typecode |-
6		brabv	$$⊢X\left\{⟨x,y⟩|\left(\left(x\subseteq A\wedge y\subseteq B\right)\wedge R\left[x\right]=y\right)\right\}Y\to \left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)$$
7	5 6	syl6bi	Could not format ( ph -> ( X ( ( A ~P_* B ) ` R ) Y -> ( X e. _V /\ Y e. _V ) ) ) : No typesetting found for |- ( ph -> ( X ( ( A ~P_* B ) ` R ) Y -> ( X e. _V /\ Y e. _V ) ) ) with typecode |-
8	7	pm4.71rd	Could not format ( ph -> ( X ( ( A ~P_* B ) ` R ) Y <-> ( ( X e. _V /\ Y e. _V ) /\ X ( ( A ~P_* B ) ` R ) Y ) ) ) : No typesetting found for |- ( ph -> ( X ( ( A ~P_* B ) ` R ) Y <-> ( ( X e. _V /\ Y e. _V ) /\ X ( ( A ~P_* B ) ` R ) Y ) ) ) with typecode |-
9		simpl	$$⊢\left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\to X\in \mathrm{V}$$
10	9	adantl	$$⊢\left(\phi \wedge \left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\right)\to X\in \mathrm{V}$$
11		simpr	$$⊢\left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\to Y\in \mathrm{V}$$
12	11	adantl	$$⊢\left(\phi \wedge \left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\right)\to Y\in \mathrm{V}$$
13	4	adantr	Could not format ( ( ph /\ ( X e. _V /\ Y e. _V ) ) -> ( ( A ~P_* B ) ` R ) = { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) } ) : No typesetting found for |- ( ( ph /\ ( X e. _V /\ Y e. _V ) ) -> ( ( A ~P_* B ) ` R ) = { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) } ) with typecode |-
14		simpl	$$⊢\left(x=X\wedge y=Y\right)\to x=X$$
15	14	sseq1d	$$⊢\left(x=X\wedge y=Y\right)\to \left(x\subseteq A\leftrightarrow X\subseteq A\right)$$
16		simpr	$$⊢\left(x=X\wedge y=Y\right)\to y=Y$$
17	16	sseq1d	$$⊢\left(x=X\wedge y=Y\right)\to \left(y\subseteq B\leftrightarrow Y\subseteq B\right)$$
18	15 17	anbi12d	$$⊢\left(x=X\wedge y=Y\right)\to \left(\left(x\subseteq A\wedge y\subseteq B\right)\leftrightarrow \left(X\subseteq A\wedge Y\subseteq B\right)\right)$$
19		imaeq2	$$⊢x=X\to R\left[x\right]=R\left[X\right]$$
20		id	$$⊢y=Y\to y=Y$$
21	19 20	eqeqan12d	$$⊢\left(x=X\wedge y=Y\right)\to \left(R\left[x\right]=y\leftrightarrow R\left[X\right]=Y\right)$$
22	18 21	anbi12d	$$⊢\left(x=X\wedge y=Y\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)$$
23	22	adantl	$$⊢\left(\left(\phi \wedge \left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\right)\wedge \left(x=X\wedge y=Y\right)\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)$$
24	10 12 13 23	brabd	Could not format ( ( ph /\ ( X e. _V /\ Y e. _V ) ) -> ( X ( ( A ~P_* B ) ` R ) Y <-> ( ( X C_ A /\ Y C_ B ) /\ ( R " X ) = Y ) ) ) : No typesetting found for |- ( ( ph /\ ( X e. _V /\ Y e. _V ) ) -> ( X ( ( A ~P_* B ) ` R ) Y <-> ( ( X C_ A /\ Y C_ B ) /\ ( R " X ) = Y ) ) ) with typecode |-
25	24	pm5.32da	Could not format ( ph -> ( ( ( X e. _V /\ Y e. _V ) /\ X ( ( A ~P_* B ) ` R ) Y ) <-> ( ( X e. _V /\ Y e. _V ) /\ ( ( X C_ A /\ Y C_ B ) /\ ( R " X ) = Y ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( X e. _V /\ Y e. _V ) /\ X ( ( A ~P_* B ) ` R ) Y ) <-> ( ( X e. _V /\ Y e. _V ) /\ ( ( X C_ A /\ Y C_ B ) /\ ( R " X ) = Y ) ) ) ) with typecode |-
26		simpr	$$⊢\left(\left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\wedge \left(\left(X\subseteq A\wedge Y\subseteq B\right)\wedge R\left[X\right]=Y\right)\right)\to \left(\left(X\subseteq A\wedge Y\subseteq B\right)\wedge R\left[X\right]=Y\right)$$
27	1	adantr	$$⊢\left(\phi \wedge X\subseteq A\right)\to A\in U$$
28		simpr	$$⊢\left(\phi \wedge X\subseteq A\right)\to X\subseteq A$$
29	27 28	ssexd	$$⊢\left(\phi \wedge X\subseteq A\right)\to X\in \mathrm{V}$$
30	29	ex	$$⊢\phi \to \left(X\subseteq A\to X\in \mathrm{V}\right)$$
31	2	adantr	$$⊢\left(\phi \wedge Y\subseteq B\right)\to B\in V$$
32		simpr	$$⊢\left(\phi \wedge Y\subseteq B\right)\to Y\subseteq B$$
33	31 32	ssexd	$$⊢\left(\phi \wedge Y\subseteq B\right)\to Y\in \mathrm{V}$$
34	33	ex	$$⊢\phi \to \left(Y\subseteq B\to Y\in \mathrm{V}\right)$$
35	30 34	anim12d	$$⊢\phi \to \left(\left(X\subseteq A\wedge Y\subseteq B\right)\to \left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\right)$$
36	35	adantrd	$$⊢\phi \to \left(\left(\left(X\subseteq A\wedge Y\subseteq B\right)\wedge R\left[X\right]=Y\right)\to \left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\right)$$
37	36	ancrd	$$⊢\phi \to \left(\left(\left(X\subseteq A\wedge Y\subseteq B\right)\wedge R\left[X\right]=Y\right)\to \left(\left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\wedge \left(\left(X\subseteq A\wedge Y\subseteq B\right)\wedge R\left[X\right]=Y\right)\right)\right)$$
38	26 37	impbid2	$$⊢\phi \to \left(\left(\left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\wedge \left(\left(X\subseteq A\wedge Y\subseteq B\right)\wedge R\left[X\right]=Y\right)\right)\leftrightarrow \left(\left(X\subseteq A\wedge Y\subseteq B\right)\wedge R\left[X\right]=Y\right)\right)$$
39	8 25 38	3bitrd	Could not format ( ph -> ( X ( ( A ~P_* B ) ` R ) Y <-> ( ( X C_ A /\ Y C_ B ) /\ ( R " X ) = Y ) ) ) : No typesetting found for |- ( ph -> ( X ( ( A ~P_* B ) ` R ) Y <-> ( ( X C_ A /\ Y C_ B ) /\ ( R " X ) = Y ) ) ) with typecode |-