Definition df-ptfin 22116

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 22113	. 2 class PtFin
2		vy	. . . . . . 7 setvar 𝑦
3		vz	. . . . . . 7 setvar 𝑧
4	2, 3	wel 2115	. . . . . 6 wff 𝑦 ∈ 𝑧
5		vx	. . . . . . 7 setvar 𝑥
6	5	cv 1536	. . . . . 6 class 𝑥
7	4, 3, 6	crab 3144	. . . . 5 class {𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧}
8		cfn 8511	. . . . 5 class Fin
9	7, 8	wcel 2114	. . . 4 wff {𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin
10	6	cuni 4840	. . . 4 class ∪ 𝑥
11	9, 2, 10	wral 3140	. . 3 wff ∀𝑦 ∈ ∪ 𝑥{𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin
12	11, 5	cab 2801	. 2 class {𝑥 ∣ ∀𝑦 ∈ ∪ 𝑥{𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin}
13	1, 12	wceq 1537	1 wff PtFin = {𝑥 ∣ ∀𝑦 ∈ ∪ 𝑥{𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin}

This definition is referenced by:  isptfin  22126