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 ‘ 𝐽 ) ‘ { 𝐴 } ) ) )