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 = { 𝑤 ∈ LMod ∣ ( Base ‘ 𝑤 ) ∈ ( ( LSpan ‘ 𝑤 ) “ ( 𝒫 ( Base ‘ 𝑤 ) ∩ Fin ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clfig	⊢ LFinGen
1		vw	⊢ 𝑤
2		clmod	⊢ LMod
3		cbs	⊢ Base
4	1	cv	⊢ 𝑤
5	4 3	cfv	⊢ ( Base ‘ 𝑤 )
6		clspn	⊢ LSpan
7	4 6	cfv	⊢ ( LSpan ‘ 𝑤 )
8	5	cpw	⊢ 𝒫 ( Base ‘ 𝑤 )
9		cfn	⊢ Fin
10	8 9	cin	⊢ ( 𝒫 ( Base ‘ 𝑤 ) ∩ Fin )
11	7 10	cima	⊢ ( ( LSpan ‘ 𝑤 ) “ ( 𝒫 ( Base ‘ 𝑤 ) ∩ Fin ) )
12	5 11	wcel	⊢ ( Base ‘ 𝑤 ) ∈ ( ( LSpan ‘ 𝑤 ) “ ( 𝒫 ( Base ‘ 𝑤 ) ∩ Fin ) )
13	12 1 2	crab	⊢ { 𝑤 ∈ LMod ∣ ( Base ‘ 𝑤 ) ∈ ( ( LSpan ‘ 𝑤 ) “ ( 𝒫 ( Base ‘ 𝑤 ) ∩ Fin ) ) }
14	0 13	wceq	⊢ LFinGen = { 𝑤 ∈ LMod ∣ ( Base ‘ 𝑤 ) ∈ ( ( LSpan ‘ 𝑤 ) “ ( 𝒫 ( Base ‘ 𝑤 ) ∩ Fin ) ) }