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

Definition df-inv 13976
 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 . (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 13973 . 2 Inv
2 vc . . 3
3 ccat 13891 . . 3
4 vx . . . 4
5 vy . . . 4
62cv 1652 . . . . 5
7 cbs 13471 . . . . 5
86, 7cfv 5456 . . . 4
94cv 1652 . . . . . 6
105cv 1652 . . . . . 6
11 csect 13972 . . . . . . 7 Sect
126, 11cfv 5456 . . . . . 6 Sect
139, 10, 12co 6083 . . . . 5 Sect
1410, 9, 12co 6083 . . . . . 6 Sect
1514ccnv 4879 . . . . 5 Sect
1613, 15cin 3321 . . . 4 Sect Sect
174, 5, 8, 8, 16cmpt2 6085 . . 3 Sect Sect
182, 3, 17cmpt 4268 . 2 Sect Sect
191, 18wceq 1653 1 Inv Sect Sect
 Colors of variables: wff set class This definition is referenced by:  invffval  13985
 Copyright terms: Public domain W3C validator