MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-subc Unicode version

Definition df-subc 13705
Description:  (Subcat `  C ) is the set of all the subcategory specifications of the category  C. Like df-subg 14634, this is not actually a collection of categories, but only sets which when given operations from the base category (using df-resc 13704) 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  (  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 ) ) ) } )
Distinct variable group:    f, c, g, h, s, x, y, z

Detailed syntax breakdown of Definition df-subc
StepHypRef Expression
1 csubc 13702 . 2  class Subcat
2 vc . . 3  set  c
3 ccat 13582 . . 3  class  Cat
4 vh . . . . . . 7  set  h
54cv 1631 . . . . . 6  class  h
62cv 1631 . . . . . . 7  class  c
7 chomf 13584 . . . . . . 7  class  Homf
86, 7cfv 5271 . . . . . 6  class  (  Homf  `  c )
9 cssc 13700 . . . . . 6  class  C_cat
105, 8, 9wbr 4039 . . . . 5  wff  h  C_cat  (  Homf  `  c )
11 vx . . . . . . . . . . 11  set  x
1211cv 1631 . . . . . . . . . 10  class  x
13 ccid 13583 . . . . . . . . . . 11  class  Id
146, 13cfv 5271 . . . . . . . . . 10  class  ( Id
`  c )
1512, 14cfv 5271 . . . . . . . . 9  class  ( ( Id `  c ) `
 x )
1612, 12, 5co 5874 . . . . . . . . 9  class  ( x h x )
1715, 16wcel 1696 . . . . . . . 8  wff  ( ( Id `  c ) `
 x )  e.  ( x h x )
18 vg . . . . . . . . . . . . . . 15  set  g
1918cv 1631 . . . . . . . . . . . . . 14  class  g
20 vf . . . . . . . . . . . . . . 15  set  f
2120cv 1631 . . . . . . . . . . . . . 14  class  f
22 vy . . . . . . . . . . . . . . . . 17  set  y
2322cv 1631 . . . . . . . . . . . . . . . 16  class  y
2412, 23cop 3656 . . . . . . . . . . . . . . 15  class  <. x ,  y >.
25 vz . . . . . . . . . . . . . . . 16  set  z
2625cv 1631 . . . . . . . . . . . . . . 15  class  z
27 cco 13236 . . . . . . . . . . . . . . . 16  class comp
286, 27cfv 5271 . . . . . . . . . . . . . . 15  class  (comp `  c )
2924, 26, 28co 5874 . . . . . . . . . . . . . 14  class  ( <.
x ,  y >.
(comp `  c )
z )
3019, 21, 29co 5874 . . . . . . . . . . . . 13  class  ( g ( <. x ,  y
>. (comp `  c )
z ) f )
3112, 26, 5co 5874 . . . . . . . . . . . . 13  class  ( x h z )
3230, 31wcel 1696 . . . . . . . . . . . 12  wff  ( g ( <. x ,  y
>. (comp `  c )
z ) f )  e.  ( x h z )
3323, 26, 5co 5874 . . . . . . . . . . . 12  class  ( y h z )
3432, 18, 33wral 2556 . . . . . . . . . . 11  wff  A. g  e.  ( y h z ) ( g (
<. x ,  y >.
(comp `  c )
z ) f )  e.  ( x h z )
3512, 23, 5co 5874 . . . . . . . . . . 11  class  ( x h y )
3634, 20, 35wral 2556 . . . . . . . . . 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  set  s
3837cv 1631 . . . . . . . . . 10  class  s
3936, 25, 38wral 2556 . . . . . . . . 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 )
4039, 22, 38wral 2556 . . . . . . . 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 )
4117, 40wa 358 . . . . . . 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 ) )
4241, 11, 38wral 2556 . . . . . 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 ) )
435cdm 4705 . . . . . . 7  class  dom  h
4443cdm 4705 . . . . . 6  class  dom  dom  h
4542, 37, 44wsbc 3004 . . . . 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 ) )
4610, 45wa 358 . . . 4  wff  ( 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 ) ) )
4746, 4cab 2282 . . 3  class  { 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 ) ) ) }
482, 3, 47cmpt 4093 . 2  class  ( 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 ) ) ) } )
491, 48wceq 1632 1  wff 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 ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  subcrcl  13709  issubc  13728
  Copyright terms: Public domain W3C validator