Definition df-lnr 43101

Description: A ring is left-Noetherian iff it is Noetherian as a left module over itself. (Contributed by Stefan O'Rear, 24-Jan-2015.)

Assertion

Ref	Expression
df-lnr	⊢ LNoeR = {𝑎 ∈ Ring ∣ (ringLMod‘𝑎) ∈ LNoeM}

Detailed syntax breakdown of Definition df-lnr

Step	Hyp	Ref	Expression
1		clnr 43100	. 2 class LNoeR
2		va	. . . . . 6 setvar 𝑎
3	2	cv 1539	. . . . 5 class 𝑎
4		crglmod 21135	. . . . 5 class ringLMod
5	3, 4	cfv 6536	. . . 4 class (ringLMod‘𝑎)
6		clnm 43066	. . . 4 class LNoeM
7	5, 6	wcel 2109	. . 3 wff (ringLMod‘𝑎) ∈ LNoeM
8		crg 20198	. . 3 class Ring
9	7, 2, 8	crab 3420	. 2 class {𝑎 ∈ Ring ∣ (ringLMod‘𝑎) ∈ LNoeM}
10	1, 9	wceq 1540	1 wff LNoeR = {𝑎 ∈ Ring ∣ (ringLMod‘𝑎) ∈ LNoeM}

This definition is referenced by:  islnr  43102