Theorem isfin3-4

Description: Weakly Dedekind-infinite sets are exactly those with an _om -indexed ascending chain of subsets. (Contributed by Stefan O'Rear, 7-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	isfin3-4	$$⊢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(x\right)\subseteq f\left(\mathrm{suc}x\right)\to \bigcup \mathrm{ran}f\in \mathrm{ran}f\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(y\in 𝒫A⟼A\setminus y\right)=\left(y\in 𝒫A⟼A\setminus y\right)$$
2	1	isf34lem6	$$⊢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(x\right)\subseteq f\left(\mathrm{suc}x\right)\to \bigcup \mathrm{ran}f\in \mathrm{ran}f\right)\right)$$