Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-imdir Structured version   Visualization version   GIF version

Definition df-imdir 34555
 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
StepHypRef Expression
1 cimdir 34554 . 2 class 𝒫*
2 va . . 3 setvar 𝑎
3 vb . . 3 setvar 𝑏
4 cvv 3469 . . 3 class V
5 vr . . . 4 setvar 𝑟
62cv 1537 . . . . . 6 class 𝑎
73cv 1537 . . . . . 6 class 𝑏
86, 7cxp 5530 . . . . 5 class (𝑎 × 𝑏)
98cpw 4511 . . . 4 class 𝒫 (𝑎 × 𝑏)
10 vx . . . . . . . . 9 setvar 𝑥
1110cv 1537 . . . . . . . 8 class 𝑥
1211, 6wss 3908 . . . . . . 7 wff 𝑥𝑎
13 vy . . . . . . . . 9 setvar 𝑦
1413cv 1537 . . . . . . . 8 class 𝑦
1514, 7wss 3908 . . . . . . 7 wff 𝑦𝑏
1612, 15wa 399 . . . . . 6 wff (𝑥𝑎𝑦𝑏)
175cv 1537 . . . . . . . 8 class 𝑟
1817, 11cima 5535 . . . . . . 7 class (𝑟𝑥)
1918, 14wceq 1538 . . . . . 6 wff (𝑟𝑥) = 𝑦
2016, 19wa 399 . . . . 5 wff ((𝑥𝑎𝑦𝑏) ∧ (𝑟𝑥) = 𝑦)
2120, 10, 13copab 5104 . . . 4 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝑎𝑦𝑏) ∧ (𝑟𝑥) = 𝑦)}
225, 9, 21cmpt 5122 . . 3 class (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝑎𝑦𝑏) ∧ (𝑟𝑥) = 𝑦)})
232, 3, 4, 4, 22cmpo 7142 . 2 class (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝑎𝑦𝑏) ∧ (𝑟𝑥) = 𝑦)}))
241, 23wceq 1538 1 wff 𝒫* = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝑎𝑦𝑏) ∧ (𝑟𝑥) = 𝑦)}))
 Colors of variables: wff setvar class This definition is referenced by:  bj-imdirval  34557
 Copyright terms: Public domain W3C validator