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

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
StepHypRef Expression
1 cfin1a 8679 . 2
2 vy . . . . . . 7
32cv 1394 . . . . . 6
4 cfn 7536 . . . . . 6
53, 4wcel 1818 . . . . 5
6 vx . . . . . . . 8
76cv 1394 . . . . . . 7
87, 3cdif 3472 . . . . . 6
98, 4wcel 1818 . . . . 5
105, 9wo 368 . . . 4
117cpw 4012 . . . 4
1210, 2, 11wral 2807 . . 3
1312, 6cab 2442 . 2
141, 13wceq 1395 1
 Colors of variables: wff setvar class This definition is referenced by:  isfin1a  8693
 Copyright terms: Public domain W3C validator