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

Definition df-fin4 7881
Description: A set is IV-finite (Dedekind finite) iff it has no equinumerous proper subset. Definition IV of [Levy58] p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014.)
Assertion
Ref Expression
df-fin4  |- FinIV  =  {
x  |  -.  E. y ( y  C.  x  /\  y  ~~  x
) }
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-fin4
StepHypRef Expression
1 cfin4 7874 . 2  class FinIV
2 vy . . . . . . . 8  set  y
32cv 1618 . . . . . . 7  class  y
4 vx . . . . . . . 8  set  x
54cv 1618 . . . . . . 7  class  x
63, 5wpss 3128 . . . . . 6  wff  y  C.  x
7 cen 6828 . . . . . . 7  class  ~~
83, 5, 7wbr 3997 . . . . . 6  wff  y  ~~  x
96, 8wa 360 . . . . 5  wff  ( y 
C.  x  /\  y  ~~  x )
109, 2wex 1537 . . . 4  wff  E. y
( y  C.  x  /\  y  ~~  x )
1110wn 5 . . 3  wff  -.  E. y ( y  C.  x  /\  y  ~~  x
)
1211, 4cab 2244 . 2  class  { x  |  -.  E. y ( y  C.  x  /\  y  ~~  x ) }
131, 12wceq 1619 1  wff FinIV  =  {
x  |  -.  E. y ( y  C.  x  /\  y  ~~  x
) }
Colors of variables: wff set class
This definition is referenced by:  isfin4  7891
  Copyright terms: Public domain W3C validator