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 = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ if ( ∪ 𝑗 = ∪ 𝑓 , ∩ 𝑥 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) , ∅ ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfcls ⊢ fClus
1 vj ⊢ 𝑗
2 ctop ⊢ Top
3 vf ⊢ 𝑓
4 cfil ⊢ Fil
5 4 crn ⊢ ran Fil
6 5 cuni ⊢ ∪ ran Fil
7 1 cv ⊢ 𝑗
8 7 cuni ⊢ ∪ 𝑗
9 3 cv ⊢ 𝑓
10 9 cuni ⊢ ∪ 𝑓
11 8 10 wceq ⊢ ∪ 𝑗 = ∪ 𝑓
12 vx ⊢ 𝑥
13 ccl ⊢ cls
14 7 13 cfv ⊢ ( cls ‘ 𝑗 )
15 12 cv ⊢ 𝑥
16 15 14 cfv ⊢ ( ( cls ‘ 𝑗 ) ‘ 𝑥 )
17 12 9 16 ciin ⊢ ∩ 𝑥 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑥 )
18 c0 ⊢ ∅
19 11 17 18 cif ⊢ if ( ∪ 𝑗 = ∪ 𝑓 , ∩ 𝑥 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) , ∅ )
20 1 3 2 6 19 cmpo ⊢ ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ if ( ∪ 𝑗 = ∪ 𝑓 , ∩ 𝑥 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) , ∅ ) )
21 0 20 wceq ⊢ fClus = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ if ( ∪ 𝑗 = ∪ 𝑓 , ∩ 𝑥 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) , ∅ ) )