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

Definition df-fin1a 8560
 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 7419 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 8553 . 2 FinIa
2 vy . . . . . . 7
32cv 1369 . . . . . 6
4 cfn 7415 . . . . . 6
53, 4wcel 1758 . . . . 5
6 vx . . . . . . . 8
76cv 1369 . . . . . . 7
87, 3cdif 3428 . . . . . 6
98, 4wcel 1758 . . . . 5
105, 9wo 368 . . . 4
117cpw 3963 . . . 4
1210, 2, 11wral 2796 . . 3
1312, 6cab 2437 . 2
141, 13wceq 1370 1 FinIa
 Colors of variables: wff setvar class This definition is referenced by:  isfin1a  8567
 Copyright terms: Public domain W3C validator