Definition df-iminv 35363

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

Assertion

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

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

Detailed syntax breakdown of Definition df-iminv

Step	Hyp	Ref	Expression
1		ciminv 35362	. 2 class 𝒫*
2		va	. . 3 setvar 𝑎
3		vb	. . 3 setvar 𝑏
4		cvv 3432	. . 3 class V
5		vr	. . . 4 setvar 𝑟
6	2	cv 1538	. . . . . 6 class 𝑎
7	3	cv 1538	. . . . . 6 class 𝑏
8	6, 7	cxp 5587	. . . . 5 class (𝑎 × 𝑏)
9	8	cpw 4533	. . . 4 class 𝒫 (𝑎 × 𝑏)
10		vx	. . . . . . . . 9 setvar 𝑥
11	10	cv 1538	. . . . . . . 8 class 𝑥
12	11, 6	wss 3887	. . . . . . 7 wff 𝑥 ⊆ 𝑎
13		vy	. . . . . . . . 9 setvar 𝑦
14	13	cv 1538	. . . . . . . 8 class 𝑦
15	14, 7	wss 3887	. . . . . . 7 wff 𝑦 ⊆ 𝑏
16	12, 15	wa 396	. . . . . 6 wff (𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏)
17	5	cv 1538	. . . . . . . . 9 class 𝑟
18	17	ccnv 5588	. . . . . . . 8 class ◡𝑟
19	18, 14	cima 5592	. . . . . . 7 class (◡𝑟 “ 𝑦)
20	11, 19	wceq 1539	. . . . . 6 wff 𝑥 = (◡𝑟 “ 𝑦)
21	16, 20	wa 396	. . . . 5 wff ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ 𝑥 = (◡𝑟 “ 𝑦))
22	21, 10, 13	copab 5136	. . . 4 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ 𝑥 = (◡𝑟 “ 𝑦))}
23	5, 9, 22	cmpt 5157	. . 3 class (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ 𝑥 = (◡𝑟 “ 𝑦))})
24	2, 3, 4, 4, 23	cmpo 7277	. 2 class (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ 𝑥 = (◡𝑟 “ 𝑦))}))
25	1, 24	wceq 1539	1 wff 𝒫* = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ 𝑥 = (◡𝑟 “ 𝑦))}))

This definition is referenced by:  bj-iminvval  35364