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

Metamath Proof Explorer

Theorem flimclsi

Description: The convergent points of a filter are a subset of the closure of any of the filter sets. (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion flimclsi ( 𝑆 ∈ 𝐹 → ( 𝐽 fLim 𝐹 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
2 1 flimfil ⊢ ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) )
3 2 ad2antlr ⊢ ( ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) )
4 flimnei ⊢ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → 𝑦 ∈ 𝐹 )
5 4 adantll ⊢ ( ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → 𝑦 ∈ 𝐹 )
6 simpll ⊢ ( ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → 𝑆 ∈ 𝐹 )
7 filinn0 ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ∧ 𝑦 ∈ 𝐹 ∧ 𝑆 ∈ 𝐹 ) → ( 𝑦 ∩ 𝑆 ) ≠ ∅ )
8 3 5 6 7 syl3anc ⊢ ( ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → ( 𝑦 ∩ 𝑆 ) ≠ ∅ )
9 8 ralrimiva ⊢ ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) → ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑦 ∩ 𝑆 ) ≠ ∅ )
10 flimtop ⊢ ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) → 𝐽 ∈ Top )
11 10 adantl ⊢ ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) → 𝐽 ∈ Top )
12 filelss ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ∧ 𝑆 ∈ 𝐹 ) → 𝑆 ⊆ ∪ 𝐽 )
13 12 ancoms ⊢ ( ( 𝑆 ∈ 𝐹 ∧ 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ) → 𝑆 ⊆ ∪ 𝐽 )
14 2 13 sylan2 ⊢ ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) → 𝑆 ⊆ ∪ 𝐽 )
15 1 flimelbas ⊢ ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) → 𝑥 ∈ ∪ 𝐽 )
16 15 adantl ⊢ ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) → 𝑥 ∈ ∪ 𝐽 )
17 1 neindisj2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ∧ 𝑥 ∈ ∪ 𝐽 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) )
18 11 14 16 17 syl3anc ⊢ ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) )
19 9 18 mpbird ⊢ ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
20 19 ex ⊢ ( 𝑆 ∈ 𝐹 → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
21 20 ssrdv ⊢ ( 𝑆 ∈ 𝐹 → ( 𝐽 fLim 𝐹 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )