Metamath Proof Explorer

Definition df-hof

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 ( oppCatC ) X. C to SetCat , whose object part is the hom-function Hom , and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Assertion df-hof 
|- HomF = ( c e. Cat |-> <. ( Homf ` c ) , [_ ( Base ` c ) / b ]_ ( x e. ( b X. b ) , y e. ( b X. b ) |-> ( f e. ( ( 1st ` y ) ( Hom ` c ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` c ) ` x ) |-> ( ( g ( x ( comp ` c ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` c ) ( 2nd ` y ) ) f ) ) ) ) >. )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chof 
 |-  HomF
1 vc 
 |-  c
2 ccat 
 |-  Cat
3 chomf 
 |-  Homf
4 1 cv 
 |-  c
5 4 3 cfv 
 |-  ( Homf ` c )
6 cbs 
 |-  Base
7 4 6 cfv 
 |-  ( Base ` c )
8 vb 
 |-  b
9 vx 
 |-  x
10 8 cv 
 |-  b
11 10 10 cxp 
 |-  ( b X. b )
12 vy 
 |-  y
13 vf 
 |-  f
14 c1st 
 |-  1st
15 12 cv 
 |-  y
16 15 14 cfv 
 |-  ( 1st ` y )
17 chom 
 |-  Hom
18 4 17 cfv 
 |-  ( Hom ` c )
19 9 cv 
 |-  x
20 19 14 cfv 
 |-  ( 1st ` x )
21 16 20 18 co 
 |-  ( ( 1st ` y ) ( Hom ` c ) ( 1st ` x ) )
22 vg 
 |-  g
23 c2nd 
 |-  2nd
24 19 23 cfv 
 |-  ( 2nd ` x )
25 15 23 cfv 
 |-  ( 2nd ` y )
26 24 25 18 co 
 |-  ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) )
27 vh 
 |-  h
28 19 18 cfv 
 |-  ( ( Hom ` c ) ` x )
29 22 cv 
 |-  g
30 cco 
 |-  comp
31 4 30 cfv 
 |-  ( comp ` c )
32 19 25 31 co 
 |-  ( x ( comp ` c ) ( 2nd ` y ) )
33 27 cv 
 |-  h
34 29 33 32 co 
 |-  ( g ( x ( comp ` c ) ( 2nd ` y ) ) h )
35 16 20 cop 
 |-  <. ( 1st ` y ) , ( 1st ` x ) >.
36 35 25 31 co 
 |-  ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` c ) ( 2nd ` y ) )
37 13 cv 
 |-  f
38 34 37 36 co 
 |-  ( ( g ( x ( comp ` c ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` c ) ( 2nd ` y ) ) f )
39 27 28 38 cmpt 
 |-  ( h e. ( ( Hom ` c ) ` x ) |-> ( ( g ( x ( comp ` c ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` c ) ( 2nd ` y ) ) f ) )
40 13 22 21 26 39 cmpo 
 |-  ( f e. ( ( 1st ` y ) ( Hom ` c ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` c ) ` x ) |-> ( ( g ( x ( comp ` c ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` c ) ( 2nd ` y ) ) f ) ) )
41 9 12 11 11 40 cmpo 
 |-  ( x e. ( b X. b ) , y e. ( b X. b ) |-> ( f e. ( ( 1st ` y ) ( Hom ` c ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` c ) ` x ) |-> ( ( g ( x ( comp ` c ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` c ) ( 2nd ` y ) ) f ) ) ) )
42 8 7 41 csb 
 |-  [_ ( Base ` c ) / b ]_ ( x e. ( b X. b ) , y e. ( b X. b ) |-> ( f e. ( ( 1st ` y ) ( Hom ` c ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` c ) ` x ) |-> ( ( g ( x ( comp ` c ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` c ) ( 2nd ` y ) ) f ) ) ) )
43 5 42 cop 
 |-  <. ( Homf ` c ) , [_ ( Base ` c ) / b ]_ ( x e. ( b X. b ) , y e. ( b X. b ) |-> ( f e. ( ( 1st ` y ) ( Hom ` c ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` c ) ` x ) |-> ( ( g ( x ( comp ` c ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` c ) ( 2nd ` y ) ) f ) ) ) ) >.
44 1 2 43 cmpt 
 |-  ( c e. Cat |-> <. ( Homf ` c ) , [_ ( Base ` c ) / b ]_ ( x e. ( b X. b ) , y e. ( b X. b ) |-> ( f e. ( ( 1st ` y ) ( Hom ` c ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` c ) ` x ) |-> ( ( g ( x ( comp ` c ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` c ) ( 2nd ` y ) ) f ) ) ) ) >. )
45 0 44 wceq 
 |-  HomF = ( c e. Cat |-> <. ( Homf ` c ) , [_ ( Base ` c ) / b ]_ ( x e. ( b X. b ) , y e. ( b X. b ) |-> ( f e. ( ( 1st ` y ) ( Hom ` c ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` c ) ` x ) |-> ( ( g ( x ( comp ` c ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. ( comp ` c ) ( 2nd ` y ) ) f ) ) ) ) >. )