Metamath Proof Explorer


Theorem flimnei

Description: A filter contains all of the neighborhoods of its limit points. (Contributed by Jeff Hankins, 4-Sep-2009) (Revised by Mario Carneiro, 9-Apr-2015)

Ref Expression
Assertion flimnei ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑁𝐹 )

Proof

Step Hyp Ref Expression
1 flimneiss ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 )
2 1 sselda ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑁𝐹 )