Metamath Proof Explorer

Theorem fzssnn0

Description: A finite set of sequential integers that is a subset of NN0 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 fzssuz 
 |-  ( 0 ... N ) C_ ( ZZ>= ` 0 )
2 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
3 2 eqcomi 
 |-  ( ZZ>= ` 0 ) = NN0
4 1 3 sseqtri 
 |-  ( 0 ... N ) C_ NN0