Theorem nnfi

Description: Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Assertion	nnfi	$$⊢A\in \mathrm{\omega }\to A\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		onfin2	$$⊢\mathrm{\omega }=\mathrm{On}\cap \mathrm{Fin}$$
2		inss2	$$⊢\mathrm{On}\cap \mathrm{Fin}\subseteq \mathrm{Fin}$$
3	1 2	eqsstri	$$⊢\mathrm{\omega }\subseteq \mathrm{Fin}$$
4	3	sseli	$$⊢A\in \mathrm{\omega }\to A\in \mathrm{Fin}$$