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	$$⊢\mathrm{Fin}=\left\{x|\exists y\in \mathrm{\omega }x\approx y\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfn	$$class\mathrm{Fin}$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3		com	$$class\mathrm{\omega }$$
4	1	cv	$$setvarx$$
5		cen	$$class\approx$$
6	2	cv	$$setvary$$
7	4 6 5	wbr	$$wffx\approx y$$
8	7 2 3	wrex	$$wff\exists y\in \mathrm{\omega }x\approx y$$
9	8 1	cab	$$class\left\{x|\exists y\in \mathrm{\omega }x\approx y\right\}$$
10	0 9	wceq	$$wff\mathrm{Fin}=\left\{x|\exists y\in \mathrm{\omega }x\approx y\right\}$$