Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-inv Structured version   Unicode version

Definition df-inv 15164
 Description: The inverse relation in a category. Given arrows and , we say Inv, that is, is an inverse of , if is a section of and is a section of . 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 Sect Sect
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-inv
StepHypRef Expression
1 cinv 15161 . 2 Inv
2 vc . . 3
3 ccat 15081 . . 3
4 vx . . . 4
5 vy . . . 4
62cv 1394 . . . . 5
7 cbs 14644 . . . . 5
86, 7cfv 5594 . . . 4
94cv 1394 . . . . . 6
105cv 1394 . . . . . 6
11 csect 15160 . . . . . . 7 Sect
126, 11cfv 5594 . . . . . 6 Sect
139, 10, 12co 6296 . . . . 5 Sect
1410, 9, 12co 6296 . . . . . 6 Sect
1514ccnv 5007 . . . . 5 Sect
1613, 15cin 3470 . . . 4 Sect Sect
174, 5, 8, 8, 16cmpt2 6298 . . 3 Sect Sect
182, 3, 17cmpt 4515 . 2 Sect Sect
191, 18wceq 1395 1 Inv Sect Sect
 Colors of variables: wff setvar class This definition is referenced by:  invffval  15174  isofn  15191
 Copyright terms: Public domain W3C validator