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