Theorem isfinite

Description: A set is finite iff it is strictly dominated by the class of natural number. Theorem 42 of Suppes p. 151. The Axiom of Infinity is used for the forward implication. (Contributed by FL, 16-Apr-2011)

	Ref	Expression
Assertion	isfinite	$$⊢A\in \mathrm{Fin}\leftrightarrow A\prec \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
2		isfiniteg	$$⊢\mathrm{\omega }\in \mathrm{V}\to \left(A\in \mathrm{Fin}\leftrightarrow A\prec \mathrm{\omega }\right)$$
3	1 2	ax-mp	$$⊢A\in \mathrm{Fin}\leftrightarrow A\prec \mathrm{\omega }$$