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

Metamath Proof Explorer

Theorem flfssfcf

Description: A limit point of a function is a cluster point of the function. (Contributed by Jeff Hankins, 28-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion flfssfcf ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J fLimf L ⁡ F ⊆ J fClusf L ⁡ F

Proof

Step Hyp Ref Expression
1 flimfcls ⊢ J fLim X FilMap F ⁡ L ⊆ J fClus X FilMap F ⁡ L
2 1 a1i ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J fLim X FilMap F ⁡ L ⊆ J fClus X FilMap F ⁡ L
3 flfval ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J fLimf L ⁡ F = J fLim X FilMap F ⁡ L
4 fcfval ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J fClusf L ⁡ F = J fClus X FilMap F ⁡ L
5 2 3 4 3sstr4d ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J fLimf L ⁡ F ⊆ J fClusf L ⁡ F