Description: Subset relationship for finite sets of sequential integers. (Contributed by Glauco Siliprandi, 5Apr2020)
Ref  Expression  

Assertion  fz1ssfz0   ( 1 ... N ) C_ ( 0 ... N ) 
Step  Hyp  Ref  Expression 

1  1e0p1   1 = ( 0 + 1 ) 

2  1  oveq1i   ( 1 ... N ) = ( ( 0 + 1 ) ... N ) 
3  0z   0 e. ZZ 

4  fzp1ss   ( 0 e. ZZ > ( ( 0 + 1 ) ... N ) C_ ( 0 ... N ) ) 

5  3 4  axmp   ( ( 0 + 1 ) ... N ) C_ ( 0 ... N ) 
6  2 5  eqsstri   ( 1 ... N ) C_ ( 0 ... N ) 