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	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 ) /\ x = ( `' r " y ) ) } ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ciminv	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	ccnv	$$class{r}^{-1}$$
18	17 13	cima	$$class{r}^{-1}\left[y\right]$$
19	11 18	wceq	$$wffx=r^{-1}\left[y\right]$$
20	15 19	wa	$$wff\left(\left(x\subseteq a\wedge y\subseteq b\right)\wedge x=r^{-1}\left[y\right]\right)$$
21	20 9 10	copab	$$class\left\{⟨x,y⟩|\left(\left(x\subseteq a\wedge y\subseteq b\right)\wedge x=r^{-1}\left[y\right]\right)\right\}$$
22	4 8 21	cmpt	$$class\left(r\in 𝒫\left(a\times b\right)⟼\left\{⟨x,y⟩|\left(\left(x\subseteq a\wedge y\subseteq b\right)\wedge x=r^{-1}\left[y\right]\right)\right\}\right)$$
23	1 3 2 2 22	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 x=r^{-1}\left[y\right]\right)\right\}\right)\right)$$
24	0 23	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 ) /\ x = ( `' r " 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 ) /\ x = ( `' r " y ) ) } ) ) with typecode wff