Metamath Proof Explorer


Theorem pcmplfin

Description: Given a paracompact topology J and an open cover U , there exists an open refinement v that is locally finite. (Contributed by Thierry Arnoux, 31-Jan-2020)

Ref Expression
Hypothesis pcmplfin.x X=J
Assertion pcmplfin JParacompUJX=Uv𝒫JvLocFinJvRefU

Proof

Step Hyp Ref Expression
1 pcmplfin.x X=J
2 ssexg UJJParacompUV
3 2 ancoms JParacompUJUV
4 3 3adant3 JParacompUJX=UUV
5 simp2 JParacompUJX=UUJ
6 4 5 elpwd JParacompUJX=UU𝒫J
7 ispcmp JParacompJCovHasRefLocFinJ
8 1 iscref JCovHasRefLocFinJJTopu𝒫JX=uv𝒫JLocFinJvRefu
9 7 8 bitri JParacompJTopu𝒫JX=uv𝒫JLocFinJvRefu
10 9 simprbi JParacompu𝒫JX=uv𝒫JLocFinJvRefu
11 10 3ad2ant1 JParacompUJX=Uu𝒫JX=uv𝒫JLocFinJvRefu
12 simp3 JParacompUJX=UX=U
13 unieq u=Uu=U
14 13 eqeq2d u=UX=uX=U
15 breq2 u=UvRefuvRefU
16 15 rexbidv u=Uv𝒫JLocFinJvRefuv𝒫JLocFinJvRefU
17 14 16 imbi12d u=UX=uv𝒫JLocFinJvRefuX=Uv𝒫JLocFinJvRefU
18 17 rspcv U𝒫Ju𝒫JX=uv𝒫JLocFinJvRefuX=Uv𝒫JLocFinJvRefU
19 6 11 12 18 syl3c JParacompUJX=Uv𝒫JLocFinJvRefU
20 rexin v𝒫JLocFinJvRefUv𝒫JvLocFinJvRefU
21 19 20 sylib JParacompUJX=Uv𝒫JvLocFinJvRefU