Infinite Lexicographic Order on Bijections is Well-Order 
Problem. Prove, without using $\mathsf{AC}$ if possible , that if $\alpha$ and $\beta$ are ordinals such that $\alpha$ is countable and $\beta>1$, then $\alpha^\beta$ is countable.

The induction part of the proof is simple, but the limit step requires the following lemma:

Lemma.  Let $A$ be a countable set of countable ordinals. Then $\sup(A)=\bigcup A$ is countable.

My idea of the proof is as follows. For each $\alpha\in A$, let
$$B_\alpha = \{f \mid  f:\omega\to\alpha ~\text{is bijective}\}.$$ Define an infinite lexicographic order $<_\alpha$ on $B_\alpha$ as follows:
$~~~~~~~~~f<_\alpha g~~~~~$    iff    $~~~~~f\ne g$ and for the minimal $n<\omega$
with $f(n)\ne g(n)$, we have $f(n)<g(n)$.
It is straightforward to check that $<_\alpha$ is a linear order; however, it is not so clear if it's a well-order. The same ordering is not a well-order on, for example, Cantor's space, $^\omega 2$, as there exist countable infinite descending chains in it, e.g.,
$$
\langle 1,0,0,0,\ldots\rangle >\langle 0,1,0,0,\ldots\rangle > \langle 0,0,1,0,\ldots\rangle >\ldots.
$$
(Such chains are not allowed in our case, as we only look at bijections.)
Is there a simple way to prove it is a well-order (if it is indeed so)? Or, otherwise, how does one prove the main problem?
 A: This may very well be one of the rare cases where the "direct definition" of ordinal exponentiation is easier to work with.
The more reasonable definition, the inductive one, is given by: $$\alpha^0=1;\ \alpha^{\beta+1}=\alpha^\beta\cdot\alpha;\ \text{for limit ordinals, }\alpha^\beta=\sup\{\alpha^\gamma\mid\gamma<\beta\}.$$
The direct definition is given by $\alpha^\beta$ is the order type of the lexicographic order of $$\{f\colon\beta\to\alpha\mid f^{-1}(0)\text{ is co-finite}\},$$ with the order given by $f<g$ if and only if $\gamma_{f,g}=\max\{\gamma\mid f(\gamma)\neq g(\gamma)\}$ satisfies $f(\gamma_{f,g})<g(\gamma_{f,g})$.
This so-called direct definition is somewhat confusing at first. It is counterintuitive at first. But we can think of this as polynomials, and we first compare them by their degree, then by the coefficients.
Now that we have this definition, we can prove in a slightly more direct way that $\alpha^\beta$ is countable, and indeed has the size $\max\{|\alpha|,|\beta|\}$, as long as both are infinite (if one is finite this may still hold true, but there are more cases to check, so I will leave it to you to try).
The way to do this is to note that these correspond to finite subsets of $\beta\times\alpha$; and $|\beta\times\alpha|$ has the wanted cardinality. So it is enough to show that if $\alpha$ is an infinite ordinal, then the collection of all finite subsets of $\alpha$ has the same cardinality as $\alpha$. But we are not done reducing this, indeed, the easiest way to prove this is to show that the set of all finite sequences, $\alpha^{<\omega}$, has the same cardinality as $\alpha$, as any finite set has an induced linear order which makes it a sequence.
Finally, by utilising the Gödel coding, we can define recursively a sequence of bijections $f_n\colon\alpha\to\alpha^n$. Because those are defined uniformly, we can combine them to define a single function $f\colon\omega\times\alpha\to\alpha^{<\omega}$, and by one last Gödel coding, match $\omega\times\alpha$ with $\alpha$ itself.
Phew! What a journey! Is there a simpler way? Well, kinda. If you know a bit about inner models, then you know that if $\alpha$ and $\beta$ are countable, then there is a set of natural numbers $a$ such that $a$ codes a well-order of length $\max\{\alpha,\beta\}$. Therefore, in $L[a]$ both $\alpha$ and $\beta$ are countable; as a model of $\sf ZFC$, $\alpha^\beta$ is countable there using the lemma you suggest; but since ordinal exponentiation is absolute, this holds in $V$ just as well.
Now, you might wonder, why did I go through all of that trouble? Isn't it enough to just prove the lemma? Well. As Jonathan Schilhan pointed in the comments, it's simply not provable in $\sf ZF$. It is indeed consistent tha $\omega_1$ is a limit of an $\omega$ sequence of countable ordinals. But of course, the key point there, is that you can't really choose the enumerations uniformly.
