Definition df-pcmp 32831

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 = {𝑗 ∣ 𝑗 ∈ CovHasRef(LocFin‘𝑗)}

Detailed syntax breakdown of Definition df-pcmp

Step	Hyp	Ref	Expression
1		cpcmp 32830	. 2 class Paracomp
2		vj	. . . . 5 setvar 𝑗
3	2	cv 1540	. . . 4 class 𝑗
4		clocfin 23007	. . . . . 6 class LocFin
5	3, 4	cfv 6543	. . . . 5 class (LocFin‘𝑗)
6	5	ccref 32817	. . . 4 class CovHasRef(LocFin‘𝑗)
7	3, 6	wcel 2106	. . 3 wff 𝑗 ∈ CovHasRef(LocFin‘𝑗)
8	7, 2	cab 2709	. 2 class {𝑗 ∣ 𝑗 ∈ CovHasRef(LocFin‘𝑗)}
9	1, 8	wceq 1541	1 wff Paracomp = {𝑗 ∣ 𝑗 ∈ CovHasRef(LocFin‘𝑗)}

This definition is referenced by:  ispcmp  32832