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

Definition df-fth 15321
 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. Definition 3.27(2) in [Adamek] p. 34. (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 15319 . 2 Faith
2 vc . . 3
3 vd . . 3
4 ccat 15081 . . 3
5 vf . . . . . . 7
65cv 1394 . . . . . 6
7 vg . . . . . . 7
87cv 1394 . . . . . 6
92cv 1394 . . . . . . 7
103cv 1394 . . . . . . 7
11 cfunc 15270 . . . . . . 7
129, 10, 11co 6296 . . . . . 6
136, 8, 12wbr 4456 . . . . 5
14 vx . . . . . . . . . . 11
1514cv 1394 . . . . . . . . . 10
16 vy . . . . . . . . . . 11
1716cv 1394 . . . . . . . . . 10
1815, 17, 8co 6296 . . . . . . . . 9
1918ccnv 5007 . . . . . . . 8
2019wfun 5588 . . . . . . 7
21 cbs 14644 . . . . . . . 8
229, 21cfv 5594 . . . . . . 7
2320, 16, 22wral 2807 . . . . . 6
2423, 14, 22wral 2807 . . . . 5
2513, 24wa 369 . . . 4
2625, 5, 7copab 4514 . . 3
272, 3, 4, 4, 26cmpt2 6298 . 2
281, 27wceq 1395 1 Faith
 Colors of variables: wff setvar class This definition is referenced by:  fthfunc  15323  isfth  15330
 Copyright terms: Public domain W3C validator