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 \subseteq J fClus F$

Step	Hyp	Ref	Expression
1		flimtop	$⊢ a \in (J fLim F) \to J \in Top$
2		eqid	$⊢ ⋃ J = ⋃ J$
3	2	flimfil	$⊢ a \in (J fLim F) \to F \in Fil (⋃ J)$
4		flimclsi	$⊢ x \in F \to J fLim F \subseteq cls (J) (x)$
5	4	sseld	$⊢ x \in F \to (a \in (J fLim F) \to a \in cls (J) (x))$
6	5	com12	$⊢ a \in (J fLim F) \to (x \in F \to a \in cls (J) (x))$
7	6	ralrimiv	$⊢ a \in (J fLim F) \to \forall x \in F a \in cls (J) (x)$
8	2	isfcls	$⊢ a \in (J fClus F) \leftrightarrow (J \in Top \land F \in Fil (⋃ J) \land \forall x \in F a \in cls (J) (x))$
9	1 3 7 8	syl3anbrc	$⊢ a \in (J fLim F) \to a \in (J fClus F)$
10	9	ssriv	$⊢ J fLim F \subseteq J fClus F$

Metamath Proof Explorer