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	$$⊢{𝒫}^{*}=\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)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ciminv	$$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	$$wff{𝒫}^{*}=\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)$$