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

Definition df-func 15274
 Description: Function returning all the functors from a category to a category . Definition 3.17 of [Adamek] p. 29, and definition in [Lang] p. 62 ("covariant functor"). 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. According to remark 3.19 in [Adamek] p. 30, "a functor F : A -> B is technically a family of functions; one from Ob(A) to Ob(B) [here: f, called "the object part" in the following], and for each pair (A,A') of A-objects, one from hom(A,A') to hom(FA, FA') [here: g, called "the morphism part" in the following]". (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 15270 . 2
2 vt . . 3
3 vu . . 3
4 ccat 15081 . . 3
5 vb . . . . . . . 8
65cv 1394 . . . . . . 7
73cv 1394 . . . . . . . 8
8 cbs 14644 . . . . . . . 8
97, 8cfv 5594 . . . . . . 7
10 vf . . . . . . . 8
1110cv 1394 . . . . . . 7
126, 9, 11wf 5590 . . . . . 6
13 vg . . . . . . . 8
1413cv 1394 . . . . . . 7
15 vz . . . . . . . 8
166, 6cxp 5006 . . . . . . . 8
1715cv 1394 . . . . . . . . . . . 12
18 c1st 6797 . . . . . . . . . . . 12
1917, 18cfv 5594 . . . . . . . . . . 11
2019, 11cfv 5594 . . . . . . . . . 10
21 c2nd 6798 . . . . . . . . . . . 12
2217, 21cfv 5594 . . . . . . . . . . 11
2322, 11cfv 5594 . . . . . . . . . 10
24 chom 14723 . . . . . . . . . . 11
257, 24cfv 5594 . . . . . . . . . 10
2620, 23, 25co 6296 . . . . . . . . 9
272cv 1394 . . . . . . . . . . 11
2827, 24cfv 5594 . . . . . . . . . 10
2917, 28cfv 5594 . . . . . . . . 9
30 cmap 7438 . . . . . . . . 9
3126, 29, 30co 6296 . . . . . . . 8
3215, 16, 31cixp 7488 . . . . . . 7
3314, 32wcel 1819 . . . . . 6
34 vx . . . . . . . . . . . 12
3534cv 1394 . . . . . . . . . . 11
36 ccid 15082 . . . . . . . . . . . 12
3727, 36cfv 5594 . . . . . . . . . . 11
3835, 37cfv 5594 . . . . . . . . . 10
3935, 35, 14co 6296 . . . . . . . . . 10
4038, 39cfv 5594 . . . . . . . . 9
4135, 11cfv 5594 . . . . . . . . . 10
427, 36cfv 5594 . . . . . . . . . 10
4341, 42cfv 5594 . . . . . . . . 9
4440, 43wceq 1395 . . . . . . . 8
45 vn . . . . . . . . . . . . . . . 16
4645cv 1394 . . . . . . . . . . . . . . 15
47 vm . . . . . . . . . . . . . . . 16
4847cv 1394 . . . . . . . . . . . . . . 15
49 vy . . . . . . . . . . . . . . . . . 18
5049cv 1394 . . . . . . . . . . . . . . . . 17
5135, 50cop 4038 . . . . . . . . . . . . . . . 16
52 cco 14724 . . . . . . . . . . . . . . . . 17 comp
5327, 52cfv 5594 . . . . . . . . . . . . . . . 16 comp
5451, 17, 53co 6296 . . . . . . . . . . . . . . 15 comp
5546, 48, 54co 6296 . . . . . . . . . . . . . 14 comp
5635, 17, 14co 6296 . . . . . . . . . . . . . 14
5755, 56cfv 5594 . . . . . . . . . . . . 13 comp
5850, 17, 14co 6296 . . . . . . . . . . . . . . 15
5946, 58cfv 5594 . . . . . . . . . . . . . 14
6035, 50, 14co 6296 . . . . . . . . . . . . . . 15
6148, 60cfv 5594 . . . . . . . . . . . . . 14
6250, 11cfv 5594 . . . . . . . . . . . . . . . 16
6341, 62cop 4038 . . . . . . . . . . . . . . 15
6417, 11cfv 5594 . . . . . . . . . . . . . . 15
657, 52cfv 5594 . . . . . . . . . . . . . . 15 comp
6663, 64, 65co 6296 . . . . . . . . . . . . . 14 comp
6759, 61, 66co 6296 . . . . . . . . . . . . 13 comp
6857, 67wceq 1395 . . . . . . . . . . . 12 comp comp
6950, 17, 28co 6296 . . . . . . . . . . . 12
7068, 45, 69wral 2807 . . . . . . . . . . 11 comp comp
7135, 50, 28co 6296 . . . . . . . . . . 11
7270, 47, 71wral 2807 . . . . . . . . . 10 comp comp
7372, 15, 6wral 2807 . . . . . . . . 9 comp comp
7473, 49, 6wral 2807 . . . . . . . 8 comp comp
7544, 74wa 369 . . . . . . 7 comp comp
7675, 34, 6wral 2807 . . . . . 6 comp comp
7712, 33, 76w3a 973 . . . . 5 comp comp
7827, 8cfv 5594 . . . . 5
7977, 5, 78wsbc 3327 . . . 4 comp comp
8079, 10, 13copab 4514 . . 3 comp comp
812, 3, 4, 4, 80cmpt2 6298 . 2 comp comp
821, 81wceq 1395 1 comp comp
 Colors of variables: wff setvar class This definition is referenced by:  relfunc  15278  funcrcl  15279  isfunc  15280
 Copyright terms: Public domain W3C validator