# Metamath Proof Explorer

## Definition df-pcmp

Description: Definition of a paracompact topology. A topology is said to be paracompact iff every open cover has an open refinement that is locally finite. The definition 6 of BourbakiTop1 p. I.69. also requires the topology to be Hausdorff, but this is dropped here. (Contributed by Thierry Arnoux, 7-Jan-2020)

Ref Expression
Assertion df-pcmp ${⊢}\mathrm{Paracomp}=\left\{{j}|{j}\in \mathrm{CovHasRef}\mathrm{LocFin}\left({j}\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cpcmp ${class}\mathrm{Paracomp}$
1 vj ${setvar}{j}$
2 1 cv ${setvar}{j}$
3 clocfin ${class}\mathrm{LocFin}$
4 2 3 cfv ${class}\mathrm{LocFin}\left({j}\right)$
5 4 ccref ${class}\mathrm{CovHasRef}\mathrm{LocFin}\left({j}\right)$
6 2 5 wcel ${wff}{j}\in \mathrm{CovHasRef}\mathrm{LocFin}\left({j}\right)$
7 6 1 cab ${class}\left\{{j}|{j}\in \mathrm{CovHasRef}\mathrm{LocFin}\left({j}\right)\right\}$
8 0 7 wceq ${wff}\mathrm{Paracomp}=\left\{{j}|{j}\in \mathrm{CovHasRef}\mathrm{LocFin}\left({j}\right)\right\}$