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	⊢ 𝑋 = ∪ 𝐽
Assertion	cmpfiref	⊢ ( ( 𝐽 ∈ Comp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) → ∃ 𝑣 ∈ 𝒫 𝐽 ( 𝑣 ∈ Fin ∧ 𝑣 Ref 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		cmpfiref.x	⊢ 𝑋 = ∪ 𝐽
2		cmpcref	⊢ Comp = CovHasRef Fin
3		id	⊢ ( 𝑣 ∈ Fin → 𝑣 ∈ Fin )
4	1 2 3	crefdf	⊢ ( ( 𝐽 ∈ Comp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) → ∃ 𝑣 ∈ 𝒫 𝐽 ( 𝑣 ∈ Fin ∧ 𝑣 Ref 𝑈 ) )