# Metamath Proof Explorer

## 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}}^{III}↔¬\mathrm{\omega }{\preccurlyeq }^{*}{A}\right)$

### Proof

Step Hyp Ref Expression
1 isfin32i ${⊢}{A}\in {\mathrm{Fin}}^{III}\to ¬\mathrm{\omega }{\preccurlyeq }^{*}{A}$
2 isf33lem ${⊢}{\mathrm{Fin}}^{III}=\left\{{g}|\forall {a}\in \left({𝒫{g}}^{\mathrm{\omega }}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{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(¬\mathrm{\omega }{\preccurlyeq }^{*}{A}\to {A}\in {\mathrm{Fin}}^{III}\right)$
4 1 3 impbid2 ${⊢}{A}\in {V}\to \left({A}\in {\mathrm{Fin}}^{III}↔¬\mathrm{\omega }{\preccurlyeq }^{*}{A}\right)$