Metamath Proof Explorer


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