Definition df-subc 16472

Description: (Subcat ` C ) is the set of all the subcategory specifications of the category C. Like df-subg 17591, this is not actually a collection of categories (as in definition 4.1(a) of [Adamek] p. 48), but only sets which when given operations from the base category (using df-resc 16471) form a category. All the objects and all the morphisms of the subcategory belong to the supercategory. The identity of an object, the domain and the codomain of a morphism are the same in the subcategory and the supercategory. The composition of the subcategory is a restriction of the composition of the supercategory. (Contributed by FL, 17-Sep-2009.) (Revised by Mario Carneiro, 4-Jan-2017.)

Assertion

Ref	Expression
df-subc	|- Subcat = ( c e. Cat |-> { h | ( h C_cat ( Hom f ` c ) /\ [. dom dom h / s ]. A. x e. s ( ( ( Id ` c ) ` x ) e. ( x h x ) /\ A. y e. s A. z e. s A. f e. ( x h y ) A. g e. ( y h z ) ( g ( <. x , y >. (comp ` c ) z ) f ) e. ( x h z ) ) ) } )

Distinct variable group:   f, c, g, h, s, x, y, z

Detailed syntax breakdown of Definition df-subc

Step	Hyp	Ref	Expression
1		csubc 16469	. 2 class Subcat
2		vc	. . 3 setvar c
3		ccat 16325	. . 3 class Cat
4		vh	. . . . . . 7 setvar h
5	4	cv 1482	. . . . . 6 class h
6	2	cv 1482	. . . . . . 7 class c
7		chomf 16327	. . . . . . 7 class Hom f
8	6, 7	cfv 5888	. . . . . 6 class ( Hom f ` c )
9		cssc 16467	. . . . . 6 class C_cat
10	5, 8, 9	wbr 4653	. . . . 5 wff h C_cat ( Hom f ` c )
11		vx	. . . . . . . . . . 11 setvar x
12	11	cv 1482	. . . . . . . . . 10 class x
13		ccid 16326	. . . . . . . . . . 11 class Id
14	6, 13	cfv 5888	. . . . . . . . . 10 class ( Id ` c )
15	12, 14	cfv 5888	. . . . . . . . 9 class ( ( Id ` c ) ` x )
16	12, 12, 5	co 6650	. . . . . . . . 9 class ( x h x )
17	15, 16	wcel 1990	. . . . . . . 8 wff ( ( Id ` c ) ` x ) e. ( x h x )
18		vg	. . . . . . . . . . . . . . 15 setvar g
19	18	cv 1482	. . . . . . . . . . . . . 14 class g
20		vf	. . . . . . . . . . . . . . 15 setvar f
21	20	cv 1482	. . . . . . . . . . . . . 14 class f
22		vy	. . . . . . . . . . . . . . . . 17 setvar y
23	22	cv 1482	. . . . . . . . . . . . . . . 16 class y
24	12, 23	cop 4183	. . . . . . . . . . . . . . 15 class <. x , y >.
25		vz	. . . . . . . . . . . . . . . 16 setvar z
26	25	cv 1482	. . . . . . . . . . . . . . 15 class z
27		cco 15953	. . . . . . . . . . . . . . . 16 class comp
28	6, 27	cfv 5888	. . . . . . . . . . . . . . 15 class (comp ` c )
29	24, 26, 28	co 6650	. . . . . . . . . . . . . 14 class ( <. x , y >. (comp ` c ) z )
30	19, 21, 29	co 6650	. . . . . . . . . . . . 13 class ( g ( <. x , y >. (comp ` c ) z ) f )
31	12, 26, 5	co 6650	. . . . . . . . . . . . 13 class ( x h z )
32	30, 31	wcel 1990	. . . . . . . . . . . 12 wff ( g ( <. x , y >. (comp ` c ) z ) f ) e. ( x h z )
33	23, 26, 5	co 6650	. . . . . . . . . . . 12 class ( y h z )
34	32, 18, 33	wral 2912	. . . . . . . . . . 11 wff A. g e. ( y h z ) ( g ( <. x , y >. (comp ` c ) z ) f ) e. ( x h z )
35	12, 23, 5	co 6650	. . . . . . . . . . 11 class ( x h y )
36	34, 20, 35	wral 2912	. . . . . . . . . 10 wff A. f e. ( x h y ) A. g e. ( y h z ) ( g ( <. x , y >. (comp ` c ) z ) f ) e. ( x h z )
37		vs	. . . . . . . . . . 11 setvar s
38	37	cv 1482	. . . . . . . . . 10 class s
39	36, 25, 38	wral 2912	. . . . . . . . 9 wff A. z e. s A. f e. ( x h y ) A. g e. ( y h z ) ( g ( <. x , y >. (comp ` c ) z ) f ) e. ( x h z )
40	39, 22, 38	wral 2912	. . . . . . . 8 wff A. y e. s A. z e. s A. f e. ( x h y ) A. g e. ( y h z ) ( g ( <. x , y >. (comp ` c ) z ) f ) e. ( x h z )
41	17, 40	wa 384	. . . . . . 7 wff ( ( ( Id ` c ) ` x ) e. ( x h x ) /\ A. y e. s A. z e. s A. f e. ( x h y ) A. g e. ( y h z ) ( g ( <. x , y >. (comp ` c ) z ) f ) e. ( x h z ) )
42	41, 11, 38	wral 2912	. . . . . 6 wff A. x e. s ( ( ( Id ` c ) ` x ) e. ( x h x ) /\ A. y e. s A. z e. s A. f e. ( x h y ) A. g e. ( y h z ) ( g ( <. x , y >. (comp ` c ) z ) f ) e. ( x h z ) )
43	5	cdm 5114	. . . . . . 7 class dom h
44	43	cdm 5114	. . . . . 6 class dom dom h
45	42, 37, 44	wsbc 3435	. . . . 5 wff [. dom dom h / s ]. A. x e. s ( ( ( Id ` c ) ` x ) e. ( x h x ) /\ A. y e. s A. z e. s A. f e. ( x h y ) A. g e. ( y h z ) ( g ( <. x , y >. (comp ` c ) z ) f ) e. ( x h z ) )
46	10, 45	wa 384	. . . 4 wff ( h C_cat ( Hom f ` c ) /\ [. dom dom h / s ]. A. x e. s ( ( ( Id ` c ) ` x ) e. ( x h x ) /\ A. y e. s A. z e. s A. f e. ( x h y ) A. g e. ( y h z ) ( g ( <. x , y >. (comp ` c ) z ) f ) e. ( x h z ) ) )
47	46, 4	cab 2608	. . 3 class { h | ( h C_cat ( Hom f ` c ) /\ [. dom dom h / s ]. A. x e. s ( ( ( Id ` c ) ` x ) e. ( x h x ) /\ A. y e. s A. z e. s A. f e. ( x h y ) A. g e. ( y h z ) ( g ( <. x , y >. (comp ` c ) z ) f ) e. ( x h z ) ) ) }
48	2, 3, 47	cmpt 4729	. 2 class ( c e. Cat |-> { h | ( h C_cat ( Hom f ` c ) /\ [. dom dom h / s ]. A. x e. s ( ( ( Id ` c ) ` x ) e. ( x h x ) /\ A. y e. s A. z e. s A. f e. ( x h y ) A. g e. ( y h z ) ( g ( <. x , y >. (comp ` c ) z ) f ) e. ( x h z ) ) ) } )
49	1, 48	wceq 1483	1 wff Subcat = ( c e. Cat |-> { h | ( h C_cat ( Hom f ` c ) /\ [. dom dom h / s ]. A. x e. s ( ( ( Id ` c ) ` x ) e. ( x h x ) /\ A. y e. s A. z e. s A. f e. ( x h y ) A. g e. ( y h z ) ( g ( <. x , y >. (comp ` c ) z ) f ) e. ( x h z ) ) ) } )

This definition is referenced by:  subcrcl  16476  issubc  16495