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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clnm	⊢ LNoeM
1		vw	⊢ 𝑤
2		clmod	⊢ LMod
3		vi	⊢ 𝑖
4		clss	⊢ LSubSp
5	1	cv	⊢ 𝑤
6	5 4	cfv	⊢ ( LSubSp ‘ 𝑤 )
7		cress	⊢ ↾s
8	3	cv	⊢ 𝑖
9	5 8 7	co	⊢ ( 𝑤 ↾s 𝑖 )
10		clfig	⊢ LFinGen
11	9 10	wcel	⊢ ( 𝑤 ↾s 𝑖 ) ∈ LFinGen
12	11 3 6	wral	⊢ ∀ 𝑖 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑤 ↾s 𝑖 ) ∈ LFinGen
13	12 1 2	crab	⊢ { 𝑤 ∈ LMod ∣ ∀ 𝑖 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑤 ↾s 𝑖 ) ∈ LFinGen }
14	0 13	wceq	⊢ LNoeM = { 𝑤 ∈ LMod ∣ ∀ 𝑖 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑤 ↾s 𝑖 ) ∈ LFinGen }