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

Definition df-fin7 7917
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 7910 . 2  class FinVII
2 vx . . . . . . 7  set  x
32cv 1622 . . . . . 6  class  x
4 vy . . . . . . 7  set  y
54cv 1622 . . . . . 6  class  y
6 cen 6860 . . . . . 6  class  ~~
73, 5, 6wbr 4023 . . . . 5  wff  x  ~~  y
8 con0 4392 . . . . . 6  class  On
9 com 4656 . . . . . 6  class  om
108, 9cdif 3149 . . . . 5  class  ( On 
\  om )
117, 4, 10wrex 2544 . . . 4  wff  E. y  e.  ( On  \  om ) x  ~~  y
1211wn 3 . . 3  wff  -.  E. y  e.  ( On  \  om ) x  ~~  y
1312, 2cab 2269 . 2  class  { x  |  -.  E. y  e.  ( On  \  om ) x  ~~  y }
141, 13wceq 1623 1  wff FinVII  =  { x  |  -.  E. y  e.  ( On  \  om ) x  ~~  y }
Colors of variables: wff set class
This definition is referenced by:  isfin7  7927
  Copyright terms: Public domain W3C validator