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 ⊢ S ∈ F → J fLim F ⊆ cls ⁡ J ⁡ S

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 1 flimfil ⊢ x ∈ J fLim F → F ∈ Fil ⁡ ⋃ J
3 2 ad2antlr ⊢ S ∈ F ∧ x ∈ J fLim F ∧ y ∈ nei ⁡ J ⁡ x → F ∈ Fil ⁡ ⋃ J
4 flimnei ⊢ x ∈ J fLim F ∧ y ∈ nei ⁡ J ⁡ x → y ∈ F
5 4 adantll ⊢ S ∈ F ∧ x ∈ J fLim F ∧ y ∈ nei ⁡ J ⁡ x → y ∈ F
6 simpll ⊢ S ∈ F ∧ x ∈ J fLim F ∧ y ∈ nei ⁡ J ⁡ x → S ∈ F
7 filinn0 ⊢ F ∈ Fil ⁡ ⋃ J ∧ y ∈ F ∧ S ∈ F → y ∩ S ≠ ∅
8 3 5 6 7 syl3anc ⊢ S ∈ F ∧ x ∈ J fLim F ∧ y ∈ nei ⁡ J ⁡ x → y ∩ S ≠ ∅
9 8 ralrimiva ⊢ S ∈ F ∧ x ∈ J fLim F → ∀ y ∈ nei ⁡ J ⁡ x y ∩ S ≠ ∅
10 flimtop ⊢ x ∈ J fLim F → J ∈ Top
11 10 adantl ⊢ S ∈ F ∧ x ∈ J fLim F → J ∈ Top
12 filelss ⊢ F ∈ Fil ⁡ ⋃ J ∧ S ∈ F → S ⊆ ⋃ J
13 12 ancoms ⊢ S ∈ F ∧ F ∈ Fil ⁡ ⋃ J → S ⊆ ⋃ J
14 2 13 sylan2 ⊢ S ∈ F ∧ x ∈ J fLim F → S ⊆ ⋃ J
15 1 flimelbas ⊢ x ∈ J fLim F → x ∈ ⋃ J
16 15 adantl ⊢ S ∈ F ∧ x ∈ J fLim F → x ∈ ⋃ J
17 1 neindisj2 ⊢ J ∈ Top ∧ S ⊆ ⋃ J ∧ x ∈ ⋃ J → x ∈ cls ⁡ J ⁡ S ↔ ∀ y ∈ nei ⁡ J ⁡ x y ∩ S ≠ ∅
18 11 14 16 17 syl3anc ⊢ S ∈ F ∧ x ∈ J fLim F → x ∈ cls ⁡ J ⁡ S ↔ ∀ y ∈ nei ⁡ J ⁡ x y ∩ S ≠ ∅
19 9 18 mpbird ⊢ S ∈ F ∧ x ∈ J fLim F → x ∈ cls ⁡ J ⁡ S
20 19 ex ⊢ S ∈ F → x ∈ J fLim F → x ∈ cls ⁡ J ⁡ S
21 20 ssrdv ⊢ S ∈ F → J fLim F ⊆ cls ⁡ J ⁡ S