Metamath Proof Explorer

Theorem fcfnei

Description: The property of being a cluster point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 26-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion fcfnei 
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fClusf L ) ` F ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) A. s e. L ( n i^i ( F " s ) ) =/= (/) ) ) )

Proof

Step Hyp Ref Expression
1 isfcf 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fClusf L ) ` F ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) ) ) )
2 simpll1 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> J e. ( TopOn ` X ) )
3 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
4 2 3 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> J e. Top )
5 simpr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> n e. ( ( nei ` J ) ` { A } ) )
6 eqid 
 |-  U. J = U. J
7 6 neii1 
 |-  ( ( J e. Top /\ n e. ( ( nei ` J ) ` { A } ) ) -> n C_ U. J )
8 4 5 7 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> n C_ U. J )
9 6 ntrss2 
 |-  ( ( J e. Top /\ n C_ U. J ) -> ( ( int ` J ) ` n ) C_ n )
10 4 8 9 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> ( ( int ` J ) ` n ) C_ n )
11 simplr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> A e. X )
12 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
13 2 12 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> X = U. J )
14 11 13 eleqtrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> A e. U. J )
15 14 snssd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> { A } C_ U. J )
16 6 neiint 
 |-  ( ( J e. Top /\ { A } C_ U. J /\ n C_ U. J ) -> ( n e. ( ( nei ` J ) ` { A } ) <-> { A } C_ ( ( int ` J ) ` n ) ) )
17 4 15 8 16 syl3anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> ( n e. ( ( nei ` J ) ` { A } ) <-> { A } C_ ( ( int ` J ) ` n ) ) )
18 5 17 mpbid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> { A } C_ ( ( int ` J ) ` n ) )
19 snssg 
 |-  ( A e. X -> ( A e. ( ( int ` J ) ` n ) <-> { A } C_ ( ( int ` J ) ` n ) ) )
20 11 19 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> ( A e. ( ( int ` J ) ` n ) <-> { A } C_ ( ( int ` J ) ` n ) ) )
21 18 20 mpbird 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> A e. ( ( int ` J ) ` n ) )
22 6 ntropn 
 |-  ( ( J e. Top /\ n C_ U. J ) -> ( ( int ` J ) ` n ) e. J )
23 4 8 22 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> ( ( int ` J ) ` n ) e. J )
24 eleq2 
 |-  ( o = ( ( int ` J ) ` n ) -> ( A e. o <-> A e. ( ( int ` J ) ` n ) ) )
25 ineq1 
 |-  ( o = ( ( int ` J ) ` n ) -> ( o i^i ( F " s ) ) = ( ( ( int ` J ) ` n ) i^i ( F " s ) ) )
26 25 neeq1d 
 |-  ( o = ( ( int ` J ) ` n ) -> ( ( o i^i ( F " s ) ) =/= (/) <-> ( ( ( int ` J ) ` n ) i^i ( F " s ) ) =/= (/) ) )
27 26 ralbidv 
 |-  ( o = ( ( int ` J ) ` n ) -> ( A. s e. L ( o i^i ( F " s ) ) =/= (/) <-> A. s e. L ( ( ( int ` J ) ` n ) i^i ( F " s ) ) =/= (/) ) )
28 24 27 imbi12d 
 |-  ( o = ( ( int ` J ) ` n ) -> ( ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) <-> ( A e. ( ( int ` J ) ` n ) -> A. s e. L ( ( ( int ` J ) ` n ) i^i ( F " s ) ) =/= (/) ) ) )
29 28 rspcv 
 |-  ( ( ( int ` J ) ` n ) e. J -> ( A. o e. J ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) -> ( A e. ( ( int ` J ) ` n ) -> A. s e. L ( ( ( int ` J ) ` n ) i^i ( F " s ) ) =/= (/) ) ) )
30 23 29 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> ( A. o e. J ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) -> ( A e. ( ( int ` J ) ` n ) -> A. s e. L ( ( ( int ` J ) ` n ) i^i ( F " s ) ) =/= (/) ) ) )
31 21 30 mpid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> ( A. o e. J ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) -> A. s e. L ( ( ( int ` J ) ` n ) i^i ( F " s ) ) =/= (/) ) )
32 ssrin 
 |-  ( ( ( int ` J ) ` n ) C_ n -> ( ( ( int ` J ) ` n ) i^i ( F " s ) ) C_ ( n i^i ( F " s ) ) )
33 ssn0 
 |-  ( ( ( ( ( int ` J ) ` n ) i^i ( F " s ) ) C_ ( n i^i ( F " s ) ) /\ ( ( ( int ` J ) ` n ) i^i ( F " s ) ) =/= (/) ) -> ( n i^i ( F " s ) ) =/= (/) )
34 33 ex 
 |-  ( ( ( ( int ` J ) ` n ) i^i ( F " s ) ) C_ ( n i^i ( F " s ) ) -> ( ( ( ( int ` J ) ` n ) i^i ( F " s ) ) =/= (/) -> ( n i^i ( F " s ) ) =/= (/) ) )
35 32 34 syl 
 |-  ( ( ( int ` J ) ` n ) C_ n -> ( ( ( ( int ` J ) ` n ) i^i ( F " s ) ) =/= (/) -> ( n i^i ( F " s ) ) =/= (/) ) )
36 35 ralimdv 
 |-  ( ( ( int ` J ) ` n ) C_ n -> ( A. s e. L ( ( ( int ` J ) ` n ) i^i ( F " s ) ) =/= (/) -> A. s e. L ( n i^i ( F " s ) ) =/= (/) ) )
37 10 31 36 sylsyld 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ n e. ( ( nei ` J ) ` { A } ) ) -> ( A. o e. J ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) -> A. s e. L ( n i^i ( F " s ) ) =/= (/) ) )
38 37 ralrimdva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> ( A. o e. J ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) -> A. n e. ( ( nei ` J ) ` { A } ) A. s e. L ( n i^i ( F " s ) ) =/= (/) ) )
39 simpl1 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> J e. ( TopOn ` X ) )
40 39 3 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> J e. Top )
41 opnneip 
 |-  ( ( J e. Top /\ o e. J /\ A e. o ) -> o e. ( ( nei ` J ) ` { A } ) )
42 41 3expb 
 |-  ( ( J e. Top /\ ( o e. J /\ A e. o ) ) -> o e. ( ( nei ` J ) ` { A } ) )
43 40 42 sylan 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> o e. ( ( nei ` J ) ` { A } ) )
44 ineq1 
 |-  ( n = o -> ( n i^i ( F " s ) ) = ( o i^i ( F " s ) ) )
45 44 neeq1d 
 |-  ( n = o -> ( ( n i^i ( F " s ) ) =/= (/) <-> ( o i^i ( F " s ) ) =/= (/) ) )
46 45 ralbidv 
 |-  ( n = o -> ( A. s e. L ( n i^i ( F " s ) ) =/= (/) <-> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) )
47 46 rspcv 
 |-  ( o e. ( ( nei ` J ) ` { A } ) -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. L ( n i^i ( F " s ) ) =/= (/) -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) )
48 43 47 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. L ( n i^i ( F " s ) ) =/= (/) -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) )
49 48 expr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ o e. J ) -> ( A e. o -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. L ( n i^i ( F " s ) ) =/= (/) -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) ) )
50 49 com23 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) /\ o e. J ) -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. L ( n i^i ( F " s ) ) =/= (/) -> ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) ) )
51 50 ralrimdva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> ( A. n e. ( ( nei ` J ) ` { A } ) A. s e. L ( n i^i ( F " s ) ) =/= (/) -> A. o e. J ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) ) )
52 38 51 impbid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> ( A. o e. J ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) <-> A. n e. ( ( nei ` J ) ` { A } ) A. s e. L ( n i^i ( F " s ) ) =/= (/) ) )
53 52 pm5.32da 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( A e. X /\ A. o e. J ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) A. s e. L ( n i^i ( F " s ) ) =/= (/) ) ) )
54 1 53 bitrd 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fClusf L ) ` F ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) A. s e. L ( n i^i ( F " s ) ) =/= (/) ) ) )