Metamath Proof Explorer


Theorem cmpfiref

Description: Every open cover of a Compact space has a finite refinement. (Contributed by Thierry Arnoux, 1-Feb-2020)

Ref Expression
Hypothesis cmpfiref.x X = J
Assertion cmpfiref J Comp U J X = U v 𝒫 J v Fin v Ref U

Proof

Step Hyp Ref Expression
1 cmpfiref.x X = J
2 cmpcref Comp = CovHasRef Fin
3 id v Fin v Fin
4 1 2 3 crefdf J Comp U J X = U v 𝒫 J v Fin v Ref U