# 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}\in \mathrm{TopOn}\left({X}\right)\to \left({J}\in \mathrm{Comp}↔\forall {f}\in \mathrm{Fil}\left({X}\right)\phantom{\rule{.4em}{0ex}}{J}\mathrm{fClus}{f}\ne \varnothing \right)$

### Proof

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