Theorem fin1a2

Description: Every Ia-finite set is II-finite. Theorem 1 of Levy58, p. 3. (Contributed by Stefan O'Rear, 8-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	fin1a2	$$⊢A\in {\mathrm{Fin}}^{\mathrm{Ia}}\to A\in {\mathrm{Fin}}^{\mathrm{II}}$$

Proof

Step	Hyp	Ref	Expression
1		elpwi	$$⊢b\in 𝒫A\to b\subseteq A$$
2		fin1ai	$$⊢\left(A\in {\mathrm{Fin}}^{\mathrm{Ia}}\wedge b\subseteq A\right)\to \left(b\in \mathrm{Fin}\vee A\setminus b\in \mathrm{Fin}\right)$$
3		fin12	$$⊢A\setminus b\in \mathrm{Fin}\to A\setminus b\in {\mathrm{Fin}}^{\mathrm{II}}$$
4	3	orim2i	$$⊢\left(b\in \mathrm{Fin}\vee A\setminus b\in \mathrm{Fin}\right)\to \left(b\in \mathrm{Fin}\vee A\setminus b\in {\mathrm{Fin}}^{\mathrm{II}}\right)$$
5	2 4	syl	$$⊢\left(A\in {\mathrm{Fin}}^{\mathrm{Ia}}\wedge b\subseteq A\right)\to \left(b\in \mathrm{Fin}\vee A\setminus b\in {\mathrm{Fin}}^{\mathrm{II}}\right)$$
6	1 5	sylan2	$$⊢\left(A\in {\mathrm{Fin}}^{\mathrm{Ia}}\wedge b\in 𝒫A\right)\to \left(b\in \mathrm{Fin}\vee A\setminus b\in {\mathrm{Fin}}^{\mathrm{II}}\right)$$
7	6	ralrimiva	$$⊢A\in {\mathrm{Fin}}^{\mathrm{Ia}}\to \forall b\in 𝒫A\left(b\in \mathrm{Fin}\vee A\setminus b\in {\mathrm{Fin}}^{\mathrm{II}}\right)$$
8		fin1a2s	$$⊢\left(A\in {\mathrm{Fin}}^{\mathrm{Ia}}\wedge \forall b\in 𝒫A\left(b\in \mathrm{Fin}\vee A\setminus b\in {\mathrm{Fin}}^{\mathrm{II}}\right)\right)\to A\in {\mathrm{Fin}}^{\mathrm{II}}$$
9	7 8	mpdan	$$⊢A\in {\mathrm{Fin}}^{\mathrm{Ia}}\to A\in {\mathrm{Fin}}^{\mathrm{II}}$$