Metamath Proof Explorer

Theorem pcmplfinf

Description: Given a paracompact topology J and an open cover U , there exists an open refinement ran f that is locally finite, using the same index as the original cover U . (Contributed by Thierry Arnoux, 31-Jan-2020)

Ref Expression
Hypothesis pcmplfin.x 
|- X = U. J
Assertion pcmplfinf 
|- ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) -> E. f ( f : U --> J /\ ran f Ref U /\ ran f e. ( LocFin ` J ) ) )

Proof

Step Hyp Ref Expression
1 pcmplfin.x 
 |-  X = U. J
2 simpll2 
 |-  ( ( ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) /\ v e. ~P J ) /\ ( v e. ( LocFin ` J ) /\ v Ref U ) ) -> U C_ J )
3 simpll3 
 |-  ( ( ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) /\ v e. ~P J ) /\ ( v e. ( LocFin ` J ) /\ v Ref U ) ) -> X = U. U )
4 elpwi 
 |-  ( v e. ~P J -> v C_ J )
5 4 ad2antlr 
 |-  ( ( ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) /\ v e. ~P J ) /\ ( v e. ( LocFin ` J ) /\ v Ref U ) ) -> v C_ J )
6 simprr 
 |-  ( ( ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) /\ v e. ~P J ) /\ ( v e. ( LocFin ` J ) /\ v Ref U ) ) -> v Ref U )
7 simprl 
 |-  ( ( ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) /\ v e. ~P J ) /\ ( v e. ( LocFin ` J ) /\ v Ref U ) ) -> v e. ( LocFin ` J ) )
8 1 2 3 5 6 7 locfinref 
 |-  ( ( ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) /\ v e. ~P J ) /\ ( v e. ( LocFin ` J ) /\ v Ref U ) ) -> E. f ( f : U --> J /\ ran f Ref U /\ ran f e. ( LocFin ` J ) ) )
9 1 pcmplfin 
 |-  ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) -> E. v e. ~P J ( v e. ( LocFin ` J ) /\ v Ref U ) )
10 8 9 r19.29a 
 |-  ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) -> E. f ( f : U --> J /\ ran f Ref U /\ ran f e. ( LocFin ` J ) ) )