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 \in F \to J fClus F \subseteq cls (J) (S)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2	1	isfcls	$⊢ x \in (J fClus F) \leftrightarrow (J \in Top \land F \in Fil (⋃ J) \land \forall s \in F x \in cls (J) (s))$
3	2	simp3bi	$⊢ x \in (J fClus F) \to \forall s \in F x \in cls (J) (s)$
4		fveq2	$⊢ s = S \to cls (J) (s) = cls (J) (S)$
5	4	eleq2d	$⊢ s = S \to (x \in cls (J) (s) \leftrightarrow x \in cls (J) (S))$
6	5	rspcv	$⊢ S \in F \to (\forall s \in F x \in cls (J) (s) \to x \in cls (J) (S))$
7	3 6	syl5	$⊢ S \in F \to (x \in (J fClus F) \to x \in cls (J) (S))$
8	7	ssrdv	$⊢ S \in F \to J fClus F \subseteq cls (J) (S)$