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	|- ~P_* = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ ( r " x ) = y ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cimdir	|- ~P_*
1		va	|- a
2		cvv	|- _V
3		vb	|- b
4		vr	|- r
5	1	cv	|- a
6	3	cv	|- b
7	5 6	cxp	|- ( a X. b )
8	7	cpw	|- ~P ( a X. b )
9		vx	|- x
10		vy	|- y
11	9	cv	|- x
12	11 5	wss	|- x C_ a
13	10	cv	|- y
14	13 6	wss	|- y C_ b
15	12 14	wa	|- ( x C_ a /\ y C_ b )
16	4	cv	|- r
17	16 11	cima	|- ( r " x )
18	17 13	wceq	|- ( r " x ) = y
19	15 18	wa	|- ( ( x C_ a /\ y C_ b ) /\ ( r " x ) = y )
20	19 9 10	copab	|- { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ ( r " x ) = y ) }
21	4 8 20	cmpt	|- ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ ( r " x ) = y ) } )
22	1 3 2 2 21	cmpo	|- ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ ( r " x ) = y ) } ) )
23	0 22	wceq	|- ~P_* = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ ( r " x ) = y ) } ) )