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

Definition df-fcf 22551
Description: Define a function that gives the cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009.)
Assertion
Ref Expression
df-fcf fClusf = (𝑗 ∈ Top, 𝑓 ran Fil ↦ (𝑔 ∈ ( 𝑗m 𝑓) ↦ (𝑗 fClus (( 𝑗 FilMap 𝑔)‘𝑓))))
Distinct variable group:   𝑓,𝑔,𝑗

Detailed syntax breakdown of Definition df-fcf
StepHypRef Expression
1 cfcf 22546 . 2 class fClusf
2 vj . . 3 setvar 𝑗
3 vf . . 3 setvar 𝑓
4 ctop 21502 . . 3 class Top
5 cfil 22454 . . . . 5 class Fil
65crn 5524 . . . 4 class ran Fil
76cuni 4803 . . 3 class ran Fil
8 vg . . . 4 setvar 𝑔
92cv 1537 . . . . . 6 class 𝑗
109cuni 4803 . . . . 5 class 𝑗
113cv 1537 . . . . . 6 class 𝑓
1211cuni 4803 . . . . 5 class 𝑓
13 cmap 8393 . . . . 5 class m
1410, 12, 13co 7139 . . . 4 class ( 𝑗m 𝑓)
158cv 1537 . . . . . . 7 class 𝑔
16 cfm 22542 . . . . . . 7 class FilMap
1710, 15, 16co 7139 . . . . . 6 class ( 𝑗 FilMap 𝑔)
1811, 17cfv 6328 . . . . 5 class (( 𝑗 FilMap 𝑔)‘𝑓)
19 cfcls 22545 . . . . 5 class fClus
209, 18, 19co 7139 . . . 4 class (𝑗 fClus (( 𝑗 FilMap 𝑔)‘𝑓))
218, 14, 20cmpt 5113 . . 3 class (𝑔 ∈ ( 𝑗m 𝑓) ↦ (𝑗 fClus (( 𝑗 FilMap 𝑔)‘𝑓)))
222, 3, 4, 7, 21cmpo 7141 . 2 class (𝑗 ∈ Top, 𝑓 ran Fil ↦ (𝑔 ∈ ( 𝑗m 𝑓) ↦ (𝑗 fClus (( 𝑗 FilMap 𝑔)‘𝑓))))
231, 22wceq 1538 1 wff fClusf = (𝑗 ∈ Top, 𝑓 ran Fil ↦ (𝑔 ∈ ( 𝑗m 𝑓) ↦ (𝑗 fClus (( 𝑗 FilMap 𝑔)‘𝑓))))
Colors of variables: wff setvar class
This definition is referenced by:  fcfval  22642
  Copyright terms: Public domain W3C validator