Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fcls Structured version   Unicode version

Definition df-fcls 17965
 Description: Define a function that takes a filter in a topology to its set of cluster points. (Contributed by Jeff Hankins, 10-Nov-2009.)
Assertion
Ref Expression
df-fcls
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-fcls
StepHypRef Expression
1 cfcls 17960 . 2
2 vj . . 3
3 vf . . 3
4 ctop 16950 . . 3
5 cfil 17869 . . . . 5
65crn 4871 . . . 4
76cuni 4007 . . 3
82cv 1651 . . . . . 6
98cuni 4007 . . . . 5
103cv 1651 . . . . . 6
1110cuni 4007 . . . . 5
129, 11wceq 1652 . . . 4
13 vx . . . . 5
1413cv 1651 . . . . . 6
15 ccl 17074 . . . . . . 7
168, 15cfv 5446 . . . . . 6
1714, 16cfv 5446 . . . . 5
1813, 10, 17ciin 4086 . . . 4
19 c0 3620 . . . 4
2012, 18, 19cif 3731 . . 3
212, 3, 4, 7, 20cmpt2 6075 . 2
221, 21wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  fclsval  18032  isfcls  18033
 Copyright terms: Public domain W3C validator