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

Definition df-fcf 20311
 Description: Define a function that gives the cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009.)
Assertion
Ref Expression
df-fcf
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-fcf
StepHypRef Expression
1 cfcf 20306 . 2
2 vj . . 3
3 vf . . 3
4 ctop 19263 . . 3
5 cfil 20214 . . . . 5
65crn 5006 . . . 4
76cuni 4251 . . 3
8 vg . . . 4
92cv 1378 . . . . . 6
109cuni 4251 . . . . 5
113cv 1378 . . . . . 6
1211cuni 4251 . . . . 5
13 cmap 7432 . . . . 5
1410, 12, 13co 6295 . . . 4
158cv 1378 . . . . . . 7
16 cfm 20302 . . . . . . 7
1710, 15, 16co 6295 . . . . . 6
1811, 17cfv 5594 . . . . 5
19 cfcls 20305 . . . . 5
209, 18, 19co 6295 . . . 4
218, 14, 20cmpt 4511 . . 3
222, 3, 4, 7, 21cmpt2 6297 . 2
231, 22wceq 1379 1
 Colors of variables: wff setvar class This definition is referenced by:  fcfval  20402
 Copyright terms: Public domain W3C validator