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 ... 𝑁 ) ⊆ ℕ0

Proof

Step	Hyp	Ref	Expression
1		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
2	1	ssriv	⊢ ( 0 ... 𝑁 ) ⊆ ℕ0