# Metamath Proof Explorer

## Theorem fclsopn

Description: Write the cluster point condition in terms of open sets. (Contributed by Jeff Hankins, 10-Nov-2009) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion fclsopn $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → A ∈ J fClus F ↔ A ∈ X ∧ ∀ o ∈ J A ∈ o → ∀ s ∈ F o ∩ s ≠ ∅$

### Proof

Step Hyp Ref Expression
1 isfcls2 $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → A ∈ J fClus F ↔ ∀ s ∈ F A ∈ cls ⁡ J ⁡ s$
2 filn0 $⊢ F ∈ Fil ⁡ X → F ≠ ∅$
3 2 adantl $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → F ≠ ∅$
4 r19.2z $⊢ F ≠ ∅ ∧ ∀ s ∈ F A ∈ cls ⁡ J ⁡ s → ∃ s ∈ F A ∈ cls ⁡ J ⁡ s$
5 4 ex $⊢ F ≠ ∅ → ∀ s ∈ F A ∈ cls ⁡ J ⁡ s → ∃ s ∈ F A ∈ cls ⁡ J ⁡ s$
6 3 5 syl $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → ∀ s ∈ F A ∈ cls ⁡ J ⁡ s → ∃ s ∈ F A ∈ cls ⁡ J ⁡ s$
7 topontop $⊢ J ∈ TopOn ⁡ X → J ∈ Top$
8 7 ad2antrr $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ s ∈ F → J ∈ Top$
9 filelss $⊢ F ∈ Fil ⁡ X ∧ s ∈ F → s ⊆ X$
10 9 adantll $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ s ∈ F → s ⊆ X$
11 toponuni $⊢ J ∈ TopOn ⁡ X → X = ⋃ J$
12 11 ad2antrr $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ s ∈ F → X = ⋃ J$
13 10 12 sseqtrd $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ s ∈ F → s ⊆ ⋃ J$
14 eqid $⊢ ⋃ J = ⋃ J$
15 14 clsss3 $⊢ J ∈ Top ∧ s ⊆ ⋃ J → cls ⁡ J ⁡ s ⊆ ⋃ J$
16 8 13 15 syl2anc $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ s ∈ F → cls ⁡ J ⁡ s ⊆ ⋃ J$
17 16 12 sseqtrrd $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ s ∈ F → cls ⁡ J ⁡ s ⊆ X$
18 17 sseld $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ s ∈ F → A ∈ cls ⁡ J ⁡ s → A ∈ X$
19 18 rexlimdva $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → ∃ s ∈ F A ∈ cls ⁡ J ⁡ s → A ∈ X$
20 6 19 syld $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → ∀ s ∈ F A ∈ cls ⁡ J ⁡ s → A ∈ X$
21 20 pm4.71rd $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → ∀ s ∈ F A ∈ cls ⁡ J ⁡ s ↔ A ∈ X ∧ ∀ s ∈ F A ∈ cls ⁡ J ⁡ s$
22 7 ad3antrrr $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ A ∈ X ∧ s ∈ F → J ∈ Top$
23 13 adantlr $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ A ∈ X ∧ s ∈ F → s ⊆ ⋃ J$
24 simplr $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ A ∈ X ∧ s ∈ F → A ∈ X$
25 11 ad3antrrr $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ A ∈ X ∧ s ∈ F → X = ⋃ J$
26 24 25 eleqtrd $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ A ∈ X ∧ s ∈ F → A ∈ ⋃ J$
27 14 elcls $⊢ J ∈ Top ∧ s ⊆ ⋃ J ∧ A ∈ ⋃ J → A ∈ cls ⁡ J ⁡ s ↔ ∀ o ∈ J A ∈ o → o ∩ s ≠ ∅$
28 22 23 26 27 syl3anc $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ A ∈ X ∧ s ∈ F → A ∈ cls ⁡ J ⁡ s ↔ ∀ o ∈ J A ∈ o → o ∩ s ≠ ∅$
29 28 ralbidva $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ A ∈ X → ∀ s ∈ F A ∈ cls ⁡ J ⁡ s ↔ ∀ s ∈ F ∀ o ∈ J A ∈ o → o ∩ s ≠ ∅$
30 ralcom $⊢ ∀ s ∈ F ∀ o ∈ J A ∈ o → o ∩ s ≠ ∅ ↔ ∀ o ∈ J ∀ s ∈ F A ∈ o → o ∩ s ≠ ∅$
31 r19.21v $⊢ ∀ s ∈ F A ∈ o → o ∩ s ≠ ∅ ↔ A ∈ o → ∀ s ∈ F o ∩ s ≠ ∅$
32 31 ralbii $⊢ ∀ o ∈ J ∀ s ∈ F A ∈ o → o ∩ s ≠ ∅ ↔ ∀ o ∈ J A ∈ o → ∀ s ∈ F o ∩ s ≠ ∅$
33 30 32 bitri $⊢ ∀ s ∈ F ∀ o ∈ J A ∈ o → o ∩ s ≠ ∅ ↔ ∀ o ∈ J A ∈ o → ∀ s ∈ F o ∩ s ≠ ∅$
34 29 33 bitrdi $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ A ∈ X → ∀ s ∈ F A ∈ cls ⁡ J ⁡ s ↔ ∀ o ∈ J A ∈ o → ∀ s ∈ F o ∩ s ≠ ∅$
35 34 pm5.32da $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → A ∈ X ∧ ∀ s ∈ F A ∈ cls ⁡ J ⁡ s ↔ A ∈ X ∧ ∀ o ∈ J A ∈ o → ∀ s ∈ F o ∩ s ≠ ∅$
36 1 21 35 3bitrd $⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → A ∈ J fClus F ↔ A ∈ X ∧ ∀ o ∈ J A ∈ o → ∀ s ∈ F o ∩ s ≠ ∅$