This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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