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

Metamath Proof Explorer

Definition df-fcls

Description: Define a function that takes a filter in a topology to its set of cluster points. (Contributed by Jeff Hankins, 10-Nov-2009)

Ref Expression
Assertion df-fcls ⊢ fClus = j ∈ Top , f ∈ ⋃ ran ⁡ Fil ⟼ if ⋃ j = ⋃ f ⋂ x ∈ f cls ⁡ j ⁡ x ∅

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfcls class fClus
1 vj setvar j
2 ctop class Top
3 vf setvar f
4 cfil class Fil
5 4 crn class ran ⁡ Fil
6 5 cuni class ⋃ ran ⁡ Fil
7 1 cv setvar j
8 7 cuni class ⋃ j
9 3 cv setvar f
10 9 cuni class ⋃ f
11 8 10 wceq wff ⋃ j = ⋃ f
12 vx setvar x
13 ccl class cls
14 7 13 cfv class cls ⁡ j
15 12 cv setvar x
16 15 14 cfv class cls ⁡ j ⁡ x
17 12 9 16 ciin class ⋂ x ∈ f cls ⁡ j ⁡ x
18 c0 class ∅
19 11 17 18 cif class if ⋃ j = ⋃ f ⋂ x ∈ f cls ⁡ j ⁡ x ∅
20 1 3 2 6 19 cmpo class j ∈ Top , f ∈ ⋃ ran ⁡ Fil ⟼ if ⋃ j = ⋃ f ⋂ x ∈ f cls ⁡ j ⁡ x ∅
21 0 20 wceq wff fClus = j ∈ Top , f ∈ ⋃ ran ⁡ Fil ⟼ if ⋃ j = ⋃ f ⋂ x ∈ f cls ⁡ j ⁡ x ∅