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

Definition df-ssc 13687
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 13689, 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  |-  C_cat  =  { <. h ,  j >.  |  E. t ( j  Fn  ( t  X.  t )  /\  E. s  e.  ~P  t
h  e.  X_ x  e.  ( s  X.  s
) ~P ( j `
 x ) ) }
Distinct variable group:    h, j, s, t, x

Detailed syntax breakdown of Definition df-ssc
StepHypRef Expression
1 cssc 13684 . 2  class  C_cat
2 vj . . . . . . 7  set  j
32cv 1622 . . . . . 6  class  j
4 vt . . . . . . . 8  set  t
54cv 1622 . . . . . . 7  class  t
65, 5cxp 4687 . . . . . 6  class  ( t  X.  t )
73, 6wfn 5250 . . . . 5  wff  j  Fn  ( t  X.  t
)
8 vh . . . . . . . 8  set  h
98cv 1622 . . . . . . 7  class  h
10 vx . . . . . . . 8  set  x
11 vs . . . . . . . . . 10  set  s
1211cv 1622 . . . . . . . . 9  class  s
1312, 12cxp 4687 . . . . . . . 8  class  ( s  X.  s )
1410cv 1622 . . . . . . . . . 10  class  x
1514, 3cfv 5255 . . . . . . . . 9  class  ( j `
 x )
1615cpw 3625 . . . . . . . 8  class  ~P (
j `  x )
1710, 13, 16cixp 6817 . . . . . . 7  class  X_ x  e.  ( s  X.  s
) ~P ( j `
 x )
189, 17wcel 1684 . . . . . 6  wff  h  e.  X_ x  e.  (
s  X.  s ) ~P ( j `  x )
195cpw 3625 . . . . . 6  class  ~P t
2018, 11, 19wrex 2544 . . . . 5  wff  E. s  e.  ~P  t h  e.  X_ x  e.  (
s  X.  s ) ~P ( j `  x )
217, 20wa 358 . . . 4  wff  ( j  Fn  ( t  X.  t )  /\  E. s  e.  ~P  t
h  e.  X_ x  e.  ( s  X.  s
) ~P ( j `
 x ) )
2221, 4wex 1528 . . 3  wff  E. t
( j  Fn  (
t  X.  t )  /\  E. s  e. 
~P  t h  e.  X_ x  e.  (
s  X.  s ) ~P ( j `  x ) )
2322, 8, 2copab 4076 . 2  class  { <. h ,  j >.  |  E. t ( j  Fn  ( t  X.  t
)  /\  E. s  e.  ~P  t h  e.  X_ x  e.  (
s  X.  s ) ~P ( j `  x ) ) }
241, 23wceq 1623 1  wff  C_cat  =  { <. h ,  j >.  |  E. t ( j  Fn  ( t  X.  t )  /\  E. s  e.  ~P  t
h  e.  X_ x  e.  ( s  X.  s
) ~P ( j `
 x ) ) }
Colors of variables: wff set class
This definition is referenced by:  sscrel  13690  brssc  13691
  Copyright terms: Public domain W3C validator