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 | y ω x y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfn class Fin
1 vx setvar x
2 vy setvar y
3 com class ω
4 1 cv setvar x
5 cen class
6 2 cv setvar y
7 4 6 5 wbr wff x y
8 7 2 3 wrex wff y ω x y
9 8 1 cab class x | y ω x y
10 0 9 wceq wff Fin = x | y ω x y