Metamath Proof Explorer

Theorem fclsopni

Description: An open neighborhood of a cluster point of a filter intersects any element of that filter. (Contributed by Mario Carneiro, 11-Apr-2015) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion fclsopni ⊢A∈JfClusF∧U∈J∧A∈U∧S∈F→U∩S≠∅

Proof

Step Hyp Ref Expression
1 eqid ⊢⋃J=⋃J
2 1 fclsfil ⊢A∈JfClusF→F∈Fil⁡⋃J
3 fclstopon ⊢A∈JfClusF→J∈TopOn⁡⋃J↔F∈Fil⁡⋃J
4 2 3 mpbird ⊢A∈JfClusF→J∈TopOn⁡⋃J
5 fclsopn ⊢J∈TopOn⁡⋃J∧F∈Fil⁡⋃J→A∈JfClusF↔A∈⋃J∧∀o∈JA∈o→∀s∈Fo∩s≠∅
6 4 2 5 syl2anc ⊢A∈JfClusF→A∈JfClusF↔A∈⋃J∧∀o∈JA∈o→∀s∈Fo∩s≠∅
7 6 ibi ⊢A∈JfClusF→A∈⋃J∧∀o∈JA∈o→∀s∈Fo∩s≠∅
8 eleq2 ⊢o=U→A∈o↔A∈U
9 ineq1 ⊢o=U→o∩s=U∩s
10 9 neeq1d ⊢o=U→o∩s≠∅↔U∩s≠∅
11 10 ralbidv ⊢o=U→∀s∈Fo∩s≠∅↔∀s∈FU∩s≠∅
12 8 11 imbi12d ⊢o=U→A∈o→∀s∈Fo∩s≠∅↔A∈U→∀s∈FU∩s≠∅
13 12 rspccv ⊢∀o∈JA∈o→∀s∈Fo∩s≠∅→U∈J→A∈U→∀s∈FU∩s≠∅
14 7 13 simpl2im ⊢A∈JfClusF→U∈J→A∈U→∀s∈FU∩s≠∅
15 ineq2 ⊢s=S→U∩s=U∩S
16 15 neeq1d ⊢s=S→U∩s≠∅↔U∩S≠∅
17 16 rspccv ⊢∀s∈FU∩s≠∅→S∈F→U∩S≠∅
18 14 17 syl8 ⊢A∈JfClusF→U∈J→A∈U→S∈F→U∩S≠∅
19 18 3imp2 ⊢A∈JfClusF∧U∈J∧A∈U∧S∈F→U∩S≠∅