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 = U. J
Assertion	ldlfcntref	|- ( ( J e. Ldlf /\ U C_ J /\ X = U. U ) -> E. v e. ~P J ( v ~<_ _om /\ v Ref U ) )

Proof

Step	Hyp	Ref	Expression
1		ldlfcntref.x	|- X = U. J
2		df-ldlf	|- Ldlf = CovHasRef { x | x ~<_ _om }
3		vex	|- v e. _V
4		breq1	|- ( x = v -> ( x ~<_ _om <-> v ~<_ _om ) )
5	3 4	elab	|- ( v e. { x | x ~<_ _om } <-> v ~<_ _om )
6	5	biimpi	|- ( v e. { x | x ~<_ _om } -> v ~<_ _om )
7	1 2 6	crefdf	|- ( ( J e. Ldlf /\ U C_ J /\ X = U. U ) -> E. v e. ~P J ( v ~<_ _om /\ v Ref U ) )