Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-subsmg Unicode version

Definition df-subsmg 25487
Description: Define the set of subsemigroups of  g. Experimental. (Contributed by FL, 2-Sep-2013.)
Assertion
Ref Expression
df-subsmg  |-  SubSemiGrp  =  (
g  e.  SemiGrp  |->  { h  e.  SemiGrp  |  h  C_  g } )
Distinct variable group:    g, h

Detailed syntax breakdown of Definition df-subsmg
StepHypRef Expression
1 csubsmg 25486 . 2  class  SubSemiGrp
2 vg . . 3  set  g
3 csem 21013 . . 3  class  SemiGrp
4 vh . . . . . 6  set  h
54cv 1631 . . . . 5  class  h
62cv 1631 . . . . 5  class  g
75, 6wss 3165 . . . 4  wff  h  C_  g
87, 4, 3crab 2560 . . 3  class  { h  e.  SemiGrp  |  h  C_  g }
92, 3, 8cmpt 4093 . 2  class  ( g  e.  SemiGrp  |->  { h  e.  SemiGrp  |  h  C_  g } )
101, 9wceq 1632 1  wff  SubSemiGrp  =  (
g  e.  SemiGrp  |->  { h  e.  SemiGrp  |  h  C_  g } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator