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