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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpcmp	⊢ Paracomp
1		vj	⊢ 𝑗
2	1	cv	⊢ 𝑗
3		clocfin	⊢ LocFin
4	2 3	cfv	⊢ ( LocFin ‘ 𝑗 )
5	4	ccref	⊢ CovHasRef ( LocFin ‘ 𝑗 )
6	2 5	wcel	⊢ 𝑗 ∈ CovHasRef ( LocFin ‘ 𝑗 )
7	6 1	cab	⊢ { 𝑗 ∣ 𝑗 ∈ CovHasRef ( LocFin ‘ 𝑗 ) }
8	0 7	wceq	⊢ Paracomp = { 𝑗 ∣ 𝑗 ∈ CovHasRef ( LocFin ‘ 𝑗 ) }