# Metamath Proof Explorer

## Theorem cmpcov

Description: An open cover of a compact topology has a finite subcover. (Contributed by Jeff Hankins, 29-Jun-2009)

Ref Expression
Hypothesis iscmp.1 ${⊢}{X}=\bigcup {J}$
Assertion cmpcov ${⊢}\left({J}\in \mathrm{Comp}\wedge {S}\subseteq {J}\wedge {X}=\bigcup {S}\right)\to \exists {s}\in \left(𝒫{S}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {s}$

### Proof

Step Hyp Ref Expression
1 iscmp.1 ${⊢}{X}=\bigcup {J}$
2 unieq ${⊢}{r}={S}\to \bigcup {r}=\bigcup {S}$
3 2 eqeq2d ${⊢}{r}={S}\to \left({X}=\bigcup {r}↔{X}=\bigcup {S}\right)$
4 pweq ${⊢}{r}={S}\to 𝒫{r}=𝒫{S}$
5 4 ineq1d ${⊢}{r}={S}\to 𝒫{r}\cap \mathrm{Fin}=𝒫{S}\cap \mathrm{Fin}$
6 5 rexeqdv ${⊢}{r}={S}\to \left(\exists {s}\in \left(𝒫{r}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {s}↔\exists {s}\in \left(𝒫{S}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {s}\right)$
7 3 6 imbi12d ${⊢}{r}={S}\to \left(\left({X}=\bigcup {r}\to \exists {s}\in \left(𝒫{r}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {s}\right)↔\left({X}=\bigcup {S}\to \exists {s}\in \left(𝒫{S}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {s}\right)\right)$
8 1 iscmp ${⊢}{J}\in \mathrm{Comp}↔\left({J}\in \mathrm{Top}\wedge \forall {r}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left({X}=\bigcup {r}\to \exists {s}\in \left(𝒫{r}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {s}\right)\right)$
9 8 simprbi ${⊢}{J}\in \mathrm{Comp}\to \forall {r}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left({X}=\bigcup {r}\to \exists {s}\in \left(𝒫{r}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {s}\right)$
10 9 adantr ${⊢}\left({J}\in \mathrm{Comp}\wedge {S}\subseteq {J}\right)\to \forall {r}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left({X}=\bigcup {r}\to \exists {s}\in \left(𝒫{r}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {s}\right)$
11 ssexg ${⊢}\left({S}\subseteq {J}\wedge {J}\in \mathrm{Comp}\right)\to {S}\in \mathrm{V}$
12 11 ancoms ${⊢}\left({J}\in \mathrm{Comp}\wedge {S}\subseteq {J}\right)\to {S}\in \mathrm{V}$
13 simpr ${⊢}\left({J}\in \mathrm{Comp}\wedge {S}\subseteq {J}\right)\to {S}\subseteq {J}$
14 12 13 elpwd ${⊢}\left({J}\in \mathrm{Comp}\wedge {S}\subseteq {J}\right)\to {S}\in 𝒫{J}$
15 7 10 14 rspcdva ${⊢}\left({J}\in \mathrm{Comp}\wedge {S}\subseteq {J}\right)\to \left({X}=\bigcup {S}\to \exists {s}\in \left(𝒫{S}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {s}\right)$
16 15 3impia ${⊢}\left({J}\in \mathrm{Comp}\wedge {S}\subseteq {J}\wedge {X}=\bigcup {S}\right)\to \exists {s}\in \left(𝒫{S}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {s}$