Definition df-imdir 34499

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.)

Assertion

Ref	Expression
df-imdir	⊢ 𝒫* = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ (𝑟 “ 𝑥) = 𝑦)}))

Distinct variable group:   𝑎,𝑏,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-imdir

Step	Hyp	Ref	Expression
1		cimdir 34498	. 2 class 𝒫*
2		va	. . 3 setvar 𝑎
3		vb	. . 3 setvar 𝑏
4		cvv 3491	. . 3 class V
5		vr	. . . 4 setvar 𝑟
6	2	cv 1535	. . . . . 6 class 𝑎
7	3	cv 1535	. . . . . 6 class 𝑏
8	6, 7	cxp 5546	. . . . 5 class (𝑎 × 𝑏)
9	8	cpw 4532	. . . 4 class 𝒫 (𝑎 × 𝑏)
10		vx	. . . . . . . . 9 setvar 𝑥
11	10	cv 1535	. . . . . . . 8 class 𝑥
12	11, 6	wss 3929	. . . . . . 7 wff 𝑥 ⊆ 𝑎
13		vy	. . . . . . . . 9 setvar 𝑦
14	13	cv 1535	. . . . . . . 8 class 𝑦
15	14, 7	wss 3929	. . . . . . 7 wff 𝑦 ⊆ 𝑏
16	12, 15	wa 398	. . . . . 6 wff (𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏)
17	5	cv 1535	. . . . . . . 8 class 𝑟
18	17, 11	cima 5551	. . . . . . 7 class (𝑟 “ 𝑥)
19	18, 14	wceq 1536	. . . . . 6 wff (𝑟 “ 𝑥) = 𝑦
20	16, 19	wa 398	. . . . 5 wff ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ (𝑟 “ 𝑥) = 𝑦)
21	20, 10, 13	copab 5121	. . . 4 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ (𝑟 “ 𝑥) = 𝑦)}
22	5, 9, 21	cmpt 5139	. . 3 class (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ (𝑟 “ 𝑥) = 𝑦)})
23	2, 3, 4, 4, 22	cmpo 7151	. 2 class (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ (𝑟 “ 𝑥) = 𝑦)}))
24	1, 23	wceq 1536	1 wff 𝒫* = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ (𝑟 “ 𝑥) = 𝑦)}))

This definition is referenced by:  bj-imdirval  34500