A club in $\omega_1$ induced by a bijection I'm trying to prove that if $f:\omega_1\to\omega_1\times\omega_1$ is a bijection, then the set $X_f=\{\alpha\in\omega_1:f[\alpha]=\alpha\times\alpha\}$ is a club in $\omega_1.$
So I think I see that it's closed under suprema. If $\{\alpha_\beta\}$ is a sequence in $X_f$, not cofinal in $\omega_1$, then $$f[\sup\alpha_\beta]=\bigcup f[\alpha_\beta]=\bigcup(\alpha_\beta\times\alpha_\beta)=\sup(\alpha_\beta)\times\sup(\alpha_\beta).$$
I'm not sure if it's formally OK, but at least I think I see it intuitively. 
I also see that $X_f$ is non-empty because $f[0]=\varnothing=0\times0.$ But have no idea why this has to be unbounded. Could you help me?
 A: Consider $\alpha=\alpha_0<\omega_1$. If $\alpha_0\in X_f$, we are done. Otherwise, let 
$$\beta_0=\max \{\alpha_0,\sup\pi_1[f[\alpha_0]], \sup\pi_2[f[\alpha_0]]\}$$
where $\pi_1$ and $\pi_2$ are the projections. We clearly have $\alpha_0\leq\beta_0<\omega_1$ and $f[\alpha_0]\subseteq \beta_0\times\beta_0$. Now let 
$$\alpha_1=\max\{\beta_0, \sup f^{-1}[\beta_0\times\beta_0]\}$$
We clearly have $\beta_0\leq\alpha_1$, but we also have $\alpha_0<\alpha_1$. This is obvious if $\alpha_0<\beta_0$. If $\alpha_0=\beta_0$, since $\alpha_0\notin X_f$, there is some element $x\in\beta_0\times\beta_0\setminus f[\alpha_0]$. Since $f$ is bijective this implies $f^{-1}(x)\geq\alpha_0$ and so $\sup f^{-1}[\beta_0\times\beta_0]>\alpha_0$.
Now, if $\alpha_1\in X_f$, we are done. Otherwise we can continue this process and construct sequences $\langle \alpha_n;n<\omega\rangle$ and $\langle \beta_n;n<\omega\rangle$. Note that we have ensured that $\alpha_0\leq\beta_0\leq\alpha_1\leq\beta_1\leq\dots$.
Let $\alpha_\omega=\sup_n\alpha_n=\sup_n\beta_n$. I claim that $\alpha_\omega\in X_f$. 
This follows immediately since we have arranged to have $f[\alpha_n]\subseteq \beta_n\times\beta_n \subseteq f[\alpha_{n+1}]$, which gives the desired conclusion
$f[\alpha_\omega]=\alpha_\omega\times\alpha_\omega$.
