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 ≠ ∅