# Metamath Proof Explorer

## Theorem ispcmp

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

Ref Expression
Assertion ispcmp ${⊢}{J}\in \mathrm{Paracomp}↔{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)↔{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}↔{J}\in \mathrm{CovHasRef}\mathrm{LocFin}\left({J}\right)\right)$
10 1 2 9 pm5.21nii ${⊢}{J}\in \mathrm{Paracomp}↔{J}\in \mathrm{CovHasRef}\mathrm{LocFin}\left({J}\right)$