# Metamath Proof Explorer

## Theorem fincmp

Description: A finite topology is compact. (Contributed by FL, 22-Dec-2008)

Ref Expression
Assertion fincmp ${⊢}{J}\in \left(\mathrm{Top}\cap \mathrm{Fin}\right)\to {J}\in \mathrm{Comp}$

### Proof

Step Hyp Ref Expression
1 elinel1 ${⊢}{J}\in \left(\mathrm{Top}\cap \mathrm{Fin}\right)\to {J}\in \mathrm{Top}$
2 elinel2 ${⊢}{J}\in \left(\mathrm{Top}\cap \mathrm{Fin}\right)\to {J}\in \mathrm{Fin}$
3 vex ${⊢}{y}\in \mathrm{V}$
4 3 pwid ${⊢}{y}\in 𝒫{y}$
5 velpw ${⊢}{y}\in 𝒫{J}↔{y}\subseteq {J}$
6 ssfi ${⊢}\left({J}\in \mathrm{Fin}\wedge {y}\subseteq {J}\right)\to {y}\in \mathrm{Fin}$
7 5 6 sylan2b ${⊢}\left({J}\in \mathrm{Fin}\wedge {y}\in 𝒫{J}\right)\to {y}\in \mathrm{Fin}$
8 elin ${⊢}{y}\in \left(𝒫{y}\cap \mathrm{Fin}\right)↔\left({y}\in 𝒫{y}\wedge {y}\in \mathrm{Fin}\right)$
9 unieq ${⊢}{z}={y}\to \bigcup {z}=\bigcup {y}$
10 9 rspceeqv ${⊢}\left({y}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\wedge \bigcup {J}=\bigcup {y}\right)\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {z}$
11 10 ex ${⊢}{y}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\to \left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {z}\right)$
12 8 11 sylbir ${⊢}\left({y}\in 𝒫{y}\wedge {y}\in \mathrm{Fin}\right)\to \left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {z}\right)$
13 4 7 12 sylancr ${⊢}\left({J}\in \mathrm{Fin}\wedge {y}\in 𝒫{J}\right)\to \left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\bigcup {J}=\bigcup {z}\right)$
14 13 ralrimiva ${⊢}{J}\in \mathrm{Fin}\to \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)$
15 2 14 syl ${⊢}{J}\in \left(\mathrm{Top}\cap \mathrm{Fin}\right)\to \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)$
16 eqid ${⊢}\bigcup {J}=\bigcup {J}$
17 16 iscmp ${⊢}{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)$
18 1 15 17 sylanbrc ${⊢}{J}\in \left(\mathrm{Top}\cap \mathrm{Fin}\right)\to {J}\in \mathrm{Comp}$