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 ‘ 𝑗 ) ‘ 𝑥 ) , ∅ ) )