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 ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Comp ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐽 fClus 𝑓 ) ≠ ∅ ) )

Proof

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