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

Definition df-fth 14094
 Description: Function returning all the faithful functors from a category to a category . A full functor is a functor in which all the morphism maps between objects are injections. (Contributed by Mario Carneiro, 26-Jan-2017.)
Assertion
Ref Expression
df-fth Faith
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-fth
StepHypRef Expression
1 cfth 14092 . 2 Faith
2 vc . . 3
3 vd . . 3
4 ccat 13881 . . 3
5 vf . . . . . . 7
65cv 1651 . . . . . 6
7 vg . . . . . . 7
87cv 1651 . . . . . 6
92cv 1651 . . . . . . 7
103cv 1651 . . . . . . 7
11 cfunc 14043 . . . . . . 7
129, 10, 11co 6073 . . . . . 6
136, 8, 12wbr 4204 . . . . 5
14 vx . . . . . . . . . . 11
1514cv 1651 . . . . . . . . . 10
16 vy . . . . . . . . . . 11
1716cv 1651 . . . . . . . . . 10
1815, 17, 8co 6073 . . . . . . . . 9
1918ccnv 4869 . . . . . . . 8
2019wfun 5440 . . . . . . 7
21 cbs 13461 . . . . . . . 8
229, 21cfv 5446 . . . . . . 7
2320, 16, 22wral 2697 . . . . . 6
2423, 14, 22wral 2697 . . . . 5
2513, 24wa 359 . . . 4
2625, 5, 7copab 4257 . . 3
272, 3, 4, 4, 26cmpt2 6075 . 2
281, 27wceq 1652 1 Faith
 Colors of variables: wff set class This definition is referenced by:  fthfunc  14096  isfth  14103
 Copyright terms: Public domain W3C validator