Theorem fz1ssnn

Description: A finite set of positive integers is a set of positive integers. (Contributed by Stefan O'Rear, 16-Oct-2014)

	Ref	Expression
Assertion	fz1ssnn	$$⊢\left(1\dots A\right)\subseteq \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		elfznn	$$⊢a\in \left(1\dots A\right)\to a\in \mathbb{N}$$
2	1	ssriv	$$⊢\left(1\dots A\right)\subseteq \mathbb{N}$$