Theorem ispcmp

Description: The predicate "is a paracompact topology". (Contributed by Thierry Arnoux, 7-Jan-2020)

	Ref	Expression
Assertion	ispcmp	$$⊢J\in \mathrm{Paracomp}\leftrightarrow J\in \mathrm{CovHasRef}\mathrm{LocFin}\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢J\in \mathrm{Paracomp}\to J\in \mathrm{V}$$
2		elex	$$⊢J\in \mathrm{CovHasRef}\mathrm{LocFin}\left(J\right)\to J\in \mathrm{V}$$
3		id	$$⊢j=J\to j=J$$
4		fveq2	$$⊢j=J\to \mathrm{LocFin}\left(j\right)=\mathrm{LocFin}\left(J\right)$$
5		crefeq	$$⊢\mathrm{LocFin}\left(j\right)=\mathrm{LocFin}\left(J\right)\to \mathrm{CovHasRef}\mathrm{LocFin}\left(j\right)=\mathrm{CovHasRef}\mathrm{LocFin}\left(J\right)$$
6	4 5	syl	$$⊢j=J\to \mathrm{CovHasRef}\mathrm{LocFin}\left(j\right)=\mathrm{CovHasRef}\mathrm{LocFin}\left(J\right)$$
7	3 6	eleq12d	$$⊢j=J\to \left(j\in \mathrm{CovHasRef}\mathrm{LocFin}\left(j\right)\leftrightarrow J\in \mathrm{CovHasRef}\mathrm{LocFin}\left(J\right)\right)$$
8		df-pcmp	$$⊢\mathrm{Paracomp}=\left\{j|j\in \mathrm{CovHasRef}\mathrm{LocFin}\left(j\right)\right\}$$
9	7 8	elab2g	$$⊢J\in \mathrm{V}\to \left(J\in \mathrm{Paracomp}\leftrightarrow J\in \mathrm{CovHasRef}\mathrm{LocFin}\left(J\right)\right)$$
10	1 2 9	pm5.21nii	$$⊢J\in \mathrm{Paracomp}\leftrightarrow J\in \mathrm{CovHasRef}\mathrm{LocFin}\left(J\right)$$