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 
|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> A e. ( J fLim ( ( nei ` J ) ` { A } ) ) )

Proof

Step Hyp Ref Expression
1 ssid 
 |-  ( ( nei ` J ) ` { A } ) C_ ( ( nei ` J ) ` { A } )
2 1 jctr 
 |-  ( A e. X -> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ ( ( nei ` J ) ` { A } ) ) )
3 2 adantl 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ ( ( nei ` J ) ` { A } ) ) )
4 simpl 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> J e. ( TopOn ` X ) )
5 snssi 
 |-  ( A e. X -> { A } C_ X )
6 5 adantl 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> { A } C_ X )
7 snnzg 
 |-  ( A e. X -> { A } =/= (/) )
8 7 adantl 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> { A } =/= (/) )
9 neifil 
 |-  ( ( J e. ( TopOn ` X ) /\ { A } C_ X /\ { A } =/= (/) ) -> ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) )
10 4 6 8 9 syl3anc 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) )
11 elflim 
 |-  ( ( J e. ( TopOn ` X ) /\ ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) ) -> ( A e. ( J fLim ( ( nei ` J ) ` { A } ) ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ ( ( nei ` J ) ` { A } ) ) ) )
12 10 11 syldan 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( A e. ( J fLim ( ( nei ` J ) ` { A } ) ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ ( ( nei ` J ) ` { A } ) ) ) )
13 3 12 mpbird 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> A e. ( J fLim ( ( nei ` J ) ` { A } ) ) )