Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fin1a Unicode version

Definition df-fin1a 7795
 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 6753 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
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-fin1a
StepHypRef Expression
1 cfin1a 7788 . 2 FinIa
2 vy . . . . . . 7
32cv 1618 . . . . . 6
4 cfn 6749 . . . . . 6
53, 4wcel 1621 . . . . 5
6 vx . . . . . . . 8
76cv 1618 . . . . . . 7
87, 3cdif 3075 . . . . . 6
98, 4wcel 1621 . . . . 5
105, 9wo 359 . . . 4
117cpw 3530 . . . 4
1210, 2, 11wral 2509 . . 3
1312, 6cab 2239 . 2
141, 13wceq 1619 1 FinIa
 Colors of variables: wff set class This definition is referenced by:  isfin1a  7802
 Copyright terms: Public domain W3C validator