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 ) )