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	$⊢ 𝒫_{*} = (a \in V, b \in V ⟼ (r \in 𝒫 (a \times b) ⟼ \{⟨x, y⟩ \| ((x \subseteq a \land y \subseteq b) \land r [x] = y)\}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cimdir	$class 𝒫_{*}$
1		va	$setvar a$
2		cvv	$class V$
3		vb	$setvar b$
4		vr	$setvar r$
5	1	cv	$setvar a$
6	3	cv	$setvar b$
7	5 6	cxp	$class (a \times b)$
8	7	cpw	$class 𝒫 (a \times b)$
9		vx	$setvar x$
10		vy	$setvar y$
11	9	cv	$setvar x$
12	11 5	wss	$wff x \subseteq a$
13	10	cv	$setvar y$
14	13 6	wss	$wff y \subseteq b$
15	12 14	wa	$wff (x \subseteq a \land y \subseteq b)$
16	4	cv	$setvar r$
17	16 11	cima	$class r [x]$
18	17 13	wceq	$wff r [x] = y$
19	15 18	wa	$wff ((x \subseteq a \land y \subseteq b) \land r [x] = y)$
20	19 9 10	copab	$class \{⟨x, y⟩ \| ((x \subseteq a \land y \subseteq b) \land r [x] = y)\}$
21	4 8 20	cmpt	$class (r \in 𝒫 (a \times b) ⟼ \{⟨x, y⟩ \| ((x \subseteq a \land y \subseteq b) \land r [x] = y)\})$
22	1 3 2 2 21	cmpo	$class (a \in V, b \in V ⟼ (r \in 𝒫 (a \times b) ⟼ \{⟨x, y⟩ \| ((x \subseteq a \land y \subseteq b) \land r [x] = y)\}))$
23	0 22	wceq	$wff 𝒫_{*} = (a \in V, b \in V ⟼ (r \in 𝒫 (a \times b) ⟼ \{⟨x, y⟩ \| ((x \subseteq a \land y \subseteq b) \land r [x] = y)\}))$

Metamath Proof Explorer

Definition df-imdir

Detailed syntax breakdown