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

Definition df-fin7 7801
Description: A set is VII-finite iff it cannot be infinitely well ordered. Equivalent to definition VII of [Levy58] p. 4. (Contributed by Stefan O'Rear, 12-Nov-2014.)
Assertion
Ref Expression
df-fin7  |- FinVII  =  { x  |  -.  E. y  e.  ( On  \  om ) x  ~~  y }
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-fin7
StepHypRef Expression
1 cfin7 7794 . 2  class FinVII
2 vx . . . . . . 7  set  x
32cv 1618 . . . . . 6  class  x
4 vy . . . . . . 7  set  y
54cv 1618 . . . . . 6  class  y
6 cen 6746 . . . . . 6  class  ~~
73, 5, 6wbr 3920 . . . . 5  wff  x  ~~  y
8 con0 4285 . . . . . 6  class  On
9 com 4547 . . . . . 6  class  om
108, 9cdif 3075 . . . . 5  class  ( On 
\  om )
117, 4, 10wrex 2510 . . . 4  wff  E. y  e.  ( On  \  om ) x  ~~  y
1211wn 5 . . 3  wff  -.  E. y  e.  ( On  \  om ) x  ~~  y
1312, 2cab 2239 . 2  class  { x  |  -.  E. y  e.  ( On  \  om ) x  ~~  y }
141, 13wceq 1619 1  wff FinVII  =  { x  |  -.  E. y  e.  ( On  \  om ) x  ~~  y }
Colors of variables: wff set class
This definition is referenced by:  isfin7  7811
  Copyright terms: Public domain W3C validator