Metamath Proof Explorer

Theorem ispcmp

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

Ref Expression
Assertion ispcmp ⊢ J ∈ Paracomp ↔ J ∈ CovHasRef LocFin ⁡ J

Proof

Step Hyp Ref Expression
1 elex ⊢ J ∈ Paracomp → J ∈ V
2 elex ⊢ J ∈ CovHasRef LocFin ⁡ J → J ∈ V
3 id ⊢ j = J → j = J
4 fveq2 ⊢ j = J → LocFin ⁡ j = LocFin ⁡ J
5 crefeq ⊢ LocFin ⁡ j = LocFin ⁡ J → CovHasRef LocFin ⁡ j = CovHasRef LocFin ⁡ J
6 4 5 syl ⊢ j = J → CovHasRef LocFin ⁡ j = CovHasRef LocFin ⁡ J
7 3 6 eleq12d ⊢ j = J → j ∈ CovHasRef LocFin ⁡ j ↔ J ∈ CovHasRef LocFin ⁡ J
8 df-pcmp ⊢ Paracomp = j | j ∈ CovHasRef LocFin ⁡ j
9 7 8 elab2g ⊢ J ∈ V → J ∈ Paracomp ↔ J ∈ CovHasRef LocFin ⁡ J
10 1 2 9 pm5.21nii ⊢ J ∈ Paracomp ↔ J ∈ CovHasRef LocFin ⁡ J