Definition df-imdir

Description: Definition of the functionalized direct image, which maps a binary relation between two given sets to its associated direct image relation. (Contributed by BJ, 16-Dec-2023)

	Ref	Expression
Assertion	df-imdir	Could not format assertion : No typesetting found for |- ~P_* = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ ( r " x ) = y ) } ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cimdir	Could not format ~P_* : No typesetting found for class ~P_* with typecode class
1		va	$$setvara$$
2		cvv	$$class\mathrm{V}$$
3		vb	$$setvarb$$
4		vr	$$setvarr$$
5	1	cv	$$setvara$$
6	3	cv	$$setvarb$$
7	5 6	cxp	$$class\left(a\times b\right)$$
8	7	cpw	$$class𝒫\left(a\times b\right)$$
9		vx	$$setvarx$$
10		vy	$$setvary$$
11	9	cv	$$setvarx$$
12	11 5	wss	$$wffx\subseteq a$$
13	10	cv	$$setvary$$
14	13 6	wss	$$wffy\subseteq b$$
15	12 14	wa	$$wff\left(x\subseteq a\wedge y\subseteq b\right)$$
16	4	cv	$$setvarr$$
17	16 11	cima	$$classr\left[x\right]$$
18	17 13	wceq	$$wffr\left[x\right]=y$$
19	15 18	wa	$$wff\left(\left(x\subseteq a\wedge y\subseteq b\right)\wedge r\left[x\right]=y\right)$$
20	19 9 10	copab	$$class\left\{⟨x,y⟩|\left(\left(x\subseteq a\wedge y\subseteq b\right)\wedge r\left[x\right]=y\right)\right\}$$
21	4 8 20	cmpt	$$class\left(r\in 𝒫\left(a\times b\right)⟼\left\{⟨x,y⟩|\left(\left(x\subseteq a\wedge y\subseteq b\right)\wedge r\left[x\right]=y\right)\right\}\right)$$
22	1 3 2 2 21	cmpo	$$class\left(a\in \mathrm{V},b\in \mathrm{V}⟼\left(r\in 𝒫\left(a\times b\right)⟼\left\{⟨x,y⟩|\left(\left(x\subseteq a\wedge y\subseteq b\right)\wedge r\left[x\right]=y\right)\right\}\right)\right)$$
23	0 22	wceq	Could not format ~P_* = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ ( r " x ) = y ) } ) ) : No typesetting found for wff ~P_* = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ ( r " x ) = y ) } ) ) with typecode wff