Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lnm Structured version   Unicode version

Definition df-lnm 27151
Description: A left-module is Noetherian iff it is hereditarily finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.)
Assertion
Ref Expression
df-lnm  |- LNoeM  =  {
w  e.  LMod  |  A. i  e.  ( LSubSp `  w ) ( ws  i )  e. LFinGen }
Distinct variable group:    w, i

Detailed syntax breakdown of Definition df-lnm
StepHypRef Expression
1 clnm 27150 . 2  class LNoeM
2 vw . . . . . . 7  set  w
32cv 1651 . . . . . 6  class  w
4 vi . . . . . . 7  set  i
54cv 1651 . . . . . 6  class  i
6 cress 13470 . . . . . 6  classs
73, 5, 6co 6081 . . . . 5  class  ( ws  i )
8 clfig 27142 . . . . 5  class LFinGen
97, 8wcel 1725 . . . 4  wff  ( ws  i )  e. LFinGen
10 clss 16008 . . . . 5  class  LSubSp
113, 10cfv 5454 . . . 4  class  ( LSubSp `  w )
129, 4, 11wral 2705 . . 3  wff  A. i  e.  ( LSubSp `  w )
( ws  i )  e. LFinGen
13 clmod 15950 . . 3  class  LMod
1412, 2, 13crab 2709 . 2  class  { w  e.  LMod  |  A. i  e.  ( LSubSp `  w )
( ws  i )  e. LFinGen }
151, 14wceq 1652 1  wff LNoeM  =  {
w  e.  LMod  |  A. i  e.  ( LSubSp `  w ) ( ws  i )  e. LFinGen }
Colors of variables: wff set class
This definition is referenced by:  islnm  27152
  Copyright terms: Public domain W3C validator