Metamath Proof Explorer


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 Could not format assertion : No typesetting found for |- ~P^* = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ x = ( `' r " y ) ) } ) ) with typecode |-

Detailed syntax breakdown

Step Hyp Ref Expression
0 ciminv Could not format ~P^* : No typesetting found for class ~P^* with typecode class
1 va setvar a
2 cvv class V
3 vb setvar b
4 vr setvar r
5 1 cv setvar a
6 3 cv setvar b
7 5 6 cxp class a × b
8 7 cpw class 𝒫 a × b
9 vx setvar x
10 vy setvar y
11 9 cv setvar x
12 11 5 wss wff x a
13 10 cv setvar y
14 13 6 wss wff y b
15 12 14 wa wff x a y b
16 4 cv setvar r
17 16 ccnv class r -1
18 17 13 cima class r -1 y
19 11 18 wceq wff x = r -1 y
20 15 19 wa wff x a y b x = r -1 y
21 20 9 10 copab class x y | x a y b x = r -1 y
22 4 8 21 cmpt class r 𝒫 a × b x y | x a y b x = r -1 y
23 1 3 2 2 22 cmpo class a V , b V r 𝒫 a × b x y | x a y b x = r -1 y
24 0 23 wceq Could not format ~P^* = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ x = ( `' r " y ) ) } ) ) : No typesetting found for wff ~P^* = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ x = ( `' r " y ) ) } ) ) with typecode wff