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 e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) C_ ( ( J fClusf L ) ` F ) )

Proof

Step Hyp Ref Expression
1 flimfcls 
 |-  ( J fLim ( ( X FilMap F ) ` L ) ) C_ ( J fClus ( ( X FilMap F ) ` L ) )
2 1 a1i 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( J fLim ( ( X FilMap F ) ` L ) ) C_ ( J fClus ( ( X FilMap F ) ` L ) ) )
3 flfval 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
4 fcfval 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fClusf L ) ` F ) = ( J fClus ( ( X FilMap F ) ` L ) ) )
5 2 3 4 3sstr4d 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) C_ ( ( J fClusf L ) ` F ) )