Metamath Proof Explorer


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 M0MN0

Proof

Step Hyp Ref Expression
1 fzssuz MNM
2 nn0uz 0=0
3 2 eleq2i M0M0
4 3 biimpi M0M0
5 uzss M0M0
6 4 5 syl M0M0
7 6 2 sseqtrrdi M0M0
8 1 7 sstrid M0MN0