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	$$setvarj$$
2	1	cv	$$setvarj$$
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	$$wffj\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\}$$