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)

Ref Expression
Assertion df-fin
|- Fin = { x | E. y e. _om x ~~ y }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfn
 |-  Fin
1 vx
 |-  x
2 vy
 |-  y
3 com
 |-  _om
4 1 cv
 |-  x
5 cen
 |-  ~~
6 2 cv
 |-  y
7 4 6 5 wbr
 |-  x ~~ y
8 7 2 3 wrex
 |-  E. y e. _om x ~~ y
9 8 1 cab
 |-  { x | E. y e. _om x ~~ y }
10 0 9 wceq
 |-  Fin = { x | E. y e. _om x ~~ y }