This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Filters and filter bases Filter limits 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 ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑁 ∈ 𝐹 )