Beth number - justify existence of Beth omega I read through the answers to previous questions regarding Beth numbers and  was unable to find the answer to my question, so I hope this isn't a duplicate.
I am studying the definition of Beth numbers, specifically:
$\beth_0:=\aleph_0$
$\beth_{\alpha+1}:=2^{\beth_\alpha}$
$\beth_\lambda:=\displaystyle\sup_{\alpha<\lambda}\beth_\alpha$ for limit ordinals $\lambda$
How is the third line of the definition justified? How do we know that the power set operation can be applied an infinite number of times? Is there a way to show rigorously that $\beth_\omega$ for example, exists? Would I need a version of the Axiom of Choice?
 A: To expand on my comment, recall the following version of the Recursion Theorem reads, where $\phi$ is a formula in the language of set theory:

Suppose that $\forall x \exists! y\phi(s,y)$, and define $G(s)$ to be the unique $y$ such that $\phi(s,y)$ (note the use Replacement). Then we can define a formula $\psi$ for which the following are provable.
  
  
*
  
*$\forall x \exists! y \psi(x,y)$, so $\psi$ defines a functions $F$, where $F(x)$ is the $y$ such that $\psi(x,y)$.
  
*$\forall\xi\in ON [F(\xi)=G(F\upharpoonright\xi)]$.

where $F\upharpoonright\xi$ means $F$ restricted to $\xi$. For a proof and some comments on the statement of the theorem, see Kunen's Foundations of Mathematics, page 45. 
To apply this theorem, we need only specify $G$. We let:
$$
G(s)=
\begin{cases}
\aleph_0 & \text{if $s=0$}\\
2^{s(\eta)} & \text{if $s$ is a function with dom$(s)=\eta+1$ a successor ordinal}\\
\sup_{\alpha<\lambda} s(\alpha) & \text{if $s$ is a function with dom$(s)=\lambda$ a limit ordinal}\\
0 & \text{otherwise}
\end{cases}
$$
You can now apply (2) in the theorem to this $G$ to see that $F$ is the desired $\beth$ function.
