Metamath Proof Explorer

Theorem iscmp

Description: The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypothesis iscmp.1 ${⊢}{X}=\bigcup {J}$
Assertion iscmp ${⊢}{J}\in \mathrm{Comp}↔\left({J}\in \mathrm{Top}\wedge \forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left({X}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)\right)$

Proof

Step Hyp Ref Expression
1 iscmp.1 ${⊢}{X}=\bigcup {J}$
2 pweq ${⊢}{x}={J}\to 𝒫{x}=𝒫{J}$
3 unieq ${⊢}{x}={J}\to \bigcup {x}=\bigcup {J}$
4 3 1 syl6eqr ${⊢}{x}={J}\to \bigcup {x}={X}$
5 4 eqeq1d ${⊢}{x}={J}\to \left(\bigcup {x}=\bigcup {y}↔{X}=\bigcup {y}\right)$
6 4 eqeq1d ${⊢}{x}={J}\to \left(\bigcup {x}=\bigcup {z}↔{X}=\bigcup {z}\right)$
7 6 rexbidv ${⊢}{x}={J}\to \left(\exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {x}=\bigcup {z}↔\exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)$
8 5 7 imbi12d ${⊢}{x}={J}\to \left(\left(\bigcup {x}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {x}=\bigcup {z}\right)↔\left({X}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)\right)$
9 2 8 raleqbidv ${⊢}{x}={J}\to \left(\forall {y}\in 𝒫{x}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {x}=\bigcup {z}\right)↔\forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left({X}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)\right)$
10 df-cmp ${⊢}\mathrm{Comp}=\left\{{x}\in \mathrm{Top}|\forall {y}\in 𝒫{x}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {x}=\bigcup {z}\right)\right\}$
11 9 10 elrab2 ${⊢}{J}\in \mathrm{Comp}↔\left({J}\in \mathrm{Top}\wedge \forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left({X}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{X}=\bigcup {z}\right)\right)$