Definition df-pcmp 29923

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.)

Assertion

Ref	Expression
df-pcmp	|- Paracomp = { j | j e. CovHasRef ( LocFin ` j ) }

Detailed syntax breakdown of Definition df-pcmp

Step	Hyp	Ref	Expression
1		cpcmp 29922	. 2 class Paracomp
2		vj	. . . . 5 setvar j
3	2	cv 1482	. . . 4 class j
4		clocfin 21307	. . . . . 6 class LocFin
5	3, 4	cfv 5888	. . . . 5 class ( LocFin ` j )
6	5	ccref 29909	. . . 4 class CovHasRef ( LocFin ` j )
7	3, 6	wcel 1990	. . 3 wff j e. CovHasRef ( LocFin ` j )
8	7, 2	cab 2608	. 2 class { j | j e. CovHasRef ( LocFin ` j ) }
9	1, 8	wceq 1483	1 wff Paracomp = { j | j e. CovHasRef ( LocFin ` j ) }

This definition is referenced by:  ispcmp  29924