Definition df-hof 16890

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 ` C ) 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.)

Assertion

Ref	Expression
df-hof	|- HomF = ( c e. Cat |-> <. ( Hom f ` 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 ) ) ) ) >. )

Distinct variable group:   b, c, f, g, h, x, y

Detailed syntax breakdown of Definition df-hof

Step	Hyp	Ref	Expression
1		chof 16888	. 2 class HomF
2		vc	. . 3 setvar c
3		ccat 16325	. . 3 class Cat
4	2	cv 1482	. . . . 5 class c
5		chomf 16327	. . . . 5 class Hom f
6	4, 5	cfv 5888	. . . 4 class ( Hom f ` c )
7		vb	. . . . 5 setvar b
8		cbs 15857	. . . . . 6 class Base
9	4, 8	cfv 5888	. . . . 5 class ( Base ` c )
10		vx	. . . . . 6 setvar x
11		vy	. . . . . 6 setvar y
12	7	cv 1482	. . . . . . 7 class b
13	12, 12	cxp 5112	. . . . . 6 class ( b X. b )
14		vf	. . . . . . 7 setvar f
15		vg	. . . . . . 7 setvar g
16	11	cv 1482	. . . . . . . . 9 class y
17		c1st 7166	. . . . . . . . 9 class 1st
18	16, 17	cfv 5888	. . . . . . . 8 class ( 1st ` y )
19	10	cv 1482	. . . . . . . . 9 class x
20	19, 17	cfv 5888	. . . . . . . 8 class ( 1st ` x )
21		chom 15952	. . . . . . . . 9 class Hom
22	4, 21	cfv 5888	. . . . . . . 8 class ( Hom ` c )
23	18, 20, 22	co 6650	. . . . . . 7 class ( ( 1st ` y ) ( Hom ` c ) ( 1st ` x ) )
24		c2nd 7167	. . . . . . . . 9 class 2nd
25	19, 24	cfv 5888	. . . . . . . 8 class ( 2nd ` x )
26	16, 24	cfv 5888	. . . . . . . 8 class ( 2nd ` y )
27	25, 26, 22	co 6650	. . . . . . 7 class ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) )
28		vh	. . . . . . . 8 setvar h
29	19, 22	cfv 5888	. . . . . . . 8 class ( ( Hom ` c ) ` x )
30	15	cv 1482	. . . . . . . . . 10 class g
31	28	cv 1482	. . . . . . . . . 10 class h
32		cco 15953	. . . . . . . . . . . 12 class comp
33	4, 32	cfv 5888	. . . . . . . . . . 11 class (comp ` c )
34	19, 26, 33	co 6650	. . . . . . . . . 10 class ( x (comp ` c ) ( 2nd ` y ) )
35	30, 31, 34	co 6650	. . . . . . . . 9 class ( g ( x (comp ` c ) ( 2nd ` y ) ) h )
36	14	cv 1482	. . . . . . . . 9 class f
37	18, 20	cop 4183	. . . . . . . . . 10 class <. ( 1st ` y ) , ( 1st ` x ) >.
38	37, 26, 33	co 6650	. . . . . . . . 9 class ( <. ( 1st ` y ) , ( 1st ` x ) >. (comp ` c ) ( 2nd ` y ) )
39	35, 36, 38	co 6650	. . . . . . . 8 class ( ( g ( x (comp ` c ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. (comp ` c ) ( 2nd ` y ) ) f )
40	28, 29, 39	cmpt 4729	. . . . . . 7 class ( h e. ( ( Hom ` c ) ` x ) |-> ( ( g ( x (comp ` c ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. (comp ` c ) ( 2nd ` y ) ) f ) )
41	14, 15, 23, 27, 40	cmpt2 6652	. . . . . 6 class ( 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	10, 11, 13, 13, 41	cmpt2 6652	. . . . 5 class ( 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	7, 9, 42	csb 3533	. . . 4 class [_ ( 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	6, 43	cop 4183	. . 3 class <. ( Hom f ` 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	2, 3, 44	cmpt 4729	. 2 class ( c e. Cat |-> <. ( Hom f ` 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 ) ) ) ) >. )
46	1, 45	wceq 1483	1 wff HomF = ( c e. Cat |-> <. ( Hom f ` 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 ) ) ) ) >. )

This definition is referenced by:  hofval  16892