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 = U. J
Assertion cmpfiref 
|- ( ( J e. Comp /\ U C_ J /\ X = U. U ) -> E. v e. ~P J ( v e. Fin /\ v Ref U ) )

Proof

Step Hyp Ref Expression
1 cmpfiref.x 
 |-  X = U. J
2 cmpcref 
 |-  Comp = CovHasRef Fin
3 id 
 |-  ( v e. Fin -> v e. Fin )
4 1 2 3 crefdf 
 |-  ( ( J e. Comp /\ U C_ J /\ X = U. U ) -> E. v e. ~P J ( v e. Fin /\ v Ref U ) )