This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem neiflim

Description: A point is a limit point of its neighborhood filter. (Contributed by Jeff Hankins, 7-Sep-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion neiflim ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )

Proof

Step Hyp Ref Expression
1 ssid ⊢ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } )
2 1 jctr ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
3 2 adantl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
4 simpl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5 snssi ⊢ ( 𝐴 ∈ 𝑋 → { 𝐴 } ⊆ 𝑋 )
6 5 adantl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → { 𝐴 } ⊆ 𝑋 )
7 snnzg ⊢ ( 𝐴 ∈ 𝑋 → { 𝐴 } ≠ ∅ )
8 7 adantl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → { 𝐴 } ≠ ∅ )
9 neifil ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ { 𝐴 } ⊆ 𝑋 ∧ { 𝐴 } ≠ ∅ ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) )
10 4 6 8 9 syl3anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) )
11 elflim ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) )
12 10 11 syldan ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) )
13 3 12 mpbird ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )