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

Definition df-fin1a 7906
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 6862 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
StepHypRef Expression
1 cfin1a 7899 . 2  class FinIa
2 vy . . . . . . 7  set  y
32cv 1623 . . . . . 6  class  y
4 cfn 6858 . . . . . 6  class  Fin
53, 4wcel 1685 . . . . 5  wff  y  e. 
Fin
6 vx . . . . . . . 8  set  x
76cv 1623 . . . . . . 7  class  x
87, 3cdif 3150 . . . . . 6  class  ( x 
\  y )
98, 4wcel 1685 . . . . 5  wff  ( x 
\  y )  e. 
Fin
105, 9wo 359 . . . 4  wff  ( y  e.  Fin  \/  (
x  \  y )  e.  Fin )
117cpw 3626 . . . 4  class  ~P x
1210, 2, 11wral 2544 . . 3  wff  A. y  e.  ~P  x ( y  e.  Fin  \/  (
x  \  y )  e.  Fin )
1312, 6cab 2270 . 2  class  { x  |  A. y  e.  ~P  x ( y  e. 
Fin  \/  ( x  \  y )  e.  Fin ) }
141, 13wceq 1624 1  wff FinIa  =  {
x  |  A. y  e.  ~P  x ( y  e.  Fin  \/  (
x  \  y )  e.  Fin ) }
Colors of variables: wff set class
This definition is referenced by:  isfin1a  7913
  Copyright terms: Public domain W3C validator