Metamath Proof Explorer

Theorem fclsnei

Description: Cluster points in terms of neighborhoods. (Contributed by Jeff Hankins, 11-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion fclsnei 
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 fclselbas 
 |-  ( A e. ( J fClus F ) -> A e. U. J )
3 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
4 3 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> X = U. J )
5 4 eleq2d 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. X <-> A e. U. J ) )
6 2 5 imbitrrid 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) -> A e. X ) )
7 fclsneii 
 |-  ( ( A e. ( J fClus F ) /\ n e. ( ( nei ` J ) ` { A } ) /\ s e. F ) -> ( n i^i s ) =/= (/) )
8 7 3expb 
 |-  ( ( A e. ( J fClus F ) /\ ( n e. ( ( nei ` J ) ` { A } ) /\ s e. F ) ) -> ( n i^i s ) =/= (/) )
9 8 ralrimivva 
 |-  ( A e. ( J fClus F ) -> A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) )
10 6 9 jca2 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) -> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) ) ) )
11 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
12 11 ad3antrrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> J e. Top )
13 simprl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> o e. J )
14 simprr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> A e. o )
15 opnneip 
 |-  ( ( J e. Top /\ o e. J /\ A e. o ) -> o e. ( ( nei ` J ) ` { A } ) )
16 12 13 14 15 syl3anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> o e. ( ( nei ` J ) ` { A } ) )
17 ineq1 
 |-  ( n = o -> ( n i^i s ) = ( o i^i s ) )
18 17 neeq1d 
 |-  ( n = o -> ( ( n i^i s ) =/= (/) <-> ( o i^i s ) =/= (/) ) )
19 18 ralbidv 
 |-  ( n = o -> ( A. s e. F ( n i^i s ) =/= (/) <-> A. s e. F ( o i^i s ) =/= (/) ) )
20 19 rspcv 
 |-  ( o e. ( ( nei ` J ) ` { A } ) -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) -> A. s e. F ( o i^i s ) =/= (/) ) )
21 16 20 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) -> A. s e. F ( o i^i s ) =/= (/) ) )
22 21 expr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ o e. J ) -> ( A e. o -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) -> A. s e. F ( o i^i s ) =/= (/) ) ) )
23 22 com23 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ o e. J ) -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) -> ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) )
24 23 ralrimdva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) -> A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) )
25 24 imdistanda 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) ) -> ( A e. X /\ A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) )
26 fclsopn 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) )
27 25 26 sylibrd 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) ) -> A e. ( J fClus F ) ) )
28 10 27 impbid 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) A. s e. F ( n i^i s ) =/= (/) ) ) )