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 = J
Assertion pcmplfinf J Paracomp U J X = U f f : U J ran f Ref U ran f LocFin J

Proof

Step Hyp Ref Expression
1 pcmplfin.x X = J
2 simpll2 J Paracomp U J X = U v 𝒫 J v LocFin J v Ref U U J
3 simpll3 J Paracomp U J X = U v 𝒫 J v LocFin J v Ref U X = U
4 elpwi v 𝒫 J v J
5 4 ad2antlr J Paracomp U J X = U v 𝒫 J v LocFin J v Ref U v J
6 simprr J Paracomp U J X = U v 𝒫 J v LocFin J v Ref U v Ref U
7 simprl J Paracomp U J X = U v 𝒫 J v LocFin J v Ref U v LocFin J
8 1 2 3 5 6 7 locfinref J Paracomp U J X = U v 𝒫 J v LocFin J v Ref U f f : U J ran f Ref U ran f LocFin J
9 1 pcmplfin J Paracomp U J X = U v 𝒫 J v LocFin J v Ref U
10 8 9 r19.29a J Paracomp U J X = U f f : U J ran f Ref U ran f LocFin J