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

Definition df-lnm 27277
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 27276 . 2  class LNoeM
2 vw . . . . . . 7  set  w
32cv 1631 . . . . . 6  class  w
4 vi . . . . . . 7  set  i
54cv 1631 . . . . . 6  class  i
6 cress 13165 . . . . . 6  classs
73, 5, 6co 5874 . . . . 5  class  ( ws  i )
8 clfig 27268 . . . . 5  class LFinGen
97, 8wcel 1696 . . . 4  wff  ( ws  i )  e. LFinGen
10 clss 15705 . . . . 5  class  LSubSp
113, 10cfv 5271 . . . 4  class  ( LSubSp `  w )
129, 4, 11wral 2556 . . 3  wff  A. i  e.  ( LSubSp `  w )
( ws  i )  e. LFinGen
13 clmod 15643 . . 3  class  LMod
1412, 2, 13crab 2560 . 2  class  { w  e.  LMod  |  A. i  e.  ( LSubSp `  w )
( ws  i )  e. LFinGen }
151, 14wceq 1632 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  27278
  Copyright terms: Public domain W3C validator