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

Definition df-fcls 21792
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 fClus = (𝑗 ∈ Top, 𝑓 ran Fil ↦ if( 𝑗 = 𝑓, 𝑥𝑓 ((cls‘𝑗)‘𝑥), ∅))
Distinct variable group:   𝑓,𝑗,𝑥

Detailed syntax breakdown of Definition df-fcls
StepHypRef Expression
1 cfcls 21787 . 2 class fClus
2 vj . . 3 setvar 𝑗
3 vf . . 3 setvar 𝑓
4 ctop 20746 . . 3 class Top
5 cfil 21696 . . . . 5 class Fil
65crn 5144 . . . 4 class ran Fil
76cuni 4468 . . 3 class ran Fil
82cv 1522 . . . . . 6 class 𝑗
98cuni 4468 . . . . 5 class 𝑗
103cv 1522 . . . . . 6 class 𝑓
1110cuni 4468 . . . . 5 class 𝑓
129, 11wceq 1523 . . . 4 wff 𝑗 = 𝑓
13 vx . . . . 5 setvar 𝑥
1413cv 1522 . . . . . 6 class 𝑥
15 ccl 20870 . . . . . . 7 class cls
168, 15cfv 5926 . . . . . 6 class (cls‘𝑗)
1714, 16cfv 5926 . . . . 5 class ((cls‘𝑗)‘𝑥)
1813, 10, 17ciin 4553 . . . 4 class 𝑥𝑓 ((cls‘𝑗)‘𝑥)
19 c0 3948 . . . 4 class
2012, 18, 19cif 4119 . . 3 class if( 𝑗 = 𝑓, 𝑥𝑓 ((cls‘𝑗)‘𝑥), ∅)
212, 3, 4, 7, 20cmpt2 6692 . 2 class (𝑗 ∈ Top, 𝑓 ran Fil ↦ if( 𝑗 = 𝑓, 𝑥𝑓 ((cls‘𝑗)‘𝑥), ∅))
221, 21wceq 1523 1 wff fClus = (𝑗 ∈ Top, 𝑓 ran Fil ↦ if( 𝑗 = 𝑓, 𝑥𝑓 ((cls‘𝑗)‘𝑥), ∅))
Colors of variables: wff setvar class
This definition is referenced by:  fclsval  21859  isfcls  21860
  Copyright terms: Public domain W3C validator