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

Proof

Step	Hyp	Ref	Expression
1		ldlfcntref.x	$$⊢X=\bigcup J$$
2		df-ldlf	$$⊢\mathrm{Ldlf}=\mathrm{CovHasRef}\left\{x|x\preccurlyeq \mathrm{\omega }\right\}$$
3		vex	$$⊢v\in \mathrm{V}$$
4		breq1	$$⊢x=v\to \left(x\preccurlyeq \mathrm{\omega }\leftrightarrow v\preccurlyeq \mathrm{\omega }\right)$$
5	3 4	elab	$$⊢v\in \left\{x|x\preccurlyeq \mathrm{\omega }\right\}\leftrightarrow v\preccurlyeq \mathrm{\omega }$$
6	5	biimpi	$$⊢v\in \left\{x|x\preccurlyeq \mathrm{\omega }\right\}\to v\preccurlyeq \mathrm{\omega }$$
7	1 2 6	crefdf	$$⊢\left(J\in \mathrm{Ldlf}\wedge U\subseteq J\wedge X=\bigcup U\right)\to \exists v\in 𝒫J\left(v\preccurlyeq \mathrm{\omega }\wedge v\mathrm{Ref}U\right)$$