Definition df-fuc 16604

Description: Definition of the category of functors between two fixed categories, with the objects being functors and the morphisms being natural transformations. Definition 6.15 in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.)

Assertion

Ref

Expression

df-fuc

|- FuncCat = ( t e. Cat , u e. Cat |-> { <. ( Base ` ndx ) , ( t Func u ) >. , <. ( Hom ` ndx ) , ( t Nat u ) >. , <. (comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. (comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } )

Distinct variable group:   a, b, f, g, h, t, u, v, x

Detailed syntax breakdown of Definition df-fuc

Step	Hyp	Ref	Expression
1		cfuc 16602	. 2 class FuncCat
2		vt	. . 3 setvar t
3		vu	. . 3 setvar u
4		ccat 16325	. . 3 class Cat
5		cnx 15854	. . . . . 6 class ndx
6		cbs 15857	. . . . . 6 class Base
7	5, 6	cfv 5888	. . . . 5 class ( Base ` ndx )
8	2	cv 1482	. . . . . 6 class t
9	3	cv 1482	. . . . . 6 class u
10		cfunc 16514	. . . . . 6 class Func
11	8, 9, 10	co 6650	. . . . 5 class ( t Func u )
12	7, 11	cop 4183	. . . 4 class <. ( Base ` ndx ) , ( t Func u ) >.
13		chom 15952	. . . . . 6 class Hom
14	5, 13	cfv 5888	. . . . 5 class ( Hom ` ndx )
15		cnat 16601	. . . . . 6 class Nat
16	8, 9, 15	co 6650	. . . . 5 class ( t Nat u )
17	14, 16	cop 4183	. . . 4 class <. ( Hom ` ndx ) , ( t Nat u ) >.
18		cco 15953	. . . . . 6 class comp
19	5, 18	cfv 5888	. . . . 5 class (comp ` ndx )
20		vv	. . . . . 6 setvar v
21		vh	. . . . . 6 setvar h
22	11, 11	cxp 5112	. . . . . 6 class ( ( t Func u ) X. ( t Func u ) )
23		vf	. . . . . . 7 setvar f
24	20	cv 1482	. . . . . . . 8 class v
25		c1st 7166	. . . . . . . 8 class 1st
26	24, 25	cfv 5888	. . . . . . 7 class ( 1st ` v )
27		vg	. . . . . . . 8 setvar g
28		c2nd 7167	. . . . . . . . 9 class 2nd
29	24, 28	cfv 5888	. . . . . . . 8 class ( 2nd ` v )
30		vb	. . . . . . . . 9 setvar b
31		va	. . . . . . . . 9 setvar a
32	27	cv 1482	. . . . . . . . . 10 class g
33	21	cv 1482	. . . . . . . . . 10 class h
34	32, 33, 16	co 6650	. . . . . . . . 9 class ( g ( t Nat u ) h )
35	23	cv 1482	. . . . . . . . . 10 class f
36	35, 32, 16	co 6650	. . . . . . . . 9 class ( f ( t Nat u ) g )
37		vx	. . . . . . . . . 10 setvar x
38	8, 6	cfv 5888	. . . . . . . . . 10 class ( Base ` t )
39	37	cv 1482	. . . . . . . . . . . 12 class x
40	30	cv 1482	. . . . . . . . . . . 12 class b
41	39, 40	cfv 5888	. . . . . . . . . . 11 class ( b ` x )
42	31	cv 1482	. . . . . . . . . . . 12 class a
43	39, 42	cfv 5888	. . . . . . . . . . 11 class ( a ` x )
44	35, 25	cfv 5888	. . . . . . . . . . . . . 14 class ( 1st ` f )
45	39, 44	cfv 5888	. . . . . . . . . . . . 13 class ( ( 1st ` f ) ` x )
46	32, 25	cfv 5888	. . . . . . . . . . . . . 14 class ( 1st ` g )
47	39, 46	cfv 5888	. . . . . . . . . . . . 13 class ( ( 1st ` g ) ` x )
48	45, 47	cop 4183	. . . . . . . . . . . 12 class <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >.
49	33, 25	cfv 5888	. . . . . . . . . . . . 13 class ( 1st ` h )
50	39, 49	cfv 5888	. . . . . . . . . . . 12 class ( ( 1st ` h ) ` x )
51	9, 18	cfv 5888	. . . . . . . . . . . 12 class (comp ` u )
52	48, 50, 51	co 6650	. . . . . . . . . . 11 class ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. (comp ` u ) ( ( 1st ` h ) ` x ) )
53	41, 43, 52	co 6650	. . . . . . . . . 10 class ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. (comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) )
54	37, 38, 53	cmpt 4729	. . . . . . . . 9 class ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. (comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) )
55	30, 31, 34, 36, 54	cmpt2 6652	. . . . . . . 8 class ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. (comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) )
56	27, 29, 55	csb 3533	. . . . . . 7 class [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. (comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) )
57	23, 26, 56	csb 3533	. . . . . 6 class [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. (comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) )
58	20, 21, 22, 11, 57	cmpt2 6652	. . . . 5 class ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. (comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) )
59	19, 58	cop 4183	. . . 4 class <. (comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. (comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >.
60	12, 17, 59	ctp 4181	. . 3 class { <. ( Base ` ndx ) , ( t Func u ) >. , <. ( Hom ` ndx ) , ( t Nat u ) >. , <. (comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. (comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. }
61	2, 3, 4, 4, 60	cmpt2 6652	. 2 class ( t e. Cat , u e. Cat |-> { <. ( Base ` ndx ) , ( t Func u ) >. , <. ( Hom ` ndx ) , ( t Nat u ) >. , <. (comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. (comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } )
62	1, 61	wceq 1483	1 wff FuncCat = ( t e. Cat , u e. Cat |-> { <. ( Base ` ndx ) , ( t Func u ) >. , <. ( Hom ` ndx ) , ( t Nat u ) >. , <. (comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. (comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } )

This definition is referenced by:  fnfuc  16605  fucval  16618