Definition df-iminv

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

	Ref	Expression
Assertion	df-iminv	|- ~P^* = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ x = ( `' r " y ) ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ciminv	|- ~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	ccnv	|- `' r
18	17 13	cima	|- ( `' r " y )
19	11 18	wceq	|- x = ( `' r " y )
20	15 19	wa	|- ( ( x C_ a /\ y C_ b ) /\ x = ( `' r " y ) )
21	20 9 10	copab	|- { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ x = ( `' r " y ) ) }
22	4 8 21	cmpt	|- ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ x = ( `' r " y ) ) } )
23	1 3 2 2 22	cmpo	|- ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ x = ( `' r " y ) ) } ) )
24	0 23	wceq	|- ~P^* = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ x = ( `' r " y ) ) } ) )