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

Metamath Proof Explorer

Theorem fclssscls

Description: The set of cluster points is a subset of the closure of any filter element. (Contributed by Mario Carneiro, 11-Apr-2015) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion fclssscls 
|- ( S e. F -> ( J fClus F ) C_ ( ( cls ` J ) ` S ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 isfcls 
 |-  ( x e. ( J fClus F ) <-> ( J e. Top /\ F e. ( Fil ` U. J ) /\ A. s e. F x e. ( ( cls ` J ) ` s ) ) )
3 2 simp3bi 
 |-  ( x e. ( J fClus F ) -> A. s e. F x e. ( ( cls ` J ) ` s ) )
4 fveq2 
 |-  ( s = S -> ( ( cls ` J ) ` s ) = ( ( cls ` J ) ` S ) )
5 4 eleq2d 
 |-  ( s = S -> ( x e. ( ( cls ` J ) ` s ) <-> x e. ( ( cls ` J ) ` S ) ) )
6 5 rspcv 
 |-  ( S e. F -> ( A. s e. F x e. ( ( cls ` J ) ` s ) -> x e. ( ( cls ` J ) ` S ) ) )
7 3 6 syl5 
 |-  ( S e. F -> ( x e. ( J fClus F ) -> x e. ( ( cls ` J ) ` S ) ) )
8 7 ssrdv 
 |-  ( S e. F -> ( J fClus F ) C_ ( ( cls ` J ) ` S ) )