Metamath Proof Explorer

Theorem fz0ssnn0

Description: Finite sets of sequential nonnegative integers starting with 0 are subsets of NN0. (Contributed by JJ, 1-Jun-2021)

Ref Expression
Assertion fz0ssnn0 
|- ( 0 ... N ) C_ NN0

Proof

Step Hyp Ref Expression
1 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
2 1 ssriv 
 |-  ( 0 ... N ) C_ NN0