Definition df-cat 16329

Description: A category is an abstraction of a structure (a group, a topology, an order...) Category theory consists in finding new formulation of the concepts associated with those structures (product, substructure...) using morphisms instead of the belonging relation. That trick has the interesting property that heterogeneous structures like topologies or groups for instance become comparable. Definition in [Lang] p. 53. In contrast to definition 3.1 of [Adamek] p. 21, where "A category is a quadruple A = (O, hom, id, o)", a category is defined as an extensible structure consisting of three slots: the objects "O" ( ( Base ` c )), the morphisms "hom" ( ( Hom ` c )) and the composition law "o" ( (comp ` c )). The identities "id" are defined by their properties related to morphisms and their composition, see condition 3.1(b) in [Adamek] p. 21 and df-cid 16330. (Note: in category theory morphisms are also called arrows.) (Contributed by FL, 24-Oct-2007.) (Revised by Mario Carneiro, 2-Jan-2017.)

Assertion

Ref

Expression

df-cat

|- Cat = { c | [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. [. (comp ` c ) / o ]. A. x e. b ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) ) }

Distinct variable group:   b, c, f, g, h, k, o, w, x, y, z

Detailed syntax breakdown of Definition df-cat

Step	Hyp	Ref	Expression
1		ccat 16325	. 2 class Cat
2		vg	. . . . . . . . . . . . . . 15 setvar g
3	2	cv 1482	. . . . . . . . . . . . . 14 class g
4		vf	. . . . . . . . . . . . . . 15 setvar f
5	4	cv 1482	. . . . . . . . . . . . . 14 class f
6		vy	. . . . . . . . . . . . . . . . 17 setvar y
7	6	cv 1482	. . . . . . . . . . . . . . . 16 class y
8		vx	. . . . . . . . . . . . . . . . 17 setvar x
9	8	cv 1482	. . . . . . . . . . . . . . . 16 class x
10	7, 9	cop 4183	. . . . . . . . . . . . . . 15 class <. y , x >.
11		vo	. . . . . . . . . . . . . . . 16 setvar o
12	11	cv 1482	. . . . . . . . . . . . . . 15 class o
13	10, 9, 12	co 6650	. . . . . . . . . . . . . 14 class ( <. y , x >. o x )
14	3, 5, 13	co 6650	. . . . . . . . . . . . 13 class ( g ( <. y , x >. o x ) f )
15	14, 5	wceq 1483	. . . . . . . . . . . 12 wff ( g ( <. y , x >. o x ) f ) = f
16		vh	. . . . . . . . . . . . . 14 setvar h
17	16	cv 1482	. . . . . . . . . . . . 13 class h
18	7, 9, 17	co 6650	. . . . . . . . . . . 12 class ( y h x )
19	15, 4, 18	wral 2912	. . . . . . . . . . 11 wff A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f
20	9, 9	cop 4183	. . . . . . . . . . . . . . 15 class <. x , x >.
21	20, 7, 12	co 6650	. . . . . . . . . . . . . 14 class ( <. x , x >. o y )
22	5, 3, 21	co 6650	. . . . . . . . . . . . 13 class ( f ( <. x , x >. o y ) g )
23	22, 5	wceq 1483	. . . . . . . . . . . 12 wff ( f ( <. x , x >. o y ) g ) = f
24	9, 7, 17	co 6650	. . . . . . . . . . . 12 class ( x h y )
25	23, 4, 24	wral 2912	. . . . . . . . . . 11 wff A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f
26	19, 25	wa 384	. . . . . . . . . 10 wff ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f )
27		vb	. . . . . . . . . . 11 setvar b
28	27	cv 1482	. . . . . . . . . 10 class b
29	26, 6, 28	wral 2912	. . . . . . . . 9 wff A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f )
30	9, 9, 17	co 6650	. . . . . . . . 9 class ( x h x )
31	29, 2, 30	wrex 2913	. . . . . . . 8 wff E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f )
32	9, 7	cop 4183	. . . . . . . . . . . . . . . 16 class <. x , y >.
33		vz	. . . . . . . . . . . . . . . . 17 setvar z
34	33	cv 1482	. . . . . . . . . . . . . . . 16 class z
35	32, 34, 12	co 6650	. . . . . . . . . . . . . . 15 class ( <. x , y >. o z )
36	3, 5, 35	co 6650	. . . . . . . . . . . . . 14 class ( g ( <. x , y >. o z ) f )
37	9, 34, 17	co 6650	. . . . . . . . . . . . . 14 class ( x h z )
38	36, 37	wcel 1990	. . . . . . . . . . . . 13 wff ( g ( <. x , y >. o z ) f ) e. ( x h z )
39		vk	. . . . . . . . . . . . . . . . . . 19 setvar k
40	39	cv 1482	. . . . . . . . . . . . . . . . . 18 class k
41	7, 34	cop 4183	. . . . . . . . . . . . . . . . . . 19 class <. y , z >.
42		vw	. . . . . . . . . . . . . . . . . . . 20 setvar w
43	42	cv 1482	. . . . . . . . . . . . . . . . . . 19 class w
44	41, 43, 12	co 6650	. . . . . . . . . . . . . . . . . 18 class ( <. y , z >. o w )
45	40, 3, 44	co 6650	. . . . . . . . . . . . . . . . 17 class ( k ( <. y , z >. o w ) g )
46	32, 43, 12	co 6650	. . . . . . . . . . . . . . . . 17 class ( <. x , y >. o w )
47	45, 5, 46	co 6650	. . . . . . . . . . . . . . . 16 class ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f )
48	9, 34	cop 4183	. . . . . . . . . . . . . . . . . 18 class <. x , z >.
49	48, 43, 12	co 6650	. . . . . . . . . . . . . . . . 17 class ( <. x , z >. o w )
50	40, 36, 49	co 6650	. . . . . . . . . . . . . . . 16 class ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) )
51	47, 50	wceq 1483	. . . . . . . . . . . . . . 15 wff ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) )
52	34, 43, 17	co 6650	. . . . . . . . . . . . . . 15 class ( z h w )
53	51, 39, 52	wral 2912	. . . . . . . . . . . . . 14 wff A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) )
54	53, 42, 28	wral 2912	. . . . . . . . . . . . 13 wff A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) )
55	38, 54	wa 384	. . . . . . . . . . . 12 wff ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) )
56	7, 34, 17	co 6650	. . . . . . . . . . . 12 class ( y h z )
57	55, 2, 56	wral 2912	. . . . . . . . . . 11 wff A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) )
58	57, 4, 24	wral 2912	. . . . . . . . . 10 wff A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) )
59	58, 33, 28	wral 2912	. . . . . . . . 9 wff A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) )
60	59, 6, 28	wral 2912	. . . . . . . 8 wff A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) )
61	31, 60	wa 384	. . . . . . 7 wff ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) )
62	61, 8, 28	wral 2912	. . . . . 6 wff A. x e. b ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) )
63		vc	. . . . . . . 8 setvar c
64	63	cv 1482	. . . . . . 7 class c
65		cco 15953	. . . . . . 7 class comp
66	64, 65	cfv 5888	. . . . . 6 class (comp ` c )
67	62, 11, 66	wsbc 3435	. . . . 5 wff [. (comp ` c ) / o ]. A. x e. b ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) )
68		chom 15952	. . . . . 6 class Hom
69	64, 68	cfv 5888	. . . . 5 class ( Hom ` c )
70	67, 16, 69	wsbc 3435	. . . 4 wff [. ( Hom ` c ) / h ]. [. (comp ` c ) / o ]. A. x e. b ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) )
71		cbs 15857	. . . . 5 class Base
72	64, 71	cfv 5888	. . . 4 class ( Base ` c )
73	70, 27, 72	wsbc 3435	. . 3 wff [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. [. (comp ` c ) / o ]. A. x e. b ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) )
74	73, 63	cab 2608	. 2 class { c | [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. [. (comp ` c ) / o ]. A. x e. b ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) ) }
75	1, 74	wceq 1483	1 wff Cat = { c | [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. [. (comp ` c ) / o ]. A. x e. b ( E. g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) /\ A. y e. b A. z e. b A. f e. ( x h y ) A. g e. ( y h z ) ( ( g ( <. x , y >. o z ) f ) e. ( x h z ) /\ A. w e. b A. k e. ( z h w ) ( ( k ( <. y , z >. o w ) g ) ( <. x , y >. o w ) f ) = ( k ( <. x , z >. o w ) ( g ( <. x , y >. o z ) f ) ) ) ) }

This definition is referenced by:  iscat  16333