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	⊢ ( 𝐽 fLim 𝐹 ) ⊆ ( 𝐽 fClus 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		flimtop	⊢ ( 𝑎 ∈ ( 𝐽 fLim 𝐹 ) → 𝐽 ∈ Top )
2		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
3	2	flimfil	⊢ ( 𝑎 ∈ ( 𝐽 fLim 𝐹 ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) )
4		flimclsi	⊢ ( 𝑥 ∈ 𝐹 → ( 𝐽 fLim 𝐹 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) )
5	4	sseld	⊢ ( 𝑥 ∈ 𝐹 → ( 𝑎 ∈ ( 𝐽 fLim 𝐹 ) → 𝑎 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) )
6	5	com12	⊢ ( 𝑎 ∈ ( 𝐽 fLim 𝐹 ) → ( 𝑥 ∈ 𝐹 → 𝑎 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) )
7	6	ralrimiv	⊢ ( 𝑎 ∈ ( 𝐽 fLim 𝐹 ) → ∀ 𝑥 ∈ 𝐹 𝑎 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) )
8	2	isfcls	⊢ ( 𝑎 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ∧ ∀ 𝑥 ∈ 𝐹 𝑎 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) )
9	1 3 7 8	syl3anbrc	⊢ ( 𝑎 ∈ ( 𝐽 fLim 𝐹 ) → 𝑎 ∈ ( 𝐽 fClus 𝐹 ) )
10	9	ssriv	⊢ ( 𝐽 fLim 𝐹 ) ⊆ ( 𝐽 fClus 𝐹 )