Theorem isfiniteg

Description: A set is finite iff it is strictly dominated by the class of natural number. Theorem 42 of Suppes p. 151. In order to avoid the Axiom of infinity, we include it as a hypothesis. (Contributed by NM, 3-Nov-2002) (Revised by Mario Carneiro, 27-Apr-2015)

	Ref	Expression
Assertion	isfiniteg	$$⊢\mathrm{\omega }\in \mathrm{V}\to \left(A\in \mathrm{Fin}\leftrightarrow A\prec \mathrm{\omega }\right)$$

Proof

Step	Hyp	Ref	Expression
1		isfi	$$⊢A\in \mathrm{Fin}\leftrightarrow \exists x\in \mathrm{\omega }A\approx x$$
2		nnsdomg	$$⊢\left(\mathrm{\omega }\in \mathrm{V}\wedge x\in \mathrm{\omega }\right)\to x\prec \mathrm{\omega }$$
3		sdomen1	$$⊢A\approx x\to \left(A\prec \mathrm{\omega }\leftrightarrow x\prec \mathrm{\omega }\right)$$
4	2 3	syl5ibrcom	$$⊢\left(\mathrm{\omega }\in \mathrm{V}\wedge x\in \mathrm{\omega }\right)\to \left(A\approx x\to A\prec \mathrm{\omega }\right)$$
5	4	rexlimdva	$$⊢\mathrm{\omega }\in \mathrm{V}\to \left(\exists x\in \mathrm{\omega }A\approx x\to A\prec \mathrm{\omega }\right)$$
6	1 5	biimtrid	$$⊢\mathrm{\omega }\in \mathrm{V}\to \left(A\in \mathrm{Fin}\to A\prec \mathrm{\omega }\right)$$
7		isfinite2	$$⊢A\prec \mathrm{\omega }\to A\in \mathrm{Fin}$$
8	6 7	impbid1	$$⊢\mathrm{\omega }\in \mathrm{V}\to \left(A\in \mathrm{Fin}\leftrightarrow A\prec \mathrm{\omega }\right)$$