This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ptfin

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

Ref Expression
Assertion df-ptfin ⊢ PtFin = x | ∀ y ∈ ⋃ x z ∈ x | y ∈ z ∈ Fin

Detailed syntax breakdown

Step Hyp Ref Expression
0 cptfin class PtFin
1 vx setvar x
2 vy setvar y
3 1 cv setvar x
4 3 cuni class ⋃ x
5 vz setvar z
6 2 cv setvar y
7 5 cv setvar z
8 6 7 wcel wff y ∈ z
9 8 5 3 crab class z ∈ x | y ∈ z
10 cfn class Fin
11 9 10 wcel wff z ∈ x | y ∈ z ∈ Fin
12 11 2 4 wral wff ∀ y ∈ ⋃ x z ∈ x | y ∈ z ∈ Fin
13 12 1 cab class x | ∀ y ∈ ⋃ x z ∈ x | y ∈ z ∈ Fin
14 0 13 wceq wff PtFin = x | ∀ y ∈ ⋃ x z ∈ x | y ∈ z ∈ Fin