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: is the set of all the subcategories of the 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.)
Assertion
Ref Expression
df-subcat

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