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

Definition df-hof 14339
 Description: Define the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from oppCat to , whose object part is the hom-function , and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 11-Jan-2017.)
Assertion
Ref Expression
df-hof HomF f comp comp
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-hof
StepHypRef Expression
1 chof 14337 . 2 HomF
2 vc . . 3
3 ccat 13881 . . 3
42cv 1651 . . . . 5
5 chomf 13883 . . . . 5 f
64, 5cfv 5446 . . . 4 f
7 vb . . . . 5
8 cbs 13461 . . . . . 6
94, 8cfv 5446 . . . . 5
10 vx . . . . . 6
11 vy . . . . . 6
127cv 1651 . . . . . . 7
1312, 12cxp 4868 . . . . . 6
14 vf . . . . . . 7
15 vg . . . . . . 7
1611cv 1651 . . . . . . . . 9
17 c1st 6339 . . . . . . . . 9
1816, 17cfv 5446 . . . . . . . 8
1910cv 1651 . . . . . . . . 9
2019, 17cfv 5446 . . . . . . . 8
21 chom 13532 . . . . . . . . 9
224, 21cfv 5446 . . . . . . . 8
2318, 20, 22co 6073 . . . . . . 7
24 c2nd 6340 . . . . . . . . 9
2519, 24cfv 5446 . . . . . . . 8
2616, 24cfv 5446 . . . . . . . 8
2725, 26, 22co 6073 . . . . . . 7
28 vh . . . . . . . 8
2919, 22cfv 5446 . . . . . . . 8
3015cv 1651 . . . . . . . . . 10
3128cv 1651 . . . . . . . . . 10
32 cco 13533 . . . . . . . . . . . 12 comp
334, 32cfv 5446 . . . . . . . . . . 11 comp
3419, 26, 33co 6073 . . . . . . . . . 10 comp
3530, 31, 34co 6073 . . . . . . . . 9 comp
3614cv 1651 . . . . . . . . 9
3718, 20cop 3809 . . . . . . . . . 10
3837, 26, 33co 6073 . . . . . . . . 9 comp
3935, 36, 38co 6073 . . . . . . . 8 comp comp
4028, 29, 39cmpt 4258 . . . . . . 7 comp comp
4114, 15, 23, 27, 40cmpt2 6075 . . . . . 6 comp comp
4210, 11, 13, 13, 41cmpt2 6075 . . . . 5 comp comp
437, 9, 42csb 3243 . . . 4 comp comp
446, 43cop 3809 . . 3 f comp comp
452, 3, 44cmpt 4258 . 2 f comp comp
461, 45wceq 1652 1 HomF f comp comp
 Colors of variables: wff set class This definition is referenced by:  hofval  14341
 Copyright terms: Public domain W3C validator