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

Definition df-sggen 25386
Description: the subsemigroup of  g generated by  x. Experimental. (Contributed by FL, 15-Jul-2012.)
Assertion
Ref Expression
df-sggen  |-  subSemiGrpGen  =  ( g  e.  SemiGrp ,  x  e. 
~P dom  dom  g  |->  |^|
{ h  e.  ( SubSemiGrp `  g )  |  x 
C_  dom  dom  h }
)
Distinct variable group:    x, g, h

Detailed syntax breakdown of Definition df-sggen
StepHypRef Expression
1 csbsgrg 25385 . 2  class  subSemiGrpGen
2 vg . . 3  set  g
3 vx . . 3  set  x
4 csem 20997 . . 3  class  SemiGrp
52cv 1622 . . . . . 6  class  g
65cdm 4689 . . . . 5  class  dom  g
76cdm 4689 . . . 4  class  dom  dom  g
87cpw 3625 . . 3  class  ~P dom  dom  g
93cv 1622 . . . . . 6  class  x
10 vh . . . . . . . . 9  set  h
1110cv 1622 . . . . . . . 8  class  h
1211cdm 4689 . . . . . . 7  class  dom  h
1312cdm 4689 . . . . . 6  class  dom  dom  h
149, 13wss 3152 . . . . 5  wff  x  C_  dom  dom  h
15 csubsmg 25383 . . . . . 6  class  SubSemiGrp
165, 15cfv 5255 . . . . 5  class  ( SubSemiGrp `  g )
1714, 10, 16crab 2547 . . . 4  class  { h  e.  ( SubSemiGrp `  g )  |  x  C_  dom  dom  h }
1817cint 3862 . . 3  class  |^| { h  e.  ( SubSemiGrp `  g )  |  x  C_  dom  dom  h }
192, 3, 4, 8, 18cmpt2 5860 . 2  class  ( g  e.  SemiGrp ,  x  e. 
~P dom  dom  g  |->  |^|
{ h  e.  ( SubSemiGrp `  g )  |  x 
C_  dom  dom  h }
)
201, 19wceq 1623 1  wff  subSemiGrpGen  =  ( g  e.  SemiGrp ,  x  e. 
~P dom  dom  g  |->  |^|
{ h  e.  ( SubSemiGrp `  g )  |  x 
C_  dom  dom  h }
)
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator