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 )