Definition df-ptfin

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

	Ref	Expression
Assertion	df-ptfin	$$⊢\mathrm{PtFin}=\left\{x|\forall y\in \bigcup x\left\{z\in x|y\in z\right\}\in \mathrm{Fin}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cptfin	$$class\mathrm{PtFin}$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3	1	cv	$$setvarx$$
4	3	cuni	$$class\bigcup x$$
5		vz	$$setvarz$$
6	2	cv	$$setvary$$
7	5	cv	$$setvarz$$
8	6 7	wcel	$$wffy\in z$$
9	8 5 3	crab	$$class\left\{z\in x|y\in z\right\}$$
10		cfn	$$class\mathrm{Fin}$$
11	9 10	wcel	$$wff\left\{z\in x|y\in z\right\}\in \mathrm{Fin}$$
12	11 2 4	wral	$$wff\forall y\in \bigcup x\left\{z\in x|y\in z\right\}\in \mathrm{Fin}$$
13	12 1	cab	$$class\left\{x|\forall y\in \bigcup x\left\{z\in x|y\in z\right\}\in \mathrm{Fin}\right\}$$
14	0 13	wceq	$$wff\mathrm{PtFin}=\left\{x|\forall y\in \bigcup x\left\{z\in x|y\in z\right\}\in \mathrm{Fin}\right\}$$