Metamath Proof Explorer

Theorem fclsneii

Description: A neighborhood of a cluster point of a filter intersects any element of that filter. (Contributed by Jeff Hankins, 11-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion fclsneii 
|- ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> ( N i^i S ) =/= (/) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> A e. ( J fClus F ) )
2 fclstop 
 |-  ( A e. ( J fClus F ) -> J e. Top )
3 1 2 syl 
 |-  ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> J e. Top )
4 simp2 
 |-  ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> N e. ( ( nei ` J ) ` { A } ) )
5 eqid 
 |-  U. J = U. J
6 5 neii1 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` { A } ) ) -> N C_ U. J )
7 3 4 6 syl2anc 
 |-  ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> N C_ U. J )
8 5 ntrss2 
 |-  ( ( J e. Top /\ N C_ U. J ) -> ( ( int ` J ) ` N ) C_ N )
9 3 7 8 syl2anc 
 |-  ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> ( ( int ` J ) ` N ) C_ N )
10 9 ssrind 
 |-  ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> ( ( ( int ` J ) ` N ) i^i S ) C_ ( N i^i S ) )
11 5 ntropn 
 |-  ( ( J e. Top /\ N C_ U. J ) -> ( ( int ` J ) ` N ) e. J )
12 3 7 11 syl2anc 
 |-  ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> ( ( int ` J ) ` N ) e. J )
13 5 fclselbas 
 |-  ( A e. ( J fClus F ) -> A e. U. J )
14 1 13 syl 
 |-  ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> A e. U. J )
15 14 snssd 
 |-  ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> { A } C_ U. J )
16 5 neiint 
 |-  ( ( J e. Top /\ { A } C_ U. J /\ N C_ U. J ) -> ( N e. ( ( nei ` J ) ` { A } ) <-> { A } C_ ( ( int ` J ) ` N ) ) )
17 3 15 7 16 syl3anc 
 |-  ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> ( N e. ( ( nei ` J ) ` { A } ) <-> { A } C_ ( ( int ` J ) ` N ) ) )
18 4 17 mpbid 
 |-  ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> { A } C_ ( ( int ` J ) ` N ) )
19 snssg 
 |-  ( A e. U. J -> ( A e. ( ( int ` J ) ` N ) <-> { A } C_ ( ( int ` J ) ` N ) ) )
20 14 19 syl 
 |-  ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> ( A e. ( ( int ` J ) ` N ) <-> { A } C_ ( ( int ` J ) ` N ) ) )
21 18 20 mpbird 
 |-  ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> A e. ( ( int ` J ) ` N ) )
22 simp3 
 |-  ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> S e. F )
23 fclsopni 
 |-  ( ( A e. ( J fClus F ) /\ ( ( ( int ` J ) ` N ) e. J /\ A e. ( ( int ` J ) ` N ) /\ S e. F ) ) -> ( ( ( int ` J ) ` N ) i^i S ) =/= (/) )
24 1 12 21 22 23 syl13anc 
 |-  ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> ( ( ( int ` J ) ` N ) i^i S ) =/= (/) )
25 ssn0 
 |-  ( ( ( ( ( int ` J ) ` N ) i^i S ) C_ ( N i^i S ) /\ ( ( ( int ` J ) ` N ) i^i S ) =/= (/) ) -> ( N i^i S ) =/= (/) )
26 10 24 25 syl2anc 
 |-  ( ( A e. ( J fClus F ) /\ N e. ( ( nei ` J ) ` { A } ) /\ S e. F ) -> ( N i^i S ) =/= (/) )