Theorem ldlfcntref

Description: Every open cover of a Lindelöf space has a countable refinement. (Contributed by Thierry Arnoux, 1-Feb-2020)

	Ref	Expression
Hypothesis	ldlfcntref.x	⊢ 𝑋 = ∪ 𝐽
Assertion	ldlfcntref	⊢ ( ( 𝐽 ∈ Ldlf ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) → ∃ 𝑣 ∈ 𝒫 𝐽 ( 𝑣 ≼ ω ∧ 𝑣 Ref 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		ldlfcntref.x	⊢ 𝑋 = ∪ 𝐽
2		df-ldlf	⊢ Ldlf = CovHasRef { 𝑥 ∣ 𝑥 ≼ ω }
3		vex	⊢ 𝑣 ∈ V
4		breq1	⊢ ( 𝑥 = 𝑣 → ( 𝑥 ≼ ω ↔ 𝑣 ≼ ω ) )
5	3 4	elab	⊢ ( 𝑣 ∈ { 𝑥 ∣ 𝑥 ≼ ω } ↔ 𝑣 ≼ ω )
6	5	biimpi	⊢ ( 𝑣 ∈ { 𝑥 ∣ 𝑥 ≼ ω } → 𝑣 ≼ ω )
7	1 2 6	crefdf	⊢ ( ( 𝐽 ∈ Ldlf ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈 ) → ∃ 𝑣 ∈ 𝒫 𝐽 ( 𝑣 ≼ ω ∧ 𝑣 Ref 𝑈 ) )