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

Definition df-ssc 14012
 Description: Define the subset relation for subcategories. Despite the name, this is not really a "category-aware" definition, which is to say it makes no explicit references to homsets or composition; instead this is a subset-like relation on the functions that are used as subcategory specifications in df-subc 14014, which makes it play an analogous role to the subset relation applied to the subgroups of a group. (Contributed by Mario Carneiro, 6-Jan-2017.)
Assertion
Ref Expression
df-ssc cat
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-ssc
StepHypRef Expression
1 cssc 14009 . 2 cat
2 vj . . . . . . 7
32cv 1652 . . . . . 6
4 vt . . . . . . . 8
54cv 1652 . . . . . . 7
65, 5cxp 4878 . . . . . 6
73, 6wfn 5451 . . . . 5
8 vh . . . . . . . 8
98cv 1652 . . . . . . 7
10 vx . . . . . . . 8
11 vs . . . . . . . . . 10
1211cv 1652 . . . . . . . . 9
1312, 12cxp 4878 . . . . . . . 8
1410cv 1652 . . . . . . . . . 10
1514, 3cfv 5456 . . . . . . . . 9
1615cpw 3801 . . . . . . . 8
1710, 13, 16cixp 7065 . . . . . . 7
189, 17wcel 1726 . . . . . 6
195cpw 3801 . . . . . 6
2018, 11, 19wrex 2708 . . . . 5
217, 20wa 360 . . . 4
2221, 4wex 1551 . . 3
2322, 8, 2copab 4267 . 2
241, 23wceq 1653 1 cat
 Colors of variables: wff set class This definition is referenced by:  sscrel  14015  brssc  14016
 Copyright terms: Public domain W3C validator