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 30998
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 30997 . 2  class LNoeM
2 vw . . . . . . 7  setvar  w
32cv 1382 . . . . . 6  class  w
4 vi . . . . . . 7  setvar  i
54cv 1382 . . . . . 6  class  i
6 cress 14615 . . . . . 6  classs
73, 5, 6co 6281 . . . . 5  class  ( ws  i )
8 clfig 30989 . . . . 5  class LFinGen
97, 8wcel 1804 . . . 4  wff  ( ws  i )  e. LFinGen
10 clss 17557 . . . . 5  class  LSubSp
113, 10cfv 5578 . . . 4  class  ( LSubSp `  w )
129, 4, 11wral 2793 . . 3  wff  A. i  e.  ( LSubSp `  w )
( ws  i )  e. LFinGen
13 clmod 17491 . . 3  class  LMod
1412, 2, 13crab 2797 . 2  class  { w  e.  LMod  |  A. i  e.  ( LSubSp `  w )
( ws  i )  e. LFinGen }
151, 14wceq 1383 1  wff LNoeM  =  {
w  e.  LMod  |  A. i  e.  ( LSubSp `  w ) ( ws  i )  e. LFinGen }
Colors of variables: wff setvar class
This definition is referenced by:  islnm  30999
  Copyright terms: Public domain W3C validator