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

Definition df-fin 6867
Description: Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our " a  e.  Fin". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 7342. If we accept Infinity, we can also express  A  e.  Fin by  A 
~<  om (theorem isfinite 7353.) (Contributed by NM, 22-Aug-2008.)
Assertion
Ref Expression
df-fin  |-  Fin  =  { x  |  E. y  e.  om  x  ~~  y }
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-fin
StepHypRef Expression
1 cfn 6863 . 2  class  Fin
2 vx . . . . . 6  set  x
32cv 1622 . . . . 5  class  x
4 vy . . . . . 6  set  y
54cv 1622 . . . . 5  class  y
6 cen 6860 . . . . 5  class  ~~
73, 5, 6wbr 4023 . . . 4  wff  x  ~~  y
8 com 4656 . . . 4  class  om
97, 4, 8wrex 2544 . . 3  wff  E. y  e.  om  x  ~~  y
109, 2cab 2269 . 2  class  { x  |  E. y  e.  om  x  ~~  y }
111, 10wceq 1623 1  wff  Fin  =  { x  |  E. y  e.  om  x  ~~  y }
Colors of variables: wff set class
This definition is referenced by:  isfi  6885  dffin1-5  8014
  Copyright terms: Public domain W3C validator