Theorem isfin3-2

Description: Weakly Dedekind-infinite sets are exactly those which can be mapped onto _om . (Contributed by Stefan O'Rear, 6-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		isfin32i	$$⊢A\in {\mathrm{Fin}}^{\mathrm{III}}\to \neg \mathrm{\omega }{\preccurlyeq }^{*}A$$
2		isf33lem	$$⊢{\mathrm{Fin}}^{\mathrm{III}}=\left\{g|\forall a\in \left({𝒫g}^{\mathrm{\omega }}\right)\left(\forall x\in \mathrm{\omega }a\left(\mathrm{suc}x\right)\subseteq a\left(x\right)\to \bigcap \mathrm{ran}a\in \mathrm{ran}a\right)\right\}$$
3	2	isf32lem12	$$⊢A\in V\to \left(\neg \mathrm{\omega }{\preccurlyeq }^{*}A\to A\in {\mathrm{Fin}}^{\mathrm{III}}\right)$$
4	1 3	impbid2	$$⊢A\in V\to \left(A\in {\mathrm{Fin}}^{\mathrm{III}}\leftrightarrow \neg \mathrm{\omega }{\preccurlyeq }^{*}A\right)$$