Reference request: $C_p(X)$ is Lindelöf if $X$ is metrizable and separable. I read that the following is a classic result:

Let $X$ be a separable metrizable space. Then $C_p(X)$ is Lindelöf.

Here $C_p(X)$ is the space of continuous real-valued functions on $X$ with the topology of pointwise convergence (i.e., the topology $C_p(X)$ inherits as a subspace of $\mathbb R^X$ with the product topology).
I tried to look for this result in some books and Google but I found no reference to it.
Where can I find a proof?
 A: I'm not exactly sure where you can find the proof all written up, but here's one.
I'll begin with a couple definitions.


*

*A network for a topological space $X$ is a collection $\mathcal N $ of (not necessarily open) subsets of $X$ such that for every open $U \subseteq X$ and every $x \in U$ there is an $N \in \mathcal N $ with $x \in N \subseteq U$.

*The network weight of a topological space $X$ is defined $$\operatorname{nw} (X) = \min \{ | \mathcal N  | : \mathcal N  \subseteq \mathcal{P} (X)\text{ is a network for }X \} + \aleph_0.$$


Fact 0. For any space $X$, $\operatorname{nw}(X) \leq \operatorname{w}(X)$, where $$\operatorname{w}(X) = \min \{ | \mathcal{B} | : \mathcal{B} \subseteq \mathcal{P}(X)\text{ is a base for }X \} + \aleph_0$$ is the weight of $X$.
Fact 1. If $\operatorname{nw}(X) = \aleph_0$, then $X$ is Lindelöf.


*

*proof. Let $\mathcal N $ be a network for $X$ of minimal cardinality. Suppose that $\mathcal{U}$ is an open cover of $X$. Let $\mathcal N ^\prime = \{ N \in \mathcal N  : ( \exists U \in \mathcal{U} ) ( N \subseteq U ) \}$. For each $N \in \mathcal N ^\prime$ pick some $U_N \in \mathcal{U}$ with $N \subseteq U_N$. Consider now $\mathcal{U}^\prime = \{ U_N : N \in \mathcal N ^\prime \} \subseteq \mathcal{U}$. Since $\mathcal N $ (and hence $\mathcal N ^\prime$) is countable, then so is $\mathcal{U}^\prime$. Given $x \in X$ there is a $U \in \mathcal{U}$ with $x \in U$, and so there is an $N \in \mathcal N $ with $x \in N \subseteq U$.  Then $N \in \mathcal N ^\prime$, and it follows that $x \in N \subseteq U_N \in \mathcal{U}^\prime$. Therefore $\mathcal{U}^\prime$ is a countable subcover of $\mathcal{U}$.


Fact 2. For any space $X$, $\operatorname{nw}(C_p(X)) 
\leq \operatorname{nw}(X)$. (In fact, we have equality, but this is not needed.)


*

*proof. Fix a network $\mathcal N $ of $X$ of minimal cardinality. For $N_1 , \ldots , N_k \in \mathcal N $ and open intervals $I_1 , \ldots , I_n$ in $\mathbb R$ with rational endpoints define $$W_{N_1,I_1;\ldots;N_k,I_k} = \{ f \in C_p(X) : ( \forall i \leq k ) ( f[N_i] \subseteq I_i ) \}.$$ Define $\mathcal M $ to be the collection of all such $W_{N_1,I_1;\ldots;N_k,I_k}$. It follows that $| \mathcal M  | = \operatorname{nw}(X)$. To show that $\mathcal M $ is a network for $C_p(X)$ it suffices to show that for every basic open set $$U = U_{x_1,J_1;\ldots;x_\ell,J_\ell} = \{ f \in C_p(X) : ( \forall i \leq \ell ) ( f(x_i) \in J_i ) \}$$ ($x_1 , \ldots , x_\ell \in X$ and $J_1 , \ldots , J_\ell$ open intervals in $\mathbb R$ with rational endpoints) and each $f \in U$ there is a $W = W_{N_1,I_1;\ldots;N_k,I_k} \in \mathcal M$ such that $f \in W \subseteq U$.
Since $f$ is continuous, for each $i \leq \ell$ we have that $f^{-1} [ J_i ]$ is open in $X$ and $x_i \in f^{-1} [ J_i ]$, so there is an $N_i \in \mathcal N $ with $x_i \in N_i \subseteq f^{-1} [ J_i ]$. Setting $k = \ell$ and $I_i = J_i$ for $i \leq k$ it is easy to see that $f \in W = W_{N_1,I_1;\ldots;N_k,I_k} \subseteq U$. Therefore $\mathcal M $ is a network for $C_p(X)$, and so $\operatorname{nw}(C_p(X)) \leq | \mathcal M  | = \operatorname{nw}(X)$.

If $X$ is a separable metrizable space, then $X$ is second-countable, and so using Facts 0 and 2 $\operatorname{nw}(C_p(X)) \leq \operatorname{nw}(X) \leq \operatorname{w}(X) = \aleph_0$. By Fact 1 it follows that $C_p(X)$ is Lindelöf.
