Definition df-fin1a 9107

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 7959 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.)

Assertion

Ref	Expression
df-fin1a	|- FinIa = { x | A. y e. ~P x ( y e. Fin \/ ( x \ y ) e. Fin ) }

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-fin1a

Step	Hyp	Ref	Expression
1		cfin1a 9100	. 2 class FinIa
2		vy	. . . . . . 7 setvar y
3	2	cv 1482	. . . . . 6 class y
4		cfn 7955	. . . . . 6 class Fin
5	3, 4	wcel 1990	. . . . 5 wff y e. Fin
6		vx	. . . . . . . 8 setvar x
7	6	cv 1482	. . . . . . 7 class x
8	7, 3	cdif 3571	. . . . . 6 class ( x \ y )
9	8, 4	wcel 1990	. . . . 5 wff ( x \ y ) e. Fin
10	5, 9	wo 383	. . . 4 wff ( y e. Fin \/ ( x \ y ) e. Fin )
11	7	cpw 4158	. . . 4 class ~P x
12	10, 2, 11	wral 2912	. . 3 wff A. y e. ~P x ( y e. Fin \/ ( x \ y ) e. Fin )
13	12, 6	cab 2608	. 2 class { x | A. y e. ~P x ( y e. Fin \/ ( x \ y ) e. Fin ) }
14	1, 13	wceq 1483	1 wff FinIa = { x | A. y e. ~P x ( y e. Fin \/ ( x \ y ) e. Fin ) }

This definition is referenced by:  isfin1a  9114