Theorem fin11a

Description: Every I-finite set is Ia-finite. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 17-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		elpwi	$$⊢x\in 𝒫A\to x\subseteq A$$
2		ssfi	$$⊢\left(A\in \mathrm{Fin}\wedge x\subseteq A\right)\to x\in \mathrm{Fin}$$
3	1 2	sylan2	$$⊢\left(A\in \mathrm{Fin}\wedge x\in 𝒫A\right)\to x\in \mathrm{Fin}$$
4	3	orcd	$$⊢\left(A\in \mathrm{Fin}\wedge x\in 𝒫A\right)\to \left(x\in \mathrm{Fin}\vee A\setminus x\in \mathrm{Fin}\right)$$
5	4	ralrimiva	$$⊢A\in \mathrm{Fin}\to \forall x\in 𝒫A\left(x\in \mathrm{Fin}\vee A\setminus x\in \mathrm{Fin}\right)$$
6		isfin1a	$$⊢A\in \mathrm{Fin}\to \left(A\in {\mathrm{Fin}}^{\mathrm{Ia}}\leftrightarrow \forall x\in 𝒫A\left(x\in \mathrm{Fin}\vee A\setminus x\in \mathrm{Fin}\right)\right)$$
7	5 6	mpbird	$$⊢A\in \mathrm{Fin}\to A\in {\mathrm{Fin}}^{\mathrm{Ia}}$$