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

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

Detailed syntax breakdown of Definition df-full
StepHypRef Expression
1 cful 14101 . 2 Full
2 vc . . 3
3 vd . . 3
4 ccat 13891 . . 3
5 vf . . . . . . 7
65cv 1652 . . . . . 6
7 vg . . . . . . 7
87cv 1652 . . . . . 6
92cv 1652 . . . . . . 7
103cv 1652 . . . . . . 7
11 cfunc 14053 . . . . . . 7
129, 10, 11co 6083 . . . . . 6
136, 8, 12wbr 4214 . . . . 5
14 vx . . . . . . . . . . 11
1514cv 1652 . . . . . . . . . 10
16 vy . . . . . . . . . . 11
1716cv 1652 . . . . . . . . . 10
1815, 17, 8co 6083 . . . . . . . . 9
1918crn 4881 . . . . . . . 8
2015, 6cfv 5456 . . . . . . . . 9
2117, 6cfv 5456 . . . . . . . . 9
22 chom 13542 . . . . . . . . . 10
2310, 22cfv 5456 . . . . . . . . 9
2420, 21, 23co 6083 . . . . . . . 8
2519, 24wceq 1653 . . . . . . 7
26 cbs 13471 . . . . . . . 8
279, 26cfv 5456 . . . . . . 7
2825, 16, 27wral 2707 . . . . . 6
2928, 14, 27wral 2707 . . . . 5
3013, 29wa 360 . . . 4
3130, 5, 7copab 4267 . . 3
322, 3, 4, 4, 31cmpt2 6085 . 2
331, 32wceq 1653 1 Full
 Colors of variables: wff set class This definition is referenced by:  fullfunc  14105  isfull  14109
 Copyright terms: Public domain W3C validator