# Metamath Proof Explorer

## Theorem sscmp

Description: A subset of a compact topology (i.e. a coarser topology) is compact. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Hypothesis sscmp.1 ${⊢}{X}=\bigcup {K}$
Assertion sscmp ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\to {J}\in \mathrm{Comp}$

### Proof

Step Hyp Ref Expression
1 sscmp.1 ${⊢}{X}=\bigcup {K}$
2 topontop ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {J}\in \mathrm{Top}$
3 2 3ad2ant1 ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\to {J}\in \mathrm{Top}$
4 elpwi ${⊢}{x}\in 𝒫{J}\to {x}\subseteq {J}$
5 simpl2 ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\wedge \left({x}\subseteq {J}\wedge \bigcup {J}=\bigcup {x}\right)\right)\to {K}\in \mathrm{Comp}$
6 simprl ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\wedge \left({x}\subseteq {J}\wedge \bigcup {J}=\bigcup {x}\right)\right)\to {x}\subseteq {J}$
7 simpl3 ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\wedge \left({x}\subseteq {J}\wedge \bigcup {J}=\bigcup {x}\right)\right)\to {J}\subseteq {K}$
8 6 7 sstrd ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\wedge \left({x}\subseteq {J}\wedge \bigcup {J}=\bigcup {x}\right)\right)\to {x}\subseteq {K}$
9 simpl1 ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\wedge \left({x}\subseteq {J}\wedge \bigcup {J}=\bigcup {x}\right)\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
10 toponuni ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}=\bigcup {J}$
11 9 10 syl ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\wedge \left({x}\subseteq {J}\wedge \bigcup {J}=\bigcup {x}\right)\right)\to {X}=\bigcup {J}$
12 simprr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\wedge \left({x}\subseteq {J}\wedge \bigcup {J}=\bigcup {x}\right)\right)\to \bigcup {J}=\bigcup {x}$
13 11 12 eqtrd ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\wedge \left({x}\subseteq {J}\wedge \bigcup {J}=\bigcup {x}\right)\right)\to {X}=\bigcup {x}$
14 1 cmpcov ${⊢}\left({K}\in \mathrm{Comp}\wedge {x}\subseteq {K}\wedge {X}=\bigcup {x}\right)\to \exists {y}\in \left(𝒫{x}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}$
15 5 8 13 14 syl3anc ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\wedge \left({x}\subseteq {J}\wedge \bigcup {J}=\bigcup {x}\right)\right)\to \exists {y}\in \left(𝒫{x}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}$
16 11 eqeq1d ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\wedge \left({x}\subseteq {J}\wedge \bigcup {J}=\bigcup {x}\right)\right)\to \left({X}=\bigcup {y}↔\bigcup {J}=\bigcup {y}\right)$
17 16 rexbidv ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\wedge \left({x}\subseteq {J}\wedge \bigcup {J}=\bigcup {x}\right)\right)\to \left(\exists {y}\in \left(𝒫{x}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {y}↔\exists {y}\in \left(𝒫{x}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {y}\right)$
18 15 17 mpbid ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\wedge \left({x}\subseteq {J}\wedge \bigcup {J}=\bigcup {x}\right)\right)\to \exists {y}\in \left(𝒫{x}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {y}$
19 18 expr ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\wedge {x}\subseteq {J}\right)\to \left(\bigcup {J}=\bigcup {x}\to \exists {y}\in \left(𝒫{x}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {y}\right)$
20 4 19 sylan2 ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\wedge {x}\in 𝒫{J}\right)\to \left(\bigcup {J}=\bigcup {x}\to \exists {y}\in \left(𝒫{x}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {y}\right)$
21 20 ralrimiva ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\to \forall {x}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left(\bigcup {J}=\bigcup {x}\to \exists {y}\in \left(𝒫{x}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {y}\right)$
22 eqid ${⊢}\bigcup {J}=\bigcup {J}$
23 22 iscmp ${⊢}{J}\in \mathrm{Comp}↔\left({J}\in \mathrm{Top}\wedge \forall {x}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left(\bigcup {J}=\bigcup {x}\to \exists {y}\in \left(𝒫{x}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {y}\right)\right)$
24 3 21 23 sylanbrc ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{Comp}\wedge {J}\subseteq {K}\right)\to {J}\in \mathrm{Comp}$