This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-fcf

Description: Define a function that gives the cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009)

Ref Expression
Assertion df-fcf fClusf = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ ( 𝑔 ∈ ( ∪ 𝑗 ↑m ∪ 𝑓 ) ↦ ( 𝑗 fClus ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfcf ⊢ fClusf
1 vj ⊢ 𝑗
2 ctop ⊢ Top
3 vf ⊢ 𝑓
4 cfil ⊢ Fil
5 4 crn ⊢ ran Fil
6 5 cuni ⊢ ∪ ran Fil
7 vg ⊢ 𝑔
8 1 cv ⊢ 𝑗
9 8 cuni ⊢ ∪ 𝑗
10 cmap ⊢ ↑m
11 3 cv ⊢ 𝑓
12 11 cuni ⊢ ∪ 𝑓
13 9 12 10 co ⊢ ( ∪ 𝑗 ↑m ∪ 𝑓 )
14 cfcls ⊢ fClus
15 cfm ⊢ FilMap
16 7 cv ⊢ 𝑔
17 9 16 15 co ⊢ ( ∪ 𝑗 FilMap 𝑔 )
18 11 17 cfv ⊢ ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 )
19 8 18 14 co ⊢ ( 𝑗 fClus ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 ) )
20 7 13 19 cmpt ⊢ ( 𝑔 ∈ ( ∪ 𝑗 ↑m ∪ 𝑓 ) ↦ ( 𝑗 fClus ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 ) ) )
21 1 3 2 6 20 cmpo ⊢ ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ ( 𝑔 ∈ ( ∪ 𝑗 ↑m ∪ 𝑓 ) ↦ ( 𝑗 fClus ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 ) ) ) )
22 0 21 wceq ⊢ fClusf = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ ( 𝑔 ∈ ( ∪ 𝑗 ↑m ∪ 𝑓 ) ↦ ( 𝑗 fClus ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 ) ) ) )