Metamath Proof Explorer

Theorem fglmod

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

Ref Expression
Assertion fglmod 
|- ( M e. LFinGen -> M e. LMod )

Proof

Step Hyp Ref Expression
1 df-lfig 
 |-  LFinGen = { a e. LMod | ( Base ` a ) e. ( ( LSpan ` a ) " ( ~P ( Base ` a ) i^i Fin ) ) }
2 1 ssrab3 
 |-  LFinGen C_ LMod
3 2 sseli 
 |-  ( M e. LFinGen -> M e. LMod )