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=\bigcup J$$
Assertion	cmpfiref	$$⊢\left(J\in \mathrm{Comp}\wedge U\subseteq J\wedge X=\bigcup U\right)\to \exists v\in 𝒫J\left(v\in \mathrm{Fin}\wedge v\mathrm{Ref}U\right)$$

Proof

Step	Hyp	Ref	Expression
1		cmpfiref.x	$$⊢X=\bigcup J$$
2		cmpcref	$$⊢\mathrm{Comp}=\mathrm{CovHasRef}\mathrm{Fin}$$
3		id	$$⊢v\in \mathrm{Fin}\to v\in \mathrm{Fin}$$
4	1 2 3	crefdf	$$⊢\left(J\in \mathrm{Comp}\wedge U\subseteq J\wedge X=\bigcup U\right)\to \exists v\in 𝒫J\left(v\in \mathrm{Fin}\wedge v\mathrm{Ref}U\right)$$