This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \| \exists y \in ω x \approx 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 \approx$
6	2	cv	$setvar y$
7	4 6 5	wbr	$wff x \approx y$
8	7 2 3	wrex	$wff \exists y \in ω x \approx y$
9	8 1	cab	$class \{x \| \exists y \in ω x \approx y\}$
10	0 9	wceq	$wff Fin = \{x \| \exists y \in ω x \approx y\}$