Theorem fglmod

Description: Finitely generated left modules are left modules. (Contributed by Stefan O'Rear, 1-Jan-2015)

	Ref	Expression
Assertion	fglmod	⊢ ( 𝑀 ∈ LFinGen → 𝑀 ∈ LMod )

Proof

Step	Hyp	Ref	Expression
1		df-lfig	⊢ LFinGen = { 𝑎 ∈ LMod ∣ ( Base ‘ 𝑎 ) ∈ ( ( LSpan ‘ 𝑎 ) “ ( 𝒫 ( Base ‘ 𝑎 ) ∩ Fin ) ) }
2	1	ssrab3	⊢ LFinGen ⊆ LMod
3	2	sseli	⊢ ( 𝑀 ∈ LFinGen → 𝑀 ∈ LMod )