Definition df-inv 16408

Description: The inverse relation in a category. Given arrows f : X --> Y and g : Y --> X, we say gInv f, that is, g is an inverse of f, if g is a section of f and f is a section of g. Definition 3.8 of [Adamek] p. 28. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 2-Jan-2017.)

Assertion

Ref	Expression
df-inv	|- Inv = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( ( x (Sect ` c ) y ) i^i `' ( y (Sect ` c ) x ) ) ) )

Distinct variable group:   x, c, y

Detailed syntax breakdown of Definition df-inv

Step	Hyp	Ref	Expression
1		cinv 16405	. 2 class Inv
2		vc	. . 3 setvar c
3		ccat 16325	. . 3 class Cat
4		vx	. . . 4 setvar x
5		vy	. . . 4 setvar y
6	2	cv 1482	. . . . 5 class c
7		cbs 15857	. . . . 5 class Base
8	6, 7	cfv 5888	. . . 4 class ( Base ` c )
9	4	cv 1482	. . . . . 6 class x
10	5	cv 1482	. . . . . 6 class y
11		csect 16404	. . . . . . 7 class Sect
12	6, 11	cfv 5888	. . . . . 6 class (Sect ` c )
13	9, 10, 12	co 6650	. . . . 5 class ( x (Sect ` c ) y )
14	10, 9, 12	co 6650	. . . . . 6 class ( y (Sect ` c ) x )
15	14	ccnv 5113	. . . . 5 class `' ( y (Sect ` c ) x )
16	13, 15	cin 3573	. . . 4 class ( ( x (Sect ` c ) y ) i^i `' ( y (Sect ` c ) x ) )
17	4, 5, 8, 8, 16	cmpt2 6652	. . 3 class ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( ( x (Sect ` c ) y ) i^i `' ( y (Sect ` c ) x ) ) )
18	2, 3, 17	cmpt 4729	. 2 class ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( ( x (Sect ` c ) y ) i^i `' ( y (Sect ` c ) x ) ) ) )
19	1, 18	wceq 1483	1 wff Inv = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( ( x (Sect ` c ) y ) i^i `' ( y (Sect ` c ) x ) ) ) )

This definition is referenced by:  invffval  16418  isofn  16435