Separability of codomains of Borel functions taking values in completely regular spaces

Question

I am looking for a reference (or a counterexample) to the following statement.

Let $X$ be a separable metric space. Suppose that $Y$ is a completely regular topological space and $f\colon X\to Y$ is a surjective Borel function. Must $Y$ be separable too?

This would be almost automatic if this condition forced metrisability of $Y$, but I see not reason for this to happen.

Answer 1

Theorem 1. (PFA) If $f:X\to Y$ is a Borel map, $X$ is Polish, $Y$ is $T_3$, and the induced maps $f^n:X^n\to Y^n$ are Borel, then $Y$ is hereditarily Lindelof and hereditarily separable.

In addition, $Y$ doesn't have to be metrizable, since the map $f = \text{Id}_\mathbb{R}:(\mathbb{R}, \tau_e)\to (\mathbb{R}, \tau_s)$ where $\tau_e$ is Euclidean topology and $\tau_s$ is Sorgenfrey topology is Borel, but $(\mathbb{R}, \tau_s)$ is not metrizable. Though perhaps not the best example given that the induced map $f^2$ is surely not Borel, since Sorgenfrey plane is not Lindelof.

Let $f:X\to Y$ be Borel where $X$ is a Polish space. In this question Taras Banakh claims its possible to prove that $Y$ has countable tightness using Four Poles theorem:

Theorem 2. (Brzuchowski, Cichoń, Grzegorek, Ryll-Nardzewski) Suppose $I\subseteq \mathcal{P}(X)$ is a proper $\sigma$-ideal of Polish space $X$ with Borel basis. Let $\mathcal{A}\subseteq I$ be a point-finite cover of $X$. Then there is $\mathcal{B}\subseteq\mathcal{A}$ such that $\bigcup \mathcal{B}\not\in\sigma(I\cup \mathcal{B}(X))$, the $\sigma$-field generated by $I\cup \mathcal{B}(X)$.

I'm not sure how to prove this claim myself, but lets assume that its true. That is, lets assume:

Theorem 3. If $f:X\to Y$ is Borel, $X$ is Polish, then $Y$ has countable tightness.

We have the following two theorems, consequences of theorems 7.10 and 8.10 in Todorcevic's Parition problems in topology, for the latter see this article (note that $\text{PFA}$ implies $\text{MA}_{\omega_1}$):

Theorem 4. (PFA) If $X$ is a $T_3$ space, then $X$ is hereditarily Lindelof if and only if it has countable tightness.

Theorem 5. (MA$_{\omega_1}$) If $X$ is a $T_3$ space with countable tightness space that contains a hereditarily Lindelof subspace thats non-separable, then $X^n$ is not Lindelof for some $n$.

Combining theorem 4 and 5 we get:

Theorem 6. (PFA) If $X$ is a $T_3$ hereditarily Lindelof space thats not hereditarily separable, then $X^n$ is not Lindelof for some $n$.

Proof of theorem 1: From theorem 3 it follows that $Y^n$ has countable tightness for each $n$. Theorem 4 then implies $Y^n$ is hereditarily Lindelof, and from theorem 6 it follows that $Y$ needs to be hereditarily separable. $\square$