Theorem isfin3-3

Description: Weakly Dedekind-infinite sets are exactly those with an _om -indexed descending chain of subsets. (Contributed by Stefan O'Rear, 7-Nov-2014)

	Ref	Expression
Assertion	isfin3-3	$$⊢A\in V\to \left(A\in {\mathrm{Fin}}^{\mathrm{III}}\leftrightarrow \forall f\in \left({𝒫A}^{\mathrm{\omega }}\right)\left(\forall x\in \mathrm{\omega }f\left(\mathrm{suc}x\right)\subseteq f\left(x\right)\to \bigcap \mathrm{ran}f\in \mathrm{ran}f\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isf33lem	$$⊢{\mathrm{Fin}}^{\mathrm{III}}=\left\{g|\forall a\in \left({𝒫g}^{\mathrm{\omega }}\right)\left(\forall b\in \mathrm{\omega }a\left(\mathrm{suc}b\right)\subseteq a\left(b\right)\to \bigcap \mathrm{ran}a\in \mathrm{ran}a\right)\right\}$$
2	1	isfin3ds	$$⊢A\in V\to \left(A\in {\mathrm{Fin}}^{\mathrm{III}}\leftrightarrow \forall f\in \left({𝒫A}^{\mathrm{\omega }}\right)\left(\forall x\in \mathrm{\omega }f\left(\mathrm{suc}x\right)\subseteq f\left(x\right)\to \bigcap \mathrm{ran}f\in \mathrm{ran}f\right)\right)$$