Definition df-catc 16745

Description: Definition of the category Cat, which consists of all categories in the universe u (i.e. "small categories", see definition 3.44. of [Adamek] p. 39), with functors as the morphisms. Definition 3.47 of [Adamek] p. 40. (Contributed by Mario Carneiro, 3-Jan-2017.)

Assertion

Ref	Expression
df-catc	|- CatCat = ( u e. _V |-> [_ ( u i^i Cat ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x Func y ) ) >. , <. (comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } )

Distinct variable group:   f, b, g, u, v, x, y, z

Detailed syntax breakdown of Definition df-catc

Step	Hyp	Ref	Expression
1		ccatc 16744	. 2 class CatCat
2		vu	. . 3 setvar u
3		cvv 3200	. . 3 class _V
4		vb	. . . 4 setvar b
5	2	cv 1482	. . . . 5 class u
6		ccat 16325	. . . . 5 class Cat
7	5, 6	cin 3573	. . . 4 class ( u i^i Cat )
8		cnx 15854	. . . . . . 7 class ndx
9		cbs 15857	. . . . . . 7 class Base
10	8, 9	cfv 5888	. . . . . 6 class ( Base ` ndx )
11	4	cv 1482	. . . . . 6 class b
12	10, 11	cop 4183	. . . . 5 class <. ( Base ` ndx ) , b >.
13		chom 15952	. . . . . . 7 class Hom
14	8, 13	cfv 5888	. . . . . 6 class ( Hom ` ndx )
15		vx	. . . . . . 7 setvar x
16		vy	. . . . . . 7 setvar y
17	15	cv 1482	. . . . . . . 8 class x
18	16	cv 1482	. . . . . . . 8 class y
19		cfunc 16514	. . . . . . . 8 class Func
20	17, 18, 19	co 6650	. . . . . . 7 class ( x Func y )
21	15, 16, 11, 11, 20	cmpt2 6652	. . . . . 6 class ( x e. b , y e. b |-> ( x Func y ) )
22	14, 21	cop 4183	. . . . 5 class <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x Func y ) ) >.
23		cco 15953	. . . . . . 7 class comp
24	8, 23	cfv 5888	. . . . . 6 class (comp ` ndx )
25		vv	. . . . . . 7 setvar v
26		vz	. . . . . . 7 setvar z
27	11, 11	cxp 5112	. . . . . . 7 class ( b X. b )
28		vg	. . . . . . . 8 setvar g
29		vf	. . . . . . . 8 setvar f
30	25	cv 1482	. . . . . . . . . 10 class v
31		c2nd 7167	. . . . . . . . . 10 class 2nd
32	30, 31	cfv 5888	. . . . . . . . 9 class ( 2nd ` v )
33	26	cv 1482	. . . . . . . . 9 class z
34	32, 33, 19	co 6650	. . . . . . . 8 class ( ( 2nd ` v ) Func z )
35	30, 19	cfv 5888	. . . . . . . 8 class ( Func ` v )
36	28	cv 1482	. . . . . . . . 9 class g
37	29	cv 1482	. . . . . . . . 9 class f
38		ccofu 16516	. . . . . . . . 9 class o.func
39	36, 37, 38	co 6650	. . . . . . . 8 class ( g o.func f )
40	28, 29, 34, 35, 39	cmpt2 6652	. . . . . . 7 class ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) )
41	25, 26, 27, 11, 40	cmpt2 6652	. . . . . 6 class ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) )
42	24, 41	cop 4183	. . . . 5 class <. (comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >.
43	12, 22, 42	ctp 4181	. . . 4 class { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x Func y ) ) >. , <. (comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. }
44	4, 7, 43	csb 3533	. . 3 class [_ ( u i^i Cat ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x Func y ) ) >. , <. (comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. }
45	2, 3, 44	cmpt 4729	. 2 class ( u e. _V |-> [_ ( u i^i Cat ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x Func y ) ) >. , <. (comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } )
46	1, 45	wceq 1483	1 wff CatCat = ( u e. _V |-> [_ ( u i^i Cat ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x Func y ) ) >. , <. (comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } )

This definition is referenced by:  catcval  16746