Metamath Proof Explorer

Theorem neiflim

Description: A point is a limit point of its neighborhood filter. (Contributed by Jeff Hankins, 7-Sep-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion neiflim ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → A ∈ J fLim nei ⁡ J ⁡ A

Proof

Step Hyp Ref Expression
1 ssid ⊢ nei ⁡ J ⁡ A ⊆ nei ⁡ J ⁡ A
2 1 jctr ⊢ A ∈ X → A ∈ X ∧ nei ⁡ J ⁡ A ⊆ nei ⁡ J ⁡ A
3 2 adantl ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → A ∈ X ∧ nei ⁡ J ⁡ A ⊆ nei ⁡ J ⁡ A
4 simpl ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → J ∈ TopOn ⁡ X
5 snssi ⊢ A ∈ X → A ⊆ X
6 5 adantl ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → A ⊆ X
7 snnzg ⊢ A ∈ X → A ≠ ∅
8 7 adantl ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → A ≠ ∅
9 neifil ⊢ J ∈ TopOn ⁡ X ∧ A ⊆ X ∧ A ≠ ∅ → nei ⁡ J ⁡ A ∈ Fil ⁡ X
10 4 6 8 9 syl3anc ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → nei ⁡ J ⁡ A ∈ Fil ⁡ X
11 elflim ⊢ J ∈ TopOn ⁡ X ∧ nei ⁡ J ⁡ A ∈ Fil ⁡ X → A ∈ J fLim nei ⁡ J ⁡ A ↔ A ∈ X ∧ nei ⁡ J ⁡ A ⊆ nei ⁡ J ⁡ A
12 10 11 syldan ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → A ∈ J fLim nei ⁡ J ⁡ A ↔ A ∈ X ∧ nei ⁡ J ⁡ A ⊆ nei ⁡ J ⁡ A
13 3 12 mpbird ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → A ∈ J fLim nei ⁡ J ⁡ A