Regressive function on an ordinal I'm trying to prove the following statement.
Let $0<\overline{\alpha}\leq\alpha$ be two ordinals such that $\omega_{\overline{\alpha}}$ is the cofinality of $\omega_\alpha$. Let $f$ be a mapping of $\omega_\alpha$ into $\omega_\alpha$ such that $f(\xi)<\xi$ for any $0<\xi<\omega_\alpha$. Then there exists $\lambda_0<\omega_\alpha$ such that $f^{-1}(\lambda_0)$ has cardinality $\geq\aleph_{\overline{\alpha}}$.
I think I almost have it: From the preceding exercise, I know that $f$ cannot be divergent, i.e. I know that there exists $\lambda<\omega_\alpha$ such that $f^{-1}([0,\lambda])$ is cofinal and therefore has cardinality $\geq\aleph_{\overline{\alpha}}$. My idea was to define $\lambda_0$ to be the least ordinal $\lambda$ such that $|f^{-1}([0,\lambda])|\geq\aleph_{\overline{\alpha}}$. I would like to conclude that $|f^{-1}(\left[0,\lambda_0\right[)|<\aleph_{\overline{\alpha}}$, but I don't know how. It would be true if the cofinality of $\lambda_0$ was $<\omega_{\overline{\alpha}}$. Is there some way to show this? Am I on the right track?
I have found out that the statement is a (very) special case of a theorem called Fodor's Lemma. However its proof is quite involved and I don't have any experience with the concept "stationary", so I'm not able in a reasonable amount of time to understand it enough to reduce it to an elementary proof of the above statement. But maybe that is an easy task for an experienced set theorist. 
 A: Since the restriction of the function $f$ to
$\omega_{\bar\alpha}$ is still regressive, and the
cofinality of $\omega_{\bar\alpha}$ is itself, we may
immediately reduce to the case $\bar\alpha=\alpha$. This
can also be described as the case that
$\omega_\alpha=\omega_{\bar\alpha}$ is regular. Assume
towards contradiction that every $f^{-1}(\lambda)$ has size
less than $\omega_{\bar\alpha}$. In particular, every
$f^{-1}(\lambda)$ is bounded in $\omega_\alpha$, having
supremum $\beta_\lambda\lt\omega_\alpha$. Since
$\omega_\alpha$ is regular and has uncountable cofinality,
we may find an ordinal $\delta\lt\omega_\alpha$ that is
closed under the function $\lambda\mapsto\beta_\lambda$, in
the sense that $\beta_\lambda\lt\delta$ whenever
$\lambda\lt\delta$ (this is a fun exercise: start with any
ordinal $\delta_0$, let $\delta_{n+1}$ be the supremum +1 of
$\beta_\lambda$ for all $\lambda\lt\delta_n$, and let
$\delta=\text{sup}_n\delta_n$). Now, the point is that
$f(\delta)$ must be less than $\delta$, but it can't be any
particular $\lambda\lt\delta$ since $\delta$ is larger than
$\beta_\lambda$. QED
