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 \in LMod \| \forall i \in LSubSp (w) w ↾_{𝑠} i \in LFinGen\}$

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 \in LFinGen$
12	11 3 6	wral	$wff \forall i \in LSubSp (w) w ↾_{𝑠} i \in LFinGen$
13	12 1 2	crab	$class \{w \in LMod \| \forall i \in LSubSp (w) w ↾_{𝑠} i \in LFinGen\}$
14	0 13	wceq	$wff LNoeM = \{w \in LMod \| \forall i \in LSubSp (w) w ↾_{𝑠} i \in LFinGen\}$

Metamath Proof Explorer