Definition df-lnr

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clnr	⊢ LNoeR
1		va	⊢ 𝑎
2		crg	⊢ Ring
3		crglmod	⊢ ringLMod
4	1	cv	⊢ 𝑎
5	4 3	cfv	⊢ ( ringLMod ‘ 𝑎 )
6		clnm	⊢ LNoeM
7	5 6	wcel	⊢ ( ringLMod ‘ 𝑎 ) ∈ LNoeM
8	7 1 2	crab	⊢ { 𝑎 ∈ Ring ∣ ( ringLMod ‘ 𝑎 ) ∈ LNoeM }
9	0 8	wceq	⊢ LNoeR = { 𝑎 ∈ Ring ∣ ( ringLMod ‘ 𝑎 ) ∈ LNoeM }