Definition df-lnm 40901

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 = {𝑤 ∈ LMod ∣ ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤 ↾s 𝑖) ∈ LFinGen}

Distinct variable group:   𝑤,𝑖

Detailed syntax breakdown of Definition df-lnm

Step	Hyp	Ref	Expression
1		clnm 40900	. 2 class LNoeM
2		vw	. . . . . . 7 setvar 𝑤
3	2	cv 1538	. . . . . 6 class 𝑤
4		vi	. . . . . . 7 setvar 𝑖
5	4	cv 1538	. . . . . 6 class 𝑖
6		cress 16941	. . . . . 6 class ↾s
7	3, 5, 6	co 7275	. . . . 5 class (𝑤 ↾s 𝑖)
8		clfig 40892	. . . . 5 class LFinGen
9	7, 8	wcel 2106	. . . 4 wff (𝑤 ↾s 𝑖) ∈ LFinGen
10		clss 20193	. . . . 5 class LSubSp
11	3, 10	cfv 6433	. . . 4 class (LSubSp‘𝑤)
12	9, 4, 11	wral 3064	. . 3 wff ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤 ↾s 𝑖) ∈ LFinGen
13		clmod 20123	. . 3 class LMod
14	12, 2, 13	crab 3068	. 2 class {𝑤 ∈ LMod ∣ ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤 ↾s 𝑖) ∈ LFinGen}
15	1, 14	wceq 1539	1 wff LNoeM = {𝑤 ∈ LMod ∣ ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤 ↾s 𝑖) ∈ LFinGen}

This definition is referenced by:  islnm  40902