# Metamath Proof Explorer

## Theorem locfincmp

Description: For a compact space, the locally finite covers are precisely the finite covers. Sadly, this property does not properly characterize all compact spaces. (Contributed by Jeff Hankins, 22-Jan-2010) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses locfincmp.1 ${⊢}{X}=\bigcup {J}$
locfincmp.2 ${⊢}{Y}=\bigcup {C}$
Assertion locfincmp ${⊢}{J}\in \mathrm{Comp}\to \left({C}\in \mathrm{LocFin}\left({J}\right)↔\left({C}\in \mathrm{Fin}\wedge {X}={Y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 locfincmp.1 ${⊢}{X}=\bigcup {J}$
2 locfincmp.2 ${⊢}{Y}=\bigcup {C}$
3 1 locfinnei ${⊢}\left({C}\in \mathrm{LocFin}\left({J}\right)\wedge {x}\in {X}\right)\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {o}\wedge \left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\in \mathrm{Fin}\right)$
4 3 ralrimiva ${⊢}{C}\in \mathrm{LocFin}\left({J}\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {o}\wedge \left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\in \mathrm{Fin}\right)$
5 1 cmpcov2 ${⊢}\left({J}\in \mathrm{Comp}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {o}\wedge \left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\in \mathrm{Fin}\right)\right)\to \exists {c}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({X}=\bigcup {c}\wedge \forall {o}\in {c}\phantom{\rule{.4em}{0ex}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\in \mathrm{Fin}\right)$
6 4 5 sylan2 ${⊢}\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\to \exists {c}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({X}=\bigcup {c}\wedge \forall {o}\in {c}\phantom{\rule{.4em}{0ex}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\in \mathrm{Fin}\right)$
7 elfpw ${⊢}{c}\in \left(𝒫{J}\cap \mathrm{Fin}\right)↔\left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)$
8 simplrr ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\to {c}\in \mathrm{Fin}$
9 eldifsn ${⊢}{x}\in \left({C}\setminus \left\{\varnothing \right\}\right)↔\left({x}\in {C}\wedge {x}\ne \varnothing \right)$
10 ineq1 ${⊢}{s}={x}\to {s}\cap {o}={x}\cap {o}$
11 10 neeq1d ${⊢}{s}={x}\to \left({s}\cap {o}\ne \varnothing ↔{x}\cap {o}\ne \varnothing \right)$
12 simplrl ${⊢}\left(\left(\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\wedge \left({x}\in {C}\wedge {y}\in {x}\right)\right)\wedge \left({o}\in {c}\wedge {y}\in {o}\right)\right)\to {x}\in {C}$
13 simplrr ${⊢}\left(\left(\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\wedge \left({x}\in {C}\wedge {y}\in {x}\right)\right)\wedge \left({o}\in {c}\wedge {y}\in {o}\right)\right)\to {y}\in {x}$
14 simprr ${⊢}\left(\left(\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\wedge \left({x}\in {C}\wedge {y}\in {x}\right)\right)\wedge \left({o}\in {c}\wedge {y}\in {o}\right)\right)\to {y}\in {o}$
15 inelcm ${⊢}\left({y}\in {x}\wedge {y}\in {o}\right)\to {x}\cap {o}\ne \varnothing$
16 13 14 15 syl2anc ${⊢}\left(\left(\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\wedge \left({x}\in {C}\wedge {y}\in {x}\right)\right)\wedge \left({o}\in {c}\wedge {y}\in {o}\right)\right)\to {x}\cap {o}\ne \varnothing$
17 11 12 16 elrabd ${⊢}\left(\left(\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\wedge \left({x}\in {C}\wedge {y}\in {x}\right)\right)\wedge \left({o}\in {c}\wedge {y}\in {o}\right)\right)\to {x}\in \left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}$
18 elunii ${⊢}\left({y}\in {x}\wedge {x}\in {C}\right)\to {y}\in \bigcup {C}$
19 18 2 eleqtrrdi ${⊢}\left({y}\in {x}\wedge {x}\in {C}\right)\to {y}\in {Y}$
20 19 ancoms ${⊢}\left({x}\in {C}\wedge {y}\in {x}\right)\to {y}\in {Y}$
21 20 adantl ${⊢}\left(\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\wedge \left({x}\in {C}\wedge {y}\in {x}\right)\right)\to {y}\in {Y}$
22 1 2 locfinbas ${⊢}{C}\in \mathrm{LocFin}\left({J}\right)\to {X}={Y}$
23 22 adantl ${⊢}\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\to {X}={Y}$
24 23 ad3antrrr ${⊢}\left(\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\wedge \left({x}\in {C}\wedge {y}\in {x}\right)\right)\to {X}={Y}$
25 21 24 eleqtrrd ${⊢}\left(\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\wedge \left({x}\in {C}\wedge {y}\in {x}\right)\right)\to {y}\in {X}$
26 simplr ${⊢}\left(\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\wedge \left({x}\in {C}\wedge {y}\in {x}\right)\right)\to {X}=\bigcup {c}$
27 25 26 eleqtrd ${⊢}\left(\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\wedge \left({x}\in {C}\wedge {y}\in {x}\right)\right)\to {y}\in \bigcup {c}$
28 eluni2 ${⊢}{y}\in \bigcup {c}↔\exists {o}\in {c}\phantom{\rule{.4em}{0ex}}{y}\in {o}$
29 27 28 sylib ${⊢}\left(\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\wedge \left({x}\in {C}\wedge {y}\in {x}\right)\right)\to \exists {o}\in {c}\phantom{\rule{.4em}{0ex}}{y}\in {o}$
30 17 29 reximddv ${⊢}\left(\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\wedge \left({x}\in {C}\wedge {y}\in {x}\right)\right)\to \exists {o}\in {c}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}$
31 30 expr ${⊢}\left(\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\wedge {x}\in {C}\right)\to \left({y}\in {x}\to \exists {o}\in {c}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\right)$
32 31 exlimdv ${⊢}\left(\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\wedge {x}\in {C}\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {x}\to \exists {o}\in {c}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\right)$
33 n0 ${⊢}{x}\ne \varnothing ↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {x}$
34 eliun ${⊢}{x}\in \bigcup _{{o}\in {c}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}↔\exists {o}\in {c}\phantom{\rule{.4em}{0ex}}{x}\in \left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}$
35 32 33 34 3imtr4g ${⊢}\left(\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\wedge {x}\in {C}\right)\to \left({x}\ne \varnothing \to {x}\in \bigcup _{{o}\in {c}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\right)$
36 35 expimpd ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\to \left(\left({x}\in {C}\wedge {x}\ne \varnothing \right)\to {x}\in \bigcup _{{o}\in {c}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\right)$
37 9 36 syl5bi ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\to \left({x}\in \left({C}\setminus \left\{\varnothing \right\}\right)\to {x}\in \bigcup _{{o}\in {c}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\right)$
38 37 ssrdv ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\to {C}\setminus \left\{\varnothing \right\}\subseteq \bigcup _{{o}\in {c}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}$
39 iunfi ${⊢}\left({c}\in \mathrm{Fin}\wedge \forall {o}\in {c}\phantom{\rule{.4em}{0ex}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\in \mathrm{Fin}\right)\to \bigcup _{{o}\in {c}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\in \mathrm{Fin}$
40 39 ex ${⊢}{c}\in \mathrm{Fin}\to \left(\forall {o}\in {c}\phantom{\rule{.4em}{0ex}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\in \mathrm{Fin}\to \bigcup _{{o}\in {c}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\in \mathrm{Fin}\right)$
41 ssfi ${⊢}\left(\bigcup _{{o}\in {c}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\in \mathrm{Fin}\wedge {C}\setminus \left\{\varnothing \right\}\subseteq \bigcup _{{o}\in {c}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\right)\to {C}\setminus \left\{\varnothing \right\}\in \mathrm{Fin}$
42 41 expcom ${⊢}{C}\setminus \left\{\varnothing \right\}\subseteq \bigcup _{{o}\in {c}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\to \left(\bigcup _{{o}\in {c}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\in \mathrm{Fin}\to {C}\setminus \left\{\varnothing \right\}\in \mathrm{Fin}\right)$
43 40 42 sylan9 ${⊢}\left({c}\in \mathrm{Fin}\wedge {C}\setminus \left\{\varnothing \right\}\subseteq \bigcup _{{o}\in {c}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\right)\to \left(\forall {o}\in {c}\phantom{\rule{.4em}{0ex}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\in \mathrm{Fin}\to {C}\setminus \left\{\varnothing \right\}\in \mathrm{Fin}\right)$
44 8 38 43 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\wedge {X}=\bigcup {c}\right)\to \left(\forall {o}\in {c}\phantom{\rule{.4em}{0ex}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\in \mathrm{Fin}\to {C}\setminus \left\{\varnothing \right\}\in \mathrm{Fin}\right)$
45 44 expimpd ${⊢}\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge \left({c}\subseteq {J}\wedge {c}\in \mathrm{Fin}\right)\right)\to \left(\left({X}=\bigcup {c}\wedge \forall {o}\in {c}\phantom{\rule{.4em}{0ex}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\in \mathrm{Fin}\right)\to {C}\setminus \left\{\varnothing \right\}\in \mathrm{Fin}\right)$
46 7 45 sylan2b ${⊢}\left(\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\wedge {c}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\right)\to \left(\left({X}=\bigcup {c}\wedge \forall {o}\in {c}\phantom{\rule{.4em}{0ex}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\in \mathrm{Fin}\right)\to {C}\setminus \left\{\varnothing \right\}\in \mathrm{Fin}\right)$
47 46 rexlimdva ${⊢}\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\to \left(\exists {c}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\left({X}=\bigcup {c}\wedge \forall {o}\in {c}\phantom{\rule{.4em}{0ex}}\left\{{s}\in {C}|{s}\cap {o}\ne \varnothing \right\}\in \mathrm{Fin}\right)\to {C}\setminus \left\{\varnothing \right\}\in \mathrm{Fin}\right)$
48 6 47 mpd ${⊢}\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\to {C}\setminus \left\{\varnothing \right\}\in \mathrm{Fin}$
49 snfi ${⊢}\left\{\varnothing \right\}\in \mathrm{Fin}$
50 unfi ${⊢}\left({C}\setminus \left\{\varnothing \right\}\in \mathrm{Fin}\wedge \left\{\varnothing \right\}\in \mathrm{Fin}\right)\to \left({C}\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}\in \mathrm{Fin}$
51 48 49 50 sylancl ${⊢}\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\to \left({C}\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}\in \mathrm{Fin}$
52 ssun1 ${⊢}{C}\subseteq {C}\cup \left\{\varnothing \right\}$
53 undif1 ${⊢}\left({C}\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}={C}\cup \left\{\varnothing \right\}$
54 52 53 sseqtrri ${⊢}{C}\subseteq \left({C}\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}$
55 ssfi ${⊢}\left(\left({C}\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}\in \mathrm{Fin}\wedge {C}\subseteq \left({C}\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}\right)\to {C}\in \mathrm{Fin}$
56 51 54 55 sylancl ${⊢}\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\to {C}\in \mathrm{Fin}$
57 56 23 jca ${⊢}\left({J}\in \mathrm{Comp}\wedge {C}\in \mathrm{LocFin}\left({J}\right)\right)\to \left({C}\in \mathrm{Fin}\wedge {X}={Y}\right)$
58 57 ex ${⊢}{J}\in \mathrm{Comp}\to \left({C}\in \mathrm{LocFin}\left({J}\right)\to \left({C}\in \mathrm{Fin}\wedge {X}={Y}\right)\right)$
59 cmptop ${⊢}{J}\in \mathrm{Comp}\to {J}\in \mathrm{Top}$
60 1 2 finlocfin ${⊢}\left({J}\in \mathrm{Top}\wedge {C}\in \mathrm{Fin}\wedge {X}={Y}\right)\to {C}\in \mathrm{LocFin}\left({J}\right)$
61 60 3expib ${⊢}{J}\in \mathrm{Top}\to \left(\left({C}\in \mathrm{Fin}\wedge {X}={Y}\right)\to {C}\in \mathrm{LocFin}\left({J}\right)\right)$
62 59 61 syl ${⊢}{J}\in \mathrm{Comp}\to \left(\left({C}\in \mathrm{Fin}\wedge {X}={Y}\right)\to {C}\in \mathrm{LocFin}\left({J}\right)\right)$
63 58 62 impbid ${⊢}{J}\in \mathrm{Comp}\to \left({C}\in \mathrm{LocFin}\left({J}\right)↔\left({C}\in \mathrm{Fin}\wedge {X}={Y}\right)\right)$