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	|- Paracomp = { j | j e. CovHasRef ( LocFin ` j ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpcmp	|- Paracomp
1		vj	|- j
2	1	cv	|- j
3		clocfin	|- LocFin
4	2 3	cfv	|- ( LocFin ` j )
5	4	ccref	|- CovHasRef ( LocFin ` j )
6	2 5	wcel	|- j e. CovHasRef ( LocFin ` j )
7	6 1	cab	|- { j | j e. CovHasRef ( LocFin ` j ) }
8	0 7	wceq	|- Paracomp = { j | j e. CovHasRef ( LocFin ` j ) }