Metamath Proof Explorer

Definition df-lnm

Description: A left-module isNoetherian iff it is hereditarily finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014)

Ref Expression
Assertion df-lnm 
|- LNoeM = { w e. LMod | A. i e. ( LSubSp ` w ) ( w |`s i ) e. LFinGen }

Detailed syntax breakdown

Step Hyp Ref Expression
0 clnm 
 |-  LNoeM
1 vw 
 |-  w
2 clmod 
 |-  LMod
3 vi 
 |-  i
4 clss 
 |-  LSubSp
5 1 cv 
 |-  w
6 5 4 cfv 
 |-  ( LSubSp ` w )
7 cress 
 |-  |`s
8 3 cv 
 |-  i
9 5 8 7 co 
 |-  ( w |`s i )
10 clfig 
 |-  LFinGen
11 9 10 wcel 
 |-  ( w |`s i ) e. LFinGen
12 11 3 6 wral 
 |-  A. i e. ( LSubSp ` w ) ( w |`s i ) e. LFinGen
13 12 1 2 crab 
 |-  { w e. LMod | A. i e. ( LSubSp ` w ) ( w |`s i ) e. LFinGen }
14 0 13 wceq 
 |-  LNoeM = { w e. LMod | A. i e. ( LSubSp ` w ) ( w |`s i ) e. LFinGen }