Description: Base set of a ZZ module. (Contributed by Mario Carneiro, 2Oct2015)
Ref  Expression  

Hypotheses  zlmbas.w   W = ( ZMod ` G ) 

zlmbas.2   B = ( Base ` G ) 

Assertion  zlmbas   B = ( Base ` W ) 
Step  Hyp  Ref  Expression 

1  zlmbas.w   W = ( ZMod ` G ) 

2  zlmbas.2   B = ( Base ` G ) 

3  dfbase   Base = Slot 1 

4  1nn   1 e. NN 

5  1lt5   1 < 5 

6  1 3 4 5  zlmlem   ( Base ` G ) = ( Base ` W ) 
7  2 6  eqtri   B = ( Base ` W ) 