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

Definition df-subc 14013
 Description: Subcat is the set of all the subcategory specifications of the category . Like df-subg 14942, this is not actually a collection of categories, but only sets which when given operations from the base category (using df-resc 14012) 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 cat f comp
Distinct variable group:   ,,,,,,,

Detailed syntax breakdown of Definition df-subc
StepHypRef Expression
1 csubc 14010 . 2 Subcat
2 vc . . 3
3 ccat 13890 . . 3
4 vh . . . . . . 7
54cv 1652 . . . . . 6
62cv 1652 . . . . . . 7
7 chomf 13892 . . . . . . 7 f
86, 7cfv 5455 . . . . . 6 f
9 cssc 14008 . . . . . 6 cat
105, 8, 9wbr 4213 . . . . 5 cat f
11 vx . . . . . . . . . . 11
1211cv 1652 . . . . . . . . . 10
13 ccid 13891 . . . . . . . . . . 11
146, 13cfv 5455 . . . . . . . . . 10
1512, 14cfv 5455 . . . . . . . . 9
1612, 12, 5co 6082 . . . . . . . . 9
1715, 16wcel 1726 . . . . . . . 8
18 vg . . . . . . . . . . . . . . 15
1918cv 1652 . . . . . . . . . . . . . 14
20 vf . . . . . . . . . . . . . . 15
2120cv 1652 . . . . . . . . . . . . . 14
22 vy . . . . . . . . . . . . . . . . 17
2322cv 1652 . . . . . . . . . . . . . . . 16
2412, 23cop 3818 . . . . . . . . . . . . . . 15
25 vz . . . . . . . . . . . . . . . 16
2625cv 1652 . . . . . . . . . . . . . . 15
27 cco 13542 . . . . . . . . . . . . . . . 16 comp
286, 27cfv 5455 . . . . . . . . . . . . . . 15 comp
2924, 26, 28co 6082 . . . . . . . . . . . . . 14 comp
3019, 21, 29co 6082 . . . . . . . . . . . . 13 comp
3112, 26, 5co 6082 . . . . . . . . . . . . 13
3230, 31wcel 1726 . . . . . . . . . . . 12 comp
3323, 26, 5co 6082 . . . . . . . . . . . 12
3432, 18, 33wral 2706 . . . . . . . . . . 11 comp
3512, 23, 5co 6082 . . . . . . . . . . 11
3634, 20, 35wral 2706 . . . . . . . . . 10 comp
37 vs . . . . . . . . . . 11
3837cv 1652 . . . . . . . . . 10
3936, 25, 38wral 2706 . . . . . . . . 9 comp
4039, 22, 38wral 2706 . . . . . . . 8 comp
4117, 40wa 360 . . . . . . 7 comp
4241, 11, 38wral 2706 . . . . . 6 comp
435cdm 4879 . . . . . . 7
4443cdm 4879 . . . . . 6
4542, 37, 44wsbc 3162 . . . . 5 comp
4610, 45wa 360 . . . 4 cat f comp
4746, 4cab 2423 . . 3 cat f comp
482, 3, 47cmpt 4267 . 2 cat f comp
491, 48wceq 1653 1 Subcat cat f comp
 Colors of variables: wff set class This definition is referenced by:  subcrcl  14017  issubc  14036
 Copyright terms: Public domain W3C validator