Metamath Proof Explorer

Theorem ispcmp

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

Ref Expression
Assertion ispcmp ( 𝐽 ∈ Paracomp ↔ 𝐽 ∈ CovHasRef ( LocFin ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐽 ∈ Paracomp → 𝐽 ∈ V )
2 elex ⊢ ( 𝐽 ∈ CovHasRef ( LocFin ‘ 𝐽 ) → 𝐽 ∈ V )
3 id ⊢ ( 𝑗 = 𝐽 → 𝑗 = 𝐽 )
4 fveq2 ⊢ ( 𝑗 = 𝐽 → ( LocFin ‘ 𝑗 ) = ( LocFin ‘ 𝐽 ) )
5 crefeq ⊢ ( ( LocFin ‘ 𝑗 ) = ( LocFin ‘ 𝐽 ) → CovHasRef ( LocFin ‘ 𝑗 ) = CovHasRef ( LocFin ‘ 𝐽 ) )
6 4 5 syl ⊢ ( 𝑗 = 𝐽 → CovHasRef ( LocFin ‘ 𝑗 ) = CovHasRef ( LocFin ‘ 𝐽 ) )
7 3 6 eleq12d ⊢ ( 𝑗 = 𝐽 → ( 𝑗 ∈ CovHasRef ( LocFin ‘ 𝑗 ) ↔ 𝐽 ∈ CovHasRef ( LocFin ‘ 𝐽 ) ) )
8 df-pcmp ⊢ Paracomp = { 𝑗 ∣ 𝑗 ∈ CovHasRef ( LocFin ‘ 𝑗 ) }
9 7 8 elab2g ⊢ ( 𝐽 ∈ V → ( 𝐽 ∈ Paracomp ↔ 𝐽 ∈ CovHasRef ( LocFin ‘ 𝐽 ) ) )
10 1 2 9 pm5.21nii ⊢ ( 𝐽 ∈ Paracomp ↔ 𝐽 ∈ CovHasRef ( LocFin ‘ 𝐽 ) )