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 ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑁 ∈ 𝐹 )