Theorem nnfiOLD

Description: Obsolete version of nnfi as of 23-Sep-2024. (Contributed by Stefan O'Rear, 21-Mar-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	nnfiOLD	$$⊢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}$$