Definition df-inv

Description: The inverse relation in a category. Given arrows f : X --> Y and g : Y --> X , we say g Inv 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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinv	|- Inv
1		vc	|- c
2		ccat	|- Cat
3		vx	|- x
4		cbs	|- Base
5	1	cv	|- c
6	5 4	cfv	|- ( Base ` c )
7		vy	|- y
8	3	cv	|- x
9		csect	|- Sect
10	5 9	cfv	|- ( Sect ` c )
11	7	cv	|- y
12	8 11 10	co	|- ( x ( Sect ` c ) y )
13	11 8 10	co	|- ( y ( Sect ` c ) x )
14	13	ccnv	|- `' ( y ( Sect ` c ) x )
15	12 14	cin	|- ( ( x ( Sect ` c ) y ) i^i `' ( y ( Sect ` c ) x ) )
16	3 7 6 6 15	cmpo	|- ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( ( x ( Sect ` c ) y ) i^i `' ( y ( Sect ` c ) x ) ) )
17	1 2 16	cmpt	|- ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( ( x ( Sect ` c ) y ) i^i `' ( y ( Sect ` c ) x ) ) ) )
18	0 17	wceq	|- Inv = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( ( x ( Sect ` c ) y ) i^i `' ( y ( Sect ` c ) x ) ) ) )