Metamath Proof Explorer

Theorem ispcmp

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

Ref Expression
Assertion ispcmp 
|- ( J e. Paracomp <-> J e. CovHasRef ( LocFin ` J ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( J e. Paracomp -> J e. _V )
2 elex 
 |-  ( J e. CovHasRef ( LocFin ` J ) -> J e. _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 e. CovHasRef ( LocFin ` j ) <-> J e. CovHasRef ( LocFin ` J ) ) )
8 df-pcmp 
 |-  Paracomp = { j | j e. CovHasRef ( LocFin ` j ) }
9 7 8 elab2g 
 |-  ( J e. _V -> ( J e. Paracomp <-> J e. CovHasRef ( LocFin ` J ) ) )
10 1 2 9 pm5.21nii 
 |-  ( J e. Paracomp <-> J e. CovHasRef ( LocFin ` J ) )