Theorem fin1a2lem8

Description: Lemma for fin1a2 . Split a III-infinite set in two pieces. (Contributed by Stefan O'Rear, 7-Nov-2014)

	Ref	Expression
Assertion	fin1a2lem8	$$⊢\left(A\in V\wedge \forall x\in 𝒫A\left(x\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus x\in {\mathrm{Fin}}^{\mathrm{III}}\right)\right)\to A\in {\mathrm{Fin}}^{\mathrm{III}}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(y\in \mathrm{\omega }⟼2_{𝑜}{\cdot }_{𝑜}y\right)=\left(y\in \mathrm{\omega }⟼2_{𝑜}{\cdot }_{𝑜}y\right)$$
2		eqid	$$⊢\left(y\in \mathrm{On}⟼\mathrm{suc}y\right)=\left(y\in \mathrm{On}⟼\mathrm{suc}y\right)$$
3	1 2	fin1a2lem7	$$⊢\left(A\in V\wedge \forall x\in 𝒫A\left(x\in {\mathrm{Fin}}^{\mathrm{III}}\vee A\setminus x\in {\mathrm{Fin}}^{\mathrm{III}}\right)\right)\to A\in {\mathrm{Fin}}^{\mathrm{III}}$$