Metamath Proof Explorer

Definition df-subc

Description: ( SubcatC ) is the set of all the subcategory specifications of the category C . Like df-subg , 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 ) 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)

Ref Expression
Assertion df-subc 
|- Subcat = ( c e. Cat |-> { h | ( h C_cat ( Homf ` 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 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csubc 
 |-  Subcat
1 vc 
 |-  c
2 ccat 
 |-  Cat
3 vh 
 |-  h
4 3 cv 
 |-  h
5 cssc 
 |-  C_cat
6 chomf 
 |-  Homf
7 1 cv 
 |-  c
8 7 6 cfv 
 |-  ( Homf ` c )
9 4 8 5 wbr 
 |-  h C_cat ( Homf ` c )
10 4 cdm 
 |-  dom h
11 10 cdm 
 |-  dom dom h
12 vs 
 |-  s
13 vx 
 |-  x
14 12 cv 
 |-  s
15 ccid 
 |-  Id
16 7 15 cfv 
 |-  ( Id ` c )
17 13 cv 
 |-  x
18 17 16 cfv 
 |-  ( ( Id ` c ) ` x )
19 17 17 4 co 
 |-  ( x h x )
20 18 19 wcel 
 |-  ( ( Id ` c ) ` x ) e. ( x h x )
21 vy 
 |-  y
22 vz 
 |-  z
23 vf 
 |-  f
24 21 cv 
 |-  y
25 17 24 4 co 
 |-  ( x h y )
26 vg 
 |-  g
27 22 cv 
 |-  z
28 24 27 4 co 
 |-  ( y h z )
29 26 cv 
 |-  g
30 17 24 cop 
 |-  <. x , y >.
31 cco 
 |-  comp
32 7 31 cfv 
 |-  ( comp ` c )
33 30 27 32 co 
 |-  ( <. x , y >. ( comp ` c ) z )
34 23 cv 
 |-  f
35 29 34 33 co 
 |-  ( g ( <. x , y >. ( comp ` c ) z ) f )
36 17 27 4 co 
 |-  ( x h z )
37 35 36 wcel 
 |-  ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x h z )
38 37 26 28 wral 
 |-  A. g e. ( y h z ) ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x h z )
39 38 23 25 wral 
 |-  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 14 wral 
 |-  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 40 21 14 wral 
 |-  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 20 41 wa 
 |-  ( ( ( 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 42 13 14 wral 
 |-  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 ) )
44 43 12 11 wsbc 
 |-  [. 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 ) )
45 9 44 wa 
 |-  ( h C_cat ( Homf ` 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 ) ) )
46 45 3 cab 
 |-  { h | ( h C_cat ( Homf ` 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 1 2 46 cmpt 
 |-  ( c e. Cat |-> { h | ( h C_cat ( Homf ` 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 0 47 wceq 
 |-  Subcat = ( c e. Cat |-> { h | ( h C_cat ( Homf ` 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 ) ) ) } )