This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \dots N) \subseteq ℕ_{0}$

Step	Hyp	Ref	Expression
1		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
2	1	ssriv	$⊢ (0 \dots N) \subseteq ℕ_{0}$