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 ∈ J fClus F ∧ U ∈ J ∧ A ∈ U ∧ S ∈ F → U ∩ S ≠ ∅

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 1 fclsfil ⊢ A ∈ J fClus F → F ∈ Fil ⁡ ⋃ J
3 fclstopon ⊢ A ∈ J fClus F → J ∈ TopOn ⁡ ⋃ J ↔ F ∈ Fil ⁡ ⋃ J
4 2 3 mpbird ⊢ A ∈ J fClus F → J ∈ TopOn ⁡ ⋃ J
5 fclsopn ⊢ J ∈ TopOn ⁡ ⋃ J ∧ F ∈ Fil ⁡ ⋃ J → A ∈ J fClus F ↔ A ∈ ⋃ J ∧ ∀ o ∈ J A ∈ o → ∀ s ∈ F o ∩ s ≠ ∅
6 4 2 5 syl2anc ⊢ A ∈ J fClus F → A ∈ J fClus F ↔ A ∈ ⋃ J ∧ ∀ o ∈ J A ∈ o → ∀ s ∈ F o ∩ s ≠ ∅
7 6 ibi ⊢ A ∈ J fClus F → A ∈ ⋃ J ∧ ∀ o ∈ J A ∈ o → ∀ s ∈ F o ∩ 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 ∈ F o ∩ s ≠ ∅ ↔ ∀ s ∈ F U ∩ s ≠ ∅
12 8 11 imbi12d ⊢ o = U → A ∈ o → ∀ s ∈ F o ∩ s ≠ ∅ ↔ A ∈ U → ∀ s ∈ F U ∩ s ≠ ∅
13 12 rspccv ⊢ ∀ o ∈ J A ∈ o → ∀ s ∈ F o ∩ s ≠ ∅ → U ∈ J → A ∈ U → ∀ s ∈ F U ∩ s ≠ ∅
14 7 13 simpl2im ⊢ A ∈ J fClus F → U ∈ J → A ∈ U → ∀ s ∈ F U ∩ s ≠ ∅
15 ineq2 ⊢ s = S → U ∩ s = U ∩ S
16 15 neeq1d ⊢ s = S → U ∩ s ≠ ∅ ↔ U ∩ S ≠ ∅
17 16 rspccv ⊢ ∀ s ∈ F U ∩ s ≠ ∅ → S ∈ F → U ∩ S ≠ ∅
18 14 17 syl8 ⊢ A ∈ J fClus F → U ∈ J → A ∈ U → S ∈ F → U ∩ S ≠ ∅
19 18 3imp2 ⊢ A ∈ J fClus F ∧ U ∈ J ∧ A ∈ U ∧ S ∈ F → U ∩ S ≠ ∅