Definition df-ptfin

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cptfin	|- PtFin
1		vx	|- x
2		vy	|- y
3	1	cv	|- x
4	3	cuni	|- U. x
5		vz	|- z
6	2	cv	|- y
7	5	cv	|- z
8	6 7	wcel	|- y e. z
9	8 5 3	crab	|- { z e. x | y e. z }
10		cfn	|- Fin
11	9 10	wcel	|- { z e. x | y e. z } e. Fin
12	11 2 4	wral	|- A. y e. U. x { z e. x | y e. z } e. Fin
13	12 1	cab	|- { x | A. y e. U. x { z e. x | y e. z } e. Fin }
14	0 13	wceq	|- PtFin = { x | A. y e. U. x { z e. x | y e. z } e. Fin }