Metamath Proof Explorer

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 = ⋃ J$
	Assertion	ldlfcntref	$⊢ (J \in Ldlf \land U \subseteq J \land X = ⋃ U) \to \exists v \in 𝒫 J (v ≼ ω \land v Ref U)$

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