Definition df-lfig

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clfig	|- LFinGen
1		vw	|- w
2		clmod	|- LMod
3		cbs	|- Base
4	1	cv	|- w
5	4 3	cfv	|- ( Base ` w )
6		clspn	|- LSpan
7	4 6	cfv	|- ( LSpan ` w )
8	5	cpw	|- ~P ( Base ` w )
9		cfn	|- Fin
10	8 9	cin	|- ( ~P ( Base ` w ) i^i Fin )
11	7 10	cima	|- ( ( LSpan ` w ) " ( ~P ( Base ` w ) i^i Fin ) )
12	5 11	wcel	|- ( Base ` w ) e. ( ( LSpan ` w ) " ( ~P ( Base ` w ) i^i Fin ) )
13	12 1 2	crab	|- { w e. LMod | ( Base ` w ) e. ( ( LSpan ` w ) " ( ~P ( Base ` w ) i^i Fin ) ) }
14	0 13	wceq	|- LFinGen = { w e. LMod | ( Base ` w ) e. ( ( LSpan ` w ) " ( ~P ( Base ` w ) i^i Fin ) ) }