Theorem fz2ssnn0

Description: A finite set of sequential integers that is a subset of NN0 . (Contributed by Thierry Arnoux, 8-Dec-2021)

	Ref	Expression
Assertion	fz2ssnn0	|- ( M e. NN0 -> ( M ... N ) C_ NN0 )

Proof

Step	Hyp	Ref	Expression
1		fzssuz	|- ( M ... N ) C_ ( ZZ>= ` M )
2		nn0uz	|- NN0 = ( ZZ>= ` 0 )
3	2	eleq2i	|- ( M e. NN0 <-> M e. ( ZZ>= ` 0 ) )
4	3	biimpi	|- ( M e. NN0 -> M e. ( ZZ>= ` 0 ) )
5		uzss	|- ( M e. ( ZZ>= ` 0 ) -> ( ZZ>= ` M ) C_ ( ZZ>= ` 0 ) )
6	4 5	syl	|- ( M e. NN0 -> ( ZZ>= ` M ) C_ ( ZZ>= ` 0 ) )
7	6 2	sseqtrrdi	|- ( M e. NN0 -> ( ZZ>= ` M ) C_ NN0 )
8	1 7	sstrid	|- ( M e. NN0 -> ( M ... N ) C_ NN0 )