Definition df-lfig 37638

Description: Define the class of finitely generated left modules. Finite generation of subspaces can be intepreted using ↾_s. (Contributed by Stefan O'Rear, 1-Jan-2015.)

Assertion

Ref	Expression
df-lfig	|- LFinGen = { w e. LMod | ( Base ` w ) e. ( ( LSpan ` w ) " ( ~P ( Base ` w ) i^i Fin ) ) }

Detailed syntax breakdown of Definition df-lfig

Step	Hyp	Ref	Expression
1		clfig 37637	. 2 class LFinGen
2		vw	. . . . . 6 setvar w
3	2	cv 1482	. . . . 5 class w
4		cbs 15857	. . . . 5 class Base
5	3, 4	cfv 5888	. . . 4 class ( Base ` w )
6		clspn 18971	. . . . . 6 class LSpan
7	3, 6	cfv 5888	. . . . 5 class ( LSpan ` w )
8	5	cpw 4158	. . . . . 6 class ~P ( Base ` w )
9		cfn 7955	. . . . . 6 class Fin
10	8, 9	cin 3573	. . . . 5 class ( ~P ( Base ` w ) i^i Fin )
11	7, 10	cima 5117	. . . 4 class ( ( LSpan ` w ) " ( ~P ( Base ` w ) i^i Fin ) )
12	5, 11	wcel 1990	. . 3 wff ( Base ` w ) e. ( ( LSpan ` w ) " ( ~P ( Base ` w ) i^i Fin ) )
13		clmod 18863	. . 3 class LMod
14	12, 2, 13	crab 2916	. 2 class { w e. LMod | ( Base ` w ) e. ( ( LSpan ` w ) " ( ~P ( Base ` w ) i^i Fin ) ) }
15	1, 14	wceq 1483	1 wff LFinGen = { w e. LMod | ( Base ` w ) e. ( ( LSpan ` w ) " ( ~P ( Base ` w ) i^i Fin ) ) }

This definition is referenced by:  islmodfg  37639  fglmod  37643