Theorem fin1ai

Description: Property of a Ia-finite set. (Contributed by Stefan O'Rear, 16-May-2015)

	Ref	Expression
Assertion	fin1ai	$$⊢\left(A\in {\mathrm{Fin}}^{\mathrm{Ia}}\wedge X\subseteq A\right)\to \left(X\in \mathrm{Fin}\vee A\setminus X\in \mathrm{Fin}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢x=X\to \left(x\in \mathrm{Fin}\leftrightarrow X\in \mathrm{Fin}\right)$$
2		difeq2	$$⊢x=X\to A\setminus x=A\setminus X$$
3	2	eleq1d	$$⊢x=X\to \left(A\setminus x\in \mathrm{Fin}\leftrightarrow A\setminus X\in \mathrm{Fin}\right)$$
4	1 3	orbi12d	$$⊢x=X\to \left(\left(x\in \mathrm{Fin}\vee A\setminus x\in \mathrm{Fin}\right)\leftrightarrow \left(X\in \mathrm{Fin}\vee A\setminus X\in \mathrm{Fin}\right)\right)$$
5		isfin1a	$$⊢A\in {\mathrm{Fin}}^{\mathrm{Ia}}\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)$$
6	5	ibi	$$⊢A\in {\mathrm{Fin}}^{\mathrm{Ia}}\to \forall x\in 𝒫A\left(x\in \mathrm{Fin}\vee A\setminus x\in \mathrm{Fin}\right)$$
7	6	adantr	$$⊢\left(A\in {\mathrm{Fin}}^{\mathrm{Ia}}\wedge X\subseteq A\right)\to \forall x\in 𝒫A\left(x\in \mathrm{Fin}\vee A\setminus x\in \mathrm{Fin}\right)$$
8		elpw2g	$$⊢A\in {\mathrm{Fin}}^{\mathrm{Ia}}\to \left(X\in 𝒫A\leftrightarrow X\subseteq A\right)$$
9	8	biimpar	$$⊢\left(A\in {\mathrm{Fin}}^{\mathrm{Ia}}\wedge X\subseteq A\right)\to X\in 𝒫A$$
10	4 7 9	rspcdva	$$⊢\left(A\in {\mathrm{Fin}}^{\mathrm{Ia}}\wedge X\subseteq A\right)\to \left(X\in \mathrm{Fin}\vee A\setminus X\in \mathrm{Fin}\right)$$