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 ) |
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 ) |