Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-subcat Unicode version

Definition df-subcat 25844
Description:  ( 
SubCat  `  x ) is the set of all the subcategories of the category  x. 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.)
Assertion
Ref Expression
df-subcat  |-  SubCat  =  ( x  e.  Cat OLD  |->  (  Cat OLD  i^i  (
( ~P ( dom_ `  x )  X.  ~P ( cod_ `  x )
)  X.  ( ~P ( id_ `  x
)  X.  ~P (
o_ `  x )
) ) ) )

Detailed syntax breakdown of Definition df-subcat
StepHypRef Expression
1 csubcat 25843 . 2  class  SubCat
2 vx . . 3  set  x
3 ccatOLD 25752 . . 3  class  Cat OLD
42cv 1622 . . . . . . . 8  class  x
5 cdom_ 25712 . . . . . . . 8  class  dom_
64, 5cfv 5255 . . . . . . 7  class  ( dom_ `  x )
76cpw 3625 . . . . . 6  class  ~P ( dom_ `  x )
8 ccod_ 25713 . . . . . . . 8  class  cod_
94, 8cfv 5255 . . . . . . 7  class  ( cod_ `  x )
109cpw 3625 . . . . . 6  class  ~P ( cod_ `  x )
117, 10cxp 4687 . . . . 5  class  ( ~P ( dom_ `  x
)  X.  ~P ( cod_ `  x ) )
12 cid_ 25714 . . . . . . . 8  class  id_
134, 12cfv 5255 . . . . . . 7  class  ( id_ `  x )
1413cpw 3625 . . . . . 6  class  ~P ( id_ `  x )
15 co_ 25715 . . . . . . . 8  class  o_
164, 15cfv 5255 . . . . . . 7  class  ( o_
`  x )
1716cpw 3625 . . . . . 6  class  ~P (
o_ `  x )
1814, 17cxp 4687 . . . . 5  class  ( ~P ( id_ `  x
)  X.  ~P (
o_ `  x )
)
1911, 18cxp 4687 . . . 4  class  ( ( ~P ( dom_ `  x
)  X.  ~P ( cod_ `  x ) )  X.  ( ~P ( id_ `  x )  X. 
~P ( o_ `  x ) ) )
203, 19cin 3151 . . 3  class  (  Cat
OLD  i^i  ( ( ~P ( dom_ `  x
)  X.  ~P ( cod_ `  x ) )  X.  ( ~P ( id_ `  x )  X. 
~P ( o_ `  x ) ) ) )
212, 3, 20cmpt 4077 . 2  class  ( x  e.  Cat OLD  |->  (  Cat OLD  i^i  (
( ~P ( dom_ `  x )  X.  ~P ( cod_ `  x )
)  X.  ( ~P ( id_ `  x
)  X.  ~P (
o_ `  x )
) ) ) )
221, 21wceq 1623 1  wff  SubCat  =  ( x  e.  Cat OLD  |->  (  Cat OLD  i^i  (
( ~P ( dom_ `  x )  X.  ~P ( cod_ `  x )
)  X.  ( ~P ( id_ `  x
)  X.  ~P (
o_ `  x )
) ) ) )
Colors of variables: wff set class
This definition is referenced by:  issubcat  25845  besubbeca  25848
  Copyright terms: Public domain W3C validator