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
|- ( ( A e. ( J fLim F ) /\ N e. ( ( nei ` J ) ` { A } ) ) -> N e. F )

Proof

Step Hyp Ref Expression
1 flimneiss
 |-  ( A e. ( J fLim F ) -> ( ( nei ` J ) ` { A } ) C_ F )
2 1 sselda
 |-  ( ( A e. ( J fLim F ) /\ N e. ( ( nei ` J ) ` { A } ) ) -> N e. F )