Definition df-lnm 37646

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 ) ( w ↾s i ) e. LFinGen }

Distinct variable group:   w, i

Detailed syntax breakdown of Definition df-lnm

Step	Hyp	Ref	Expression
1		clnm 37645	. 2 class LNoeM
2		vw	. . . . . . 7 setvar w
3	2	cv 1482	. . . . . 6 class w
4		vi	. . . . . . 7 setvar i
5	4	cv 1482	. . . . . 6 class i
6		cress 15858	. . . . . 6 class ↾s
7	3, 5, 6	co 6650	. . . . 5 class ( w ↾s i )
8		clfig 37637	. . . . 5 class LFinGen
9	7, 8	wcel 1990	. . . 4 wff ( w ↾s i ) e. LFinGen
10		clss 18932	. . . . 5 class LSubSp
11	3, 10	cfv 5888	. . . 4 class ( LSubSp ` w )
12	9, 4, 11	wral 2912	. . 3 wff A. i e. ( LSubSp ` w ) ( w ↾s i ) e. LFinGen
13		clmod 18863	. . 3 class LMod
14	12, 2, 13	crab 2916	. 2 class { w e. LMod | A. i e. ( LSubSp ` w ) ( w ↾s i ) e. LFinGen }
15	1, 14	wceq 1483	1 wff LNoeM = { w e. LMod | A. i e. ( LSubSp ` w ) ( w ↾s i ) e. LFinGen }

This definition is referenced by:  islnm  37647