# Metamath Proof Explorer

## Theorem fclscmp

Description: A space is compact iff every filter clusters. (Contributed by Jeff Hankins, 20-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion fclscmp $⊢ J ∈ TopOn ⁡ X → J ∈ Comp ↔ ∀ f ∈ Fil ⁡ X J fClus f ≠ ∅$

### Proof

Step Hyp Ref Expression
1 eqid $⊢ ⋃ J = ⋃ J$
2 1 fclscmpi $⊢ J ∈ Comp ∧ f ∈ Fil ⁡ ⋃ J → J fClus f ≠ ∅$
3 2 ralrimiva $⊢ J ∈ Comp → ∀ f ∈ Fil ⁡ ⋃ J J fClus f ≠ ∅$
4 toponuni $⊢ J ∈ TopOn ⁡ X → X = ⋃ J$
5 4 fveq2d $⊢ J ∈ TopOn ⁡ X → Fil ⁡ X = Fil ⁡ ⋃ J$
6 5 raleqdv $⊢ J ∈ TopOn ⁡ X → ∀ f ∈ Fil ⁡ X J fClus f ≠ ∅ ↔ ∀ f ∈ Fil ⁡ ⋃ J J fClus f ≠ ∅$
7 3 6 syl5ibr $⊢ J ∈ TopOn ⁡ X → J ∈ Comp → ∀ f ∈ Fil ⁡ X J fClus f ≠ ∅$
8 elpwi $⊢ x ∈ 𝒫 Clsd ⁡ J → x ⊆ Clsd ⁡ J$
9 vn0 $⊢ V ≠ ∅$
10 simpr $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x = ∅ → x = ∅$
11 10 inteqd $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x = ∅ → ⋂ x = ⋂ ∅$
12 int0 $⊢ ⋂ ∅ = V$
13 11 12 eqtrdi $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x = ∅ → ⋂ x = V$
14 13 neeq1d $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x = ∅ → ⋂ x ≠ ∅ ↔ V ≠ ∅$
15 9 14 mpbiri $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x = ∅ → ⋂ x ≠ ∅$
16 15 a1d $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x = ∅ → ∀ f ∈ Fil ⁡ X J fClus f ≠ ∅ → ⋂ x ≠ ∅$
17 ssfii $⊢ x ∈ V → x ⊆ fi ⁡ x$
18 17 elv $⊢ x ⊆ fi ⁡ x$
19 simplrl $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ → x ⊆ Clsd ⁡ J$
20 1 cldss2 $⊢ Clsd ⁡ J ⊆ 𝒫 ⋃ J$
21 4 ad2antrr $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ → X = ⋃ J$
22 21 pweqd $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ → 𝒫 X = 𝒫 ⋃ J$
23 20 22 sseqtrrid $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ → Clsd ⁡ J ⊆ 𝒫 X$
24 19 23 sstrd $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ → x ⊆ 𝒫 X$
25 simpr $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ → x ≠ ∅$
26 simplrr $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ → ¬ ∅ ∈ fi ⁡ x$
27 toponmax $⊢ J ∈ TopOn ⁡ X → X ∈ J$
28 27 ad2antrr $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ → X ∈ J$
29 fsubbas $⊢ X ∈ J → fi ⁡ x ∈ fBas ⁡ X ↔ x ⊆ 𝒫 X ∧ x ≠ ∅ ∧ ¬ ∅ ∈ fi ⁡ x$
30 28 29 syl $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ → fi ⁡ x ∈ fBas ⁡ X ↔ x ⊆ 𝒫 X ∧ x ≠ ∅ ∧ ¬ ∅ ∈ fi ⁡ x$
31 24 25 26 30 mpbir3and $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ → fi ⁡ x ∈ fBas ⁡ X$
32 ssfg $⊢ fi ⁡ x ∈ fBas ⁡ X → fi ⁡ x ⊆ X filGen fi ⁡ x$
33 31 32 syl $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ → fi ⁡ x ⊆ X filGen fi ⁡ x$
34 18 33 sstrid $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ → x ⊆ X filGen fi ⁡ x$
35 34 sselda $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ ∧ y ∈ x → y ∈ X filGen fi ⁡ x$
36 fclssscls $⊢ y ∈ X filGen fi ⁡ x → J fClus X filGen fi ⁡ x ⊆ cls ⁡ J ⁡ y$
37 35 36 syl $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ ∧ y ∈ x → J fClus X filGen fi ⁡ x ⊆ cls ⁡ J ⁡ y$
38 19 sselda $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ ∧ y ∈ x → y ∈ Clsd ⁡ J$
39 cldcls $⊢ y ∈ Clsd ⁡ J → cls ⁡ J ⁡ y = y$
40 38 39 syl $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ ∧ y ∈ x → cls ⁡ J ⁡ y = y$
41 37 40 sseqtrd $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ ∧ y ∈ x → J fClus X filGen fi ⁡ x ⊆ y$
42 41 ralrimiva $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ → ∀ y ∈ x J fClus X filGen fi ⁡ x ⊆ y$
43 ssint $⊢ J fClus X filGen fi ⁡ x ⊆ ⋂ x ↔ ∀ y ∈ x J fClus X filGen fi ⁡ x ⊆ y$
44 42 43 sylibr $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ → J fClus X filGen fi ⁡ x ⊆ ⋂ x$
45 fgcl $⊢ fi ⁡ x ∈ fBas ⁡ X → X filGen fi ⁡ x ∈ Fil ⁡ X$
46 oveq2 $⊢ f = X filGen fi ⁡ x → J fClus f = J fClus X filGen fi ⁡ x$
47 46 neeq1d $⊢ f = X filGen fi ⁡ x → J fClus f ≠ ∅ ↔ J fClus X filGen fi ⁡ x ≠ ∅$
48 47 rspcv $⊢ X filGen fi ⁡ x ∈ Fil ⁡ X → ∀ f ∈ Fil ⁡ X J fClus f ≠ ∅ → J fClus X filGen fi ⁡ x ≠ ∅$
49 31 45 48 3syl $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ → ∀ f ∈ Fil ⁡ X J fClus f ≠ ∅ → J fClus X filGen fi ⁡ x ≠ ∅$
50 ssn0 $⊢ J fClus X filGen fi ⁡ x ⊆ ⋂ x ∧ J fClus X filGen fi ⁡ x ≠ ∅ → ⋂ x ≠ ∅$
51 44 49 50 syl6an $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x ∧ x ≠ ∅ → ∀ f ∈ Fil ⁡ X J fClus f ≠ ∅ → ⋂ x ≠ ∅$
52 16 51 pm2.61dane $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J ∧ ¬ ∅ ∈ fi ⁡ x → ∀ f ∈ Fil ⁡ X J fClus f ≠ ∅ → ⋂ x ≠ ∅$
53 52 expr $⊢ J ∈ TopOn ⁡ X ∧ x ⊆ Clsd ⁡ J → ¬ ∅ ∈ fi ⁡ x → ∀ f ∈ Fil ⁡ X J fClus f ≠ ∅ → ⋂ x ≠ ∅$
54 8 53 sylan2 $⊢ J ∈ TopOn ⁡ X ∧ x ∈ 𝒫 Clsd ⁡ J → ¬ ∅ ∈ fi ⁡ x → ∀ f ∈ Fil ⁡ X J fClus f ≠ ∅ → ⋂ x ≠ ∅$
55 54 com23 $⊢ J ∈ TopOn ⁡ X ∧ x ∈ 𝒫 Clsd ⁡ J → ∀ f ∈ Fil ⁡ X J fClus f ≠ ∅ → ¬ ∅ ∈ fi ⁡ x → ⋂ x ≠ ∅$
56 55 ralrimdva $⊢ J ∈ TopOn ⁡ X → ∀ f ∈ Fil ⁡ X J fClus f ≠ ∅ → ∀ x ∈ 𝒫 Clsd ⁡ J ¬ ∅ ∈ fi ⁡ x → ⋂ x ≠ ∅$
57 topontop $⊢ J ∈ TopOn ⁡ X → J ∈ Top$
58 cmpfi $⊢ J ∈ Top → J ∈ Comp ↔ ∀ x ∈ 𝒫 Clsd ⁡ J ¬ ∅ ∈ fi ⁡ x → ⋂ x ≠ ∅$
59 57 58 syl $⊢ J ∈ TopOn ⁡ X → J ∈ Comp ↔ ∀ x ∈ 𝒫 Clsd ⁡ J ¬ ∅ ∈ fi ⁡ x → ⋂ x ≠ ∅$
60 56 59 sylibrd $⊢ J ∈ TopOn ⁡ X → ∀ f ∈ Fil ⁡ X J fClus f ≠ ∅ → J ∈ Comp$
61 7 60 impbid $⊢ J ∈ TopOn ⁡ X → J ∈ Comp ↔ ∀ f ∈ Fil ⁡ X J fClus f ≠ ∅$