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

Definition df-ssc 15225
 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 15227, 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 15222 . 2 cat
2 vj . . . . . . 7
32cv 1394 . . . . . 6
4 vt . . . . . . . 8
54cv 1394 . . . . . . 7
65, 5cxp 5006 . . . . . 6
73, 6wfn 5589 . . . . 5
8 vh . . . . . . . 8
98cv 1394 . . . . . . 7
10 vx . . . . . . . 8
11 vs . . . . . . . . . 10
1211cv 1394 . . . . . . . . 9
1312, 12cxp 5006 . . . . . . . 8
1410cv 1394 . . . . . . . . . 10
1514, 3cfv 5594 . . . . . . . . 9
1615cpw 4015 . . . . . . . 8
1710, 13, 16cixp 7488 . . . . . . 7
189, 17wcel 1819 . . . . . 6
195cpw 4015 . . . . . 6
2018, 11, 19wrex 2808 . . . . 5
217, 20wa 369 . . . 4
2221, 4wex 1613 . . 3
2322, 8, 2copab 4514 . 2
241, 23wceq 1395 1 cat
 Colors of variables: wff setvar class This definition is referenced by:  sscrel  15228  brssc  15229
 Copyright terms: Public domain W3C validator