# Metamath Proof Explorer

## Theorem pibt1

Description: Theorem T000001 of pi-base. A compact topology is also countably compact. See pibp16 and pibp19 for the definitions of the relevant properties. (Contributed by ML, 8-Dec-2020)

Ref Expression
Hypothesis pibt1.19 ${⊢}{C}=\left\{{x}\in \mathrm{Top}|\forall {y}\in 𝒫{x}\phantom{\rule{.4em}{0ex}}\left(\left(\bigcup {x}=\bigcup {y}\wedge {y}\preccurlyeq \mathrm{\omega }\right)\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {x}=\bigcup {z}\right)\right\}$
Assertion pibt1 ${⊢}{J}\in \mathrm{Comp}\to {J}\in {C}$

### Proof

Step Hyp Ref Expression
1 pibt1.19 ${⊢}{C}=\left\{{x}\in \mathrm{Top}|\forall {y}\in 𝒫{x}\phantom{\rule{.4em}{0ex}}\left(\left(\bigcup {x}=\bigcup {y}\wedge {y}\preccurlyeq \mathrm{\omega }\right)\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {x}=\bigcup {z}\right)\right\}$
2 pm3.41 ${⊢}\left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {z}\right)\to \left(\left(\bigcup {J}=\bigcup {y}\wedge {y}\preccurlyeq \mathrm{\omega }\right)\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {z}\right)$
3 2 ralimi ${⊢}\forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {z}\right)\to \forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left(\left(\bigcup {J}=\bigcup {y}\wedge {y}\preccurlyeq \mathrm{\omega }\right)\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {z}\right)$
4 3 anim2i ${⊢}\left({J}\in \mathrm{Top}\wedge \forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {z}\right)\right)\to \left({J}\in \mathrm{Top}\wedge \forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left(\left(\bigcup {J}=\bigcup {y}\wedge {y}\preccurlyeq \mathrm{\omega }\right)\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {z}\right)\right)$
5 eqid ${⊢}\bigcup {J}=\bigcup {J}$
6 5 pibp16 ${⊢}{J}\in \mathrm{Comp}↔\left({J}\in \mathrm{Top}\wedge \forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {z}\right)\right)$
7 5 1 pibp19 ${⊢}{J}\in {C}↔\left({J}\in \mathrm{Top}\wedge \forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left(\left(\bigcup {J}=\bigcup {y}\wedge {y}\preccurlyeq \mathrm{\omega }\right)\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {z}\right)\right)$
8 4 6 7 3imtr4i ${⊢}{J}\in \mathrm{Comp}\to {J}\in {C}$