Definition df-fin1a

Description: A set is Ia-finite iff it is not the union of two I-infinite sets. Equivalent to definition Ia of Levy58 p. 2. A I-infinite Ia-finite set is also known as an amorphous set. This is the second of Levy's eight definitions of finite set. Levy's I-finite is equivalent to our df-fin and not repeated here. These eight definitions are equivalent with Choice but strictly decreasing in strength in models where Choice fails; conversely, they provide a series of increasingly stronger notions of infiniteness. (Contributed by Stefan O'Rear, 12-Nov-2014)

	Ref	Expression
Assertion	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\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin1a	$$class{\mathrm{Fin}}^{\mathrm{Ia}}$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3	1	cv	$$setvarx$$
4	3	cpw	$$class𝒫x$$
5	2	cv	$$setvary$$
6		cfn	$$class\mathrm{Fin}$$
7	5 6	wcel	$$wffy\in \mathrm{Fin}$$
8	3 5	cdif	$$class\left(x\setminus y\right)$$
9	8 6	wcel	$$wffx\setminus y\in \mathrm{Fin}$$
10	7 9	wo	$$wff\left(y\in \mathrm{Fin}\vee x\setminus y\in \mathrm{Fin}\right)$$
11	10 2 4	wral	$$wff\forall y\in 𝒫x\left(y\in \mathrm{Fin}\vee x\setminus y\in \mathrm{Fin}\right)$$
12	11 1	cab	$$class\left\{x|\forall y\in 𝒫x\left(y\in \mathrm{Fin}\vee x\setminus y\in \mathrm{Fin}\right)\right\}$$
13	0 12	wceq	$$wff{\mathrm{Fin}}^{\mathrm{Ia}}=\left\{x|\forall y\in 𝒫x\left(y\in \mathrm{Fin}\vee x\setminus y\in \mathrm{Fin}\right)\right\}$$