Metamath Proof Explorer

Theorem flimfcls

Description: A limit point is a cluster point. (Contributed by Jeff Hankins, 12-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion flimfcls 
|- ( J fLim F ) C_ ( J fClus F )

Proof

Step Hyp Ref Expression
1 flimtop 
 |-  ( a e. ( J fLim F ) -> J e. Top )
2 eqid 
 |-  U. J = U. J
3 2 flimfil 
 |-  ( a e. ( J fLim F ) -> F e. ( Fil ` U. J ) )
4 flimclsi 
 |-  ( x e. F -> ( J fLim F ) C_ ( ( cls ` J ) ` x ) )
5 4 sseld 
 |-  ( x e. F -> ( a e. ( J fLim F ) -> a e. ( ( cls ` J ) ` x ) ) )
6 5 com12 
 |-  ( a e. ( J fLim F ) -> ( x e. F -> a e. ( ( cls ` J ) ` x ) ) )
7 6 ralrimiv 
 |-  ( a e. ( J fLim F ) -> A. x e. F a e. ( ( cls ` J ) ` x ) )
8 2 isfcls 
 |-  ( a e. ( J fClus F ) <-> ( J e. Top /\ F e. ( Fil ` U. J ) /\ A. x e. F a e. ( ( cls ` J ) ` x ) ) )
9 1 3 7 8 syl3anbrc 
 |-  ( a e. ( J fLim F ) -> a e. ( J fClus F ) )
10 9 ssriv 
 |-  ( J fLim F ) C_ ( J fClus F )