Definition df-ptfin 23825

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 23822	. 2 class PtFin
2		vy	. . . . . . 7 setvar 𝑦
3		vz	. . . . . . 7 setvar 𝑧
4	2, 3	wel 2146	. . . . . 6 wff 𝑦 ∈ 𝑧
5		vx	. . . . . . 7 setvar 𝑥
6	5	cv 1569	. . . . . 6 class 𝑥
7	4, 3, 6	crab 3413	. . . . 5 class {𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧}
8		cfn 8973	. . . . 5 class Fin
9	7, 8	wcel 2145	. . . 4 wff {𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin
10	6	cuni 4867	. . . 4 class ∪ 𝑥
11	9, 2, 10	wral 3077	. . 3 wff ∀𝑦 ∈ ∪ 𝑥{𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin
12	11, 5	cab 2739	. 2 class {𝑥 ∣ ∀𝑦 ∈ ∪ 𝑥{𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin}
13	1, 12	wceq 1570	1 wff PtFin = {𝑥 ∣ ∀𝑦 ∈ ∪ 𝑥{𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin}

This definition is used by:  isptfin  23835