This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) )