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	|- Fin1a = { x | A. y e. ~P x ( y e. Fin \/ ( x \ y ) e. Fin ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin1a	|- Fin1a
1		vx	|- x
2		vy	|- y
3	1	cv	|- x
4	3	cpw	|- ~P x
5	2	cv	|- y
6		cfn	|- Fin
7	5 6	wcel	|- y e. Fin
8	3 5	cdif	|- ( x \ y )
9	8 6	wcel	|- ( x \ y ) e. Fin
10	7 9	wo	|- ( y e. Fin \/ ( x \ y ) e. Fin )
11	10 2 4	wral	|- A. y e. ~P x ( y e. Fin \/ ( x \ y ) e. Fin )
12	11 1	cab	|- { x | A. y e. ~P x ( y e. Fin \/ ( x \ y ) e. Fin ) }
13	0 12	wceq	|- Fin1a = { x | A. y e. ~P x ( y e. Fin \/ ( x \ y ) e. Fin ) }