Theorem isfin4-2

Description: Alternate definition of IV-finite sets: they lack a denumerable subset. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	isfin4-2	$$⊢A\in V\to \left(A\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow \neg \mathrm{\omega }\preccurlyeq A\right)$$

Proof

Step	Hyp	Ref	Expression
1		isfin4	$$⊢A\in V\to \left(A\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow \neg \exists x\left(x\subset A\wedge x\approx A\right)\right)$$
2		infpssr	$$⊢\left(x\subset A\wedge x\approx A\right)\to \mathrm{\omega }\preccurlyeq A$$
3	2	exlimiv	$$⊢\exists x\left(x\subset A\wedge x\approx A\right)\to \mathrm{\omega }\preccurlyeq A$$
4		infpss	$$⊢\mathrm{\omega }\preccurlyeq A\to \exists x\left(x\subset A\wedge x\approx A\right)$$
5	3 4	impbii	$$⊢\exists x\left(x\subset A\wedge x\approx A\right)\leftrightarrow \mathrm{\omega }\preccurlyeq A$$
6	5	notbii	$$⊢\neg \exists x\left(x\subset A\wedge x\approx A\right)\leftrightarrow \neg \mathrm{\omega }\preccurlyeq A$$
7	1 6	bitrdi	$$⊢A\in V\to \left(A\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow \neg \mathrm{\omega }\preccurlyeq A\right)$$