Metamath Proof Explorer

Definition df-fin

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 . If we accept Infinity, we can also express A e. Fin by A ~< _om (Theorem isfinite .) (Contributed by NM, 22-Aug-2008)

|- Fin = { x | E. y e. _om x ~~ y }

 |-  Fin

 |-  x

 |-  y

 |-  _om

 |-  x

 |-  ~~

 |-  y

 |-  x ~~ y

 |-  E. y e. _om x ~~ y

 |-  { x | E. y e. _om x ~~ y }

 |-  Fin = { x | E. y e. _om x ~~ y }