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 ∈ LMod | ∀ i ∈ LSubSp ⁡ w w ↾ 𝑠 i ∈ LFinGen

Detailed syntax breakdown

Step Hyp Ref Expression
0 clnm class LNoeM
1 vw setvar w
2 clmod class LMod
3 vi setvar i
4 clss class LSubSp
5 1 cv setvar w
6 5 4 cfv class LSubSp ⁡ w
7 cress class ↾ 𝑠
8 3 cv setvar i
9 5 8 7 co class w ↾ 𝑠 i
10 clfig class LFinGen
11 9 10 wcel wff w ↾ 𝑠 i ∈ LFinGen
12 11 3 6 wral wff ∀ i ∈ LSubSp ⁡ w w ↾ 𝑠 i ∈ LFinGen
13 12 1 2 crab class w ∈ LMod | ∀ i ∈ LSubSp ⁡ w w ↾ 𝑠 i ∈ LFinGen
14 0 13 wceq wff LNoeM = w ∈ LMod | ∀ i ∈ LSubSp ⁡ w w ↾ 𝑠 i ∈ LFinGen