Definition df-lfig

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)

	Ref	Expression
Assertion	df-lfig	$$⊢\mathrm{LFinGen}=\left\{w\in \mathrm{LMod}|{\mathrm{Base}}_w\in \mathrm{LSpan}\left(w\right)\left[𝒫{\mathrm{Base}}_w\cap \mathrm{Fin}\right]\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clfig	$$class\mathrm{LFinGen}$$
1		vw	$$setvarw$$
2		clmod	$$class\mathrm{LMod}$$
3		cbs	$$class\mathrm{Base}$$
4	1	cv	$$setvarw$$
5	4 3	cfv	$$class{\mathrm{Base}}_w$$
6		clspn	$$class\mathrm{LSpan}$$
7	4 6	cfv	$$class\mathrm{LSpan}\left(w\right)$$
8	5	cpw	$$class𝒫{\mathrm{Base}}_w$$
9		cfn	$$class\mathrm{Fin}$$
10	8 9	cin	$$class\left(𝒫{\mathrm{Base}}_w\cap \mathrm{Fin}\right)$$
11	7 10	cima	$$class\mathrm{LSpan}\left(w\right)\left[𝒫{\mathrm{Base}}_w\cap \mathrm{Fin}\right]$$
12	5 11	wcel	$$wff{\mathrm{Base}}_w\in \mathrm{LSpan}\left(w\right)\left[𝒫{\mathrm{Base}}_w\cap \mathrm{Fin}\right]$$
13	12 1 2	crab	$$class\left\{w\in \mathrm{LMod}|{\mathrm{Base}}_w\in \mathrm{LSpan}\left(w\right)\left[𝒫{\mathrm{Base}}_w\cap \mathrm{Fin}\right]\right\}$$
14	0 13	wceq	$$wff\mathrm{LFinGen}=\left\{w\in \mathrm{LMod}|{\mathrm{Base}}_w\in \mathrm{LSpan}\left(w\right)\left[𝒫{\mathrm{Base}}_w\cap \mathrm{Fin}\right]\right\}$$