Definition df-ptfin 21309

Description: Define "point-finite." (Contributed by Jeff Hankins, 21-Jan-2010.)

Assertion

Ref	Expression
df-ptfin	|- PtFin = { x | A. y e. U. x { z e. x | y e. z } e. Fin }

Distinct variable group:   x, y, z

Detailed syntax breakdown of Definition df-ptfin

Step	Hyp	Ref	Expression
1		cptfin 21306	. 2 class PtFin
2		vy	. . . . . . 7 setvar y
3		vz	. . . . . . 7 setvar z
4	2, 3	wel 1991	. . . . . 6 wff y e. z
5		vx	. . . . . . 7 setvar x
6	5	cv 1482	. . . . . 6 class x
7	4, 3, 6	crab 2916	. . . . 5 class { z e. x | y e. z }
8		cfn 7955	. . . . 5 class Fin
9	7, 8	wcel 1990	. . . 4 wff { z e. x | y e. z } e. Fin
10	6	cuni 4436	. . . 4 class U. x
11	9, 2, 10	wral 2912	. . 3 wff A. y e. U. x { z e. x | y e. z } e. Fin
12	11, 5	cab 2608	. 2 class { x | A. y e. U. x { z e. x | y e. z } e. Fin }
13	1, 12	wceq 1483	1 wff PtFin = { x | A. y e. U. x { z e. x | y e. z } e. Fin }

This definition is referenced by:  isptfin  21319