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

Definition df-func 14047
 Description: Function returning all the functors from a category to a category . Intuitively a functor associates any morphism of to a morphism of , any object of to an object of , and respects the identity, the composition, the domain and the codomain. Here to capture the idea that a functor associates any object of to an object of we write it associates any identity of to an identity of which simplifies the definition. (Contributed by FL, 10-Feb-2008.) (Revised by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
df-func comp comp
Distinct variable group:   ,,,,,,,,,

Detailed syntax breakdown of Definition df-func
StepHypRef Expression
1 cfunc 14043 . 2
2 vt . . 3
3 vu . . 3
4 ccat 13881 . . 3
5 vb . . . . . . . 8
65cv 1651 . . . . . . 7
73cv 1651 . . . . . . . 8
8 cbs 13461 . . . . . . . 8
97, 8cfv 5446 . . . . . . 7
10 vf . . . . . . . 8
1110cv 1651 . . . . . . 7
126, 9, 11wf 5442 . . . . . 6
13 vg . . . . . . . 8
1413cv 1651 . . . . . . 7
15 vz . . . . . . . 8
166, 6cxp 4868 . . . . . . . 8
1715cv 1651 . . . . . . . . . . . 12
18 c1st 6339 . . . . . . . . . . . 12
1917, 18cfv 5446 . . . . . . . . . . 11
2019, 11cfv 5446 . . . . . . . . . 10
21 c2nd 6340 . . . . . . . . . . . 12
2217, 21cfv 5446 . . . . . . . . . . 11
2322, 11cfv 5446 . . . . . . . . . 10
24 chom 13532 . . . . . . . . . . 11
257, 24cfv 5446 . . . . . . . . . 10
2620, 23, 25co 6073 . . . . . . . . 9
272cv 1651 . . . . . . . . . . 11
2827, 24cfv 5446 . . . . . . . . . 10
2917, 28cfv 5446 . . . . . . . . 9
30 cmap 7010 . . . . . . . . 9
3126, 29, 30co 6073 . . . . . . . 8
3215, 16, 31cixp 7055 . . . . . . 7
3314, 32wcel 1725 . . . . . 6
34 vx . . . . . . . . . . . 12
3534cv 1651 . . . . . . . . . . 11
36 ccid 13882 . . . . . . . . . . . 12
3727, 36cfv 5446 . . . . . . . . . . 11
3835, 37cfv 5446 . . . . . . . . . 10
3935, 35, 14co 6073 . . . . . . . . . 10
4038, 39cfv 5446 . . . . . . . . 9
4135, 11cfv 5446 . . . . . . . . . 10
427, 36cfv 5446 . . . . . . . . . 10
4341, 42cfv 5446 . . . . . . . . 9
4440, 43wceq 1652 . . . . . . . 8
45 vn . . . . . . . . . . . . . . . 16
4645cv 1651 . . . . . . . . . . . . . . 15
47 vm . . . . . . . . . . . . . . . 16
4847cv 1651 . . . . . . . . . . . . . . 15
49 vy . . . . . . . . . . . . . . . . . 18
5049cv 1651 . . . . . . . . . . . . . . . . 17
5135, 50cop 3809 . . . . . . . . . . . . . . . 16
52 cco 13533 . . . . . . . . . . . . . . . . 17 comp
5327, 52cfv 5446 . . . . . . . . . . . . . . . 16 comp
5451, 17, 53co 6073 . . . . . . . . . . . . . . 15 comp
5546, 48, 54co 6073 . . . . . . . . . . . . . 14 comp
5635, 17, 14co 6073 . . . . . . . . . . . . . 14
5755, 56cfv 5446 . . . . . . . . . . . . 13 comp
5850, 17, 14co 6073 . . . . . . . . . . . . . . 15
5946, 58cfv 5446 . . . . . . . . . . . . . 14
6035, 50, 14co 6073 . . . . . . . . . . . . . . 15
6148, 60cfv 5446 . . . . . . . . . . . . . 14
6250, 11cfv 5446 . . . . . . . . . . . . . . . 16
6341, 62cop 3809 . . . . . . . . . . . . . . 15
6417, 11cfv 5446 . . . . . . . . . . . . . . 15
657, 52cfv 5446 . . . . . . . . . . . . . . 15 comp
6663, 64, 65co 6073 . . . . . . . . . . . . . 14 comp
6759, 61, 66co 6073 . . . . . . . . . . . . 13 comp
6857, 67wceq 1652 . . . . . . . . . . . 12 comp comp
6950, 17, 28co 6073 . . . . . . . . . . . 12
7068, 45, 69wral 2697 . . . . . . . . . . 11 comp comp
7135, 50, 28co 6073 . . . . . . . . . . 11
7270, 47, 71wral 2697 . . . . . . . . . 10 comp comp
7372, 15, 6wral 2697 . . . . . . . . 9 comp comp
7473, 49, 6wral 2697 . . . . . . . 8 comp comp
7544, 74wa 359 . . . . . . 7 comp comp
7675, 34, 6wral 2697 . . . . . 6 comp comp
7712, 33, 76w3a 936 . . . . 5 comp comp
7827, 8cfv 5446 . . . . 5
7977, 5, 78wsbc 3153 . . . 4 comp comp
8079, 10, 13copab 4257 . . 3 comp comp
812, 3, 4, 4, 80cmpt2 6075 . 2 comp comp
821, 81wceq 1652 1 comp comp
 Colors of variables: wff set class This definition is referenced by:  relfunc  14051  funcrcl  14052  isfunc  14053
 Copyright terms: Public domain W3C validator