Definition df-ptfin

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cptfin	⊢ PtFin
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4	3	cuni	⊢ ∪ 𝑥
5		vz	⊢ 𝑧
6	2	cv	⊢ 𝑦
7	5	cv	⊢ 𝑧
8	6 7	wcel	⊢ 𝑦 ∈ 𝑧
9	8 5 3	crab	⊢ { 𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧 }
10		cfn	⊢ Fin
11	9 10	wcel	⊢ { 𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧 } ∈ Fin
12	11 2 4	wral	⊢ ∀ 𝑦 ∈ ∪ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧 } ∈ Fin
13	12 1	cab	⊢ { 𝑥 ∣ ∀ 𝑦 ∈ ∪ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧 } ∈ Fin }
14	0 13	wceq	⊢ PtFin = { 𝑥 ∣ ∀ 𝑦 ∈ ∪ 𝑥 { 𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧 } ∈ Fin }