Definition df-fin 5430

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 5731. If we accept Infinity, we can also express A e. Fin by A ~< om (theorem isfinite 5741.)

Assertion

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

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-fin

Step	Hyp	Ref	Expression
1		cfn 5426	. 2 class Fin
2		vx	. . . . . 6 set x
3	2	cv 1297	. . . . 5 class x
4		vy	. . . . . 6 set y
5	4	cv 1297	. . . . 5 class y
6		cen 5423	. . . . 5 class ~~
7	3, 5, 6	wbr 3338	. . . 4 wff x ~~ y
8		com 3949	. . . 4 class om
9	7, 4, 8	wrex 2106	. . 3 wff E.y e. om x ~~ y
10	9, 2	cab 1871	. 2 class {x | E.y e. om x ~~ y}
11	1, 10	wceq 1298	1 wff Fin = {x | E.y e. om x ~~ y}

This definition is referenced by:  isfi 5441  indexfi 10174  indexfiOLD 15755

Copyright terms: Public domain