Theorem isfin1a

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

	Ref	Expression
Assertion	isfin1a	$$⊢A\in V\to \left(A\in {\mathrm{Fin}}^{\mathrm{Ia}}\leftrightarrow \forall y\in 𝒫A\left(y\in \mathrm{Fin}\vee A\setminus y\in \mathrm{Fin}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pweq	$$⊢x=A\to 𝒫x=𝒫A$$
2		difeq1	$$⊢x=A\to x\setminus y=A\setminus y$$
3	2	eleq1d	$$⊢x=A\to \left(x\setminus y\in \mathrm{Fin}\leftrightarrow A\setminus y\in \mathrm{Fin}\right)$$
4	3	orbi2d	$$⊢x=A\to \left(\left(y\in \mathrm{Fin}\vee x\setminus y\in \mathrm{Fin}\right)\leftrightarrow \left(y\in \mathrm{Fin}\vee A\setminus y\in \mathrm{Fin}\right)\right)$$
5	1 4	raleqbidv	$$⊢x=A\to \left(\forall y\in 𝒫x\left(y\in \mathrm{Fin}\vee x\setminus y\in \mathrm{Fin}\right)\leftrightarrow \forall y\in 𝒫A\left(y\in \mathrm{Fin}\vee A\setminus y\in \mathrm{Fin}\right)\right)$$
6		df-fin1a	$$⊢{\mathrm{Fin}}^{\mathrm{Ia}}=\left\{x|\forall y\in 𝒫x\left(y\in \mathrm{Fin}\vee x\setminus y\in \mathrm{Fin}\right)\right\}$$
7	5 6	elab2g	$$⊢A\in V\to \left(A\in {\mathrm{Fin}}^{\mathrm{Ia}}\leftrightarrow \forall y\in 𝒫A\left(y\in \mathrm{Fin}\vee A\setminus y\in \mathrm{Fin}\right)\right)$$