Definition df-fin1a 8686

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 7540 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

Distinct variable group:   ,

Detailed syntax breakdown of Definition df-fin1a

Step	Hyp	Ref	Expression
1		cfin1a 8679	. 2
2		vy	. . . . . . 7
3	2	cv 1394	. . . . . 6
4		cfn 7536	. . . . . 6
5	3, 4	wcel 1818	. . . . 5
6		vx	. . . . . . . 8
7	6	cv 1394	. . . . . . 7
8	7, 3	cdif 3472	. . . . . 6
9	8, 4	wcel 1818	. . . . 5
10	5, 9	wo 368	. . . 4
11	7	cpw 4012	. . . 4
12	10, 2, 11	wral 2807	. . 3
13	12, 6	cab 2442	. 2
14	1, 13	wceq 1395	1

This definition is referenced by:  isfin1a  8693