Definition 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	⊢ 𝒫* = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ ( 𝑟 “ 𝑥 ) = 𝑦 ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cimdir	⊢ 𝒫*
1		va	⊢ 𝑎
2		cvv	⊢ V
3		vb	⊢ 𝑏
4		vr	⊢ 𝑟
5	1	cv	⊢ 𝑎
6	3	cv	⊢ 𝑏
7	5 6	cxp	⊢ ( 𝑎 × 𝑏 )
8	7	cpw	⊢ 𝒫 ( 𝑎 × 𝑏 )
9		vx	⊢ 𝑥
10		vy	⊢ 𝑦
11	9	cv	⊢ 𝑥
12	11 5	wss	⊢ 𝑥 ⊆ 𝑎
13	10	cv	⊢ 𝑦
14	13 6	wss	⊢ 𝑦 ⊆ 𝑏
15	12 14	wa	⊢ ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 )
16	4	cv	⊢ 𝑟
17	16 11	cima	⊢ ( 𝑟 “ 𝑥 )
18	17 13	wceq	⊢ ( 𝑟 “ 𝑥 ) = 𝑦
19	15 18	wa	⊢ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ ( 𝑟 “ 𝑥 ) = 𝑦 )
20	19 9 10	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ ( 𝑟 “ 𝑥 ) = 𝑦 ) }
21	4 8 20	cmpt	⊢ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ ( 𝑟 “ 𝑥 ) = 𝑦 ) } )
22	1 3 2 2 21	cmpo	⊢ ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ ( 𝑟 “ 𝑥 ) = 𝑦 ) } ) )
23	0 22	wceq	⊢ 𝒫* = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ ( 𝑟 “ 𝑥 ) = 𝑦 ) } ) )