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 syl5ibr
 |-  ( ( 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 ) =/= (/) ) ) )