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 J fClus F N nei J A S F N S

Proof

Step Hyp Ref Expression
1 simp1 A J fClus F N nei J A S F A J fClus F
2 fclstop A J fClus F J Top
3 1 2 syl A J fClus F N nei J A S F J Top
4 simp2 A J fClus F N nei J A S F N nei J A
5 eqid J = J
6 5 neii1 J Top N nei J A N J
7 3 4 6 syl2anc A J fClus F N nei J A S F N J
8 5 ntrss2 J Top N J int J N N
9 3 7 8 syl2anc A J fClus F N nei J A S F int J N N
10 9 ssrind A J fClus F N nei J A S F int J N S N S
11 5 ntropn J Top N J int J N J
12 3 7 11 syl2anc A J fClus F N nei J A S F int J N J
13 5 fclselbas A J fClus F A J
14 1 13 syl A J fClus F N nei J A S F A J
15 14 snssd A J fClus F N nei J A S F A J
16 5 neiint J Top A J N J N nei J A A int J N
17 3 15 7 16 syl3anc A J fClus F N nei J A S F N nei J A A int J N
18 4 17 mpbid A J fClus F N nei J A S F A int J N
19 snssg A J A int J N A int J N
20 14 19 syl A J fClus F N nei J A S F A int J N A int J N
21 18 20 mpbird A J fClus F N nei J A S F A int J N
22 simp3 A J fClus F N nei J A S F S F
23 fclsopni A J fClus F int J N J A int J N S F int J N S
24 1 12 21 22 23 syl13anc A J fClus F N nei J A S F int J N S
25 ssn0 int J N S N S int J N S N S
26 10 24 25 syl2anc A J fClus F N nei J A S F N S