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 27174
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 27173 . 2  class LNoeM
2 vw . . . . . . 7  set  w
32cv 1622 . . . . . 6  class  w
4 vi . . . . . . 7  set  i
54cv 1622 . . . . . 6  class  i
6 cress 13149 . . . . . 6  classs
73, 5, 6co 5858 . . . . 5  class  ( ws  i )
8 clfig 27165 . . . . 5  class LFinGen
97, 8wcel 1684 . . . 4  wff  ( ws  i )  e. LFinGen
10 clss 15689 . . . . 5  class  LSubSp
113, 10cfv 5255 . . . 4  class  ( LSubSp `  w )
129, 4, 11wral 2543 . . 3  wff  A. i  e.  ( LSubSp `  w )
( ws  i )  e. LFinGen
13 clmod 15627 . . 3  class  LMod
1412, 2, 13crab 2547 . 2  class  { w  e.  LMod  |  A. i  e.  ( LSubSp `  w )
( ws  i )  e. LFinGen }
151, 14wceq 1623 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  27175
  Copyright terms: Public domain W3C validator