Definition df-iminv

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ciminv	⊢ 𝒫*
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	ccnv	⊢ ◡ 𝑟
18	17 13	cima	⊢ ( ◡ 𝑟 “ 𝑦 )
19	11 18	wceq	⊢ 𝑥 = ( ◡ 𝑟 “ 𝑦 )
20	15 19	wa	⊢ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ 𝑥 = ( ◡ 𝑟 “ 𝑦 ) )
21	20 9 10	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ 𝑥 = ( ◡ 𝑟 “ 𝑦 ) ) }
22	4 8 21	cmpt	⊢ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ 𝑥 = ( ◡ 𝑟 “ 𝑦 ) ) } )
23	1 3 2 2 22	cmpo	⊢ ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ 𝑥 = ( ◡ 𝑟 “ 𝑦 ) ) } ) )
24	0 23	wceq	⊢ 𝒫* = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏 ) ∧ 𝑥 = ( ◡ 𝑟 “ 𝑦 ) ) } ) )