Definition df-ptfin 23449

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

Assertion

Ref	Expression
df-ptfin	⊢ PtFin = {𝑥 ∣ ∀𝑦 ∈ ∪ 𝑥{𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin}

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ptfin

Step	Hyp	Ref	Expression
1		cptfin 23446	. 2 class PtFin
2		vy	. . . . . . 7 setvar 𝑦
3		vz	. . . . . . 7 setvar 𝑧
4	2, 3	wel 2110	. . . . . 6 wff 𝑦 ∈ 𝑧
5		vx	. . . . . . 7 setvar 𝑥
6	5	cv 1539	. . . . . 6 class 𝑥
7	4, 3, 6	crab 3420	. . . . 5 class {𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧}
8		cfn 8964	. . . . 5 class Fin
9	7, 8	wcel 2109	. . . 4 wff {𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin
10	6	cuni 4888	. . . 4 class ∪ 𝑥
11	9, 2, 10	wral 3052	. . 3 wff ∀𝑦 ∈ ∪ 𝑥{𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin
12	11, 5	cab 2714	. 2 class {𝑥 ∣ ∀𝑦 ∈ ∪ 𝑥{𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin}
13	1, 12	wceq 1540	1 wff PtFin = {𝑥 ∣ ∀𝑦 ∈ ∪ 𝑥{𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin}

This definition is referenced by:  isptfin  23459