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

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

Step	Hyp	Ref	Expression
1		fzssuz	$⊢ (0 \dots N) \subseteq ℤ_{\geq 0}$
2		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
3	2	eqcomi	$⊢ ℤ_{\geq 0} = ℕ_{0}$
4	1 3	sseqtri	$⊢ (0 \dots N) \subseteq ℕ_{0}$