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 ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → ( 𝑁𝑆 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 simp1 ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → 𝐴 ∈ ( 𝐽 fClus 𝐹 ) )
2 fclstop ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐽 ∈ Top )
3 1 2 syl ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → 𝐽 ∈ Top )
4 simp2 ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
5 eqid 𝐽 = 𝐽
6 5 neii1 ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑁 𝐽 )
7 3 4 6 syl2anc ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → 𝑁 𝐽 )
8 5 ntrss2 ( ( 𝐽 ∈ Top ∧ 𝑁 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ⊆ 𝑁 )
9 3 7 8 syl2anc ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ⊆ 𝑁 )
10 9 ssrind ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∩ 𝑆 ) ⊆ ( 𝑁𝑆 ) )
11 5 ntropn ( ( 𝐽 ∈ Top ∧ 𝑁 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∈ 𝐽 )
12 3 7 11 syl2anc ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∈ 𝐽 )
13 5 fclselbas ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐴 𝐽 )
14 1 13 syl ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → 𝐴 𝐽 )
15 14 snssd ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → { 𝐴 } ⊆ 𝐽 )
16 5 neiint ( ( 𝐽 ∈ Top ∧ { 𝐴 } ⊆ 𝐽𝑁 𝐽 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ↔ { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) )
17 3 15 7 16 syl3anc ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ↔ { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) )
18 4 17 mpbid ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) )
19 snssg ( 𝐴 𝐽 → ( 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ↔ { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) )
20 14 19 syl ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → ( 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ↔ { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) )
21 18 20 mpbird ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) )
22 simp3 ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → 𝑆𝐹 )
23 fclsopni ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ ( ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∈ 𝐽𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∧ 𝑆𝐹 ) ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∩ 𝑆 ) ≠ ∅ )
24 1 12 21 22 23 syl13anc ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∩ 𝑆 ) ≠ ∅ )
25 ssn0 ( ( ( ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∩ 𝑆 ) ⊆ ( 𝑁𝑆 ) ∧ ( ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∩ 𝑆 ) ≠ ∅ ) → ( 𝑁𝑆 ) ≠ ∅ )
26 10 24 25 syl2anc ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆𝐹 ) → ( 𝑁𝑆 ) ≠ ∅ )