Definition df-lnr 43122

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 43121	. 2 class LNoeR
2		va	. . . . . 6 setvar 𝑎
3	2	cv 1539	. . . . 5 class 𝑎
4		crglmod 21171	. . . . 5 class ringLMod
5	3, 4	cfv 6561	. . . 4 class (ringLMod‘𝑎)
6		clnm 43087	. . . 4 class LNoeM
7	5, 6	wcel 2108	. . 3 wff (ringLMod‘𝑎) ∈ LNoeM
8		crg 20230	. . 3 class Ring
9	7, 2, 8	crab 3436	. 2 class {𝑎 ∈ Ring ∣ (ringLMod‘𝑎) ∈ LNoeM}
10	1, 9	wceq 1540	1 wff LNoeR = {𝑎 ∈ Ring ∣ (ringLMod‘𝑎) ∈ LNoeM}

This definition is referenced by:  islnr  43123