What is the formal way of constructing limit ordinals larger than $\omega$ (for example, $\omega + \omega$)? I am trying to figure out how one constructs limit ordinals that are larger than $\omega$. In my book, the Axiom of Infinity (to create a set $X$ that contains the natural numbers) followed by the Separation / Comprehension Schema (with the formula $\varphi(n):= n \text{ is a natural number }$) is used to carve $\omega$ from $X$...the author calls this set $\omega$ the least limit ordinal.
I have read that, starting at $\omega$, you would (informally) apply the successor function an infinite number of times. This yields $S(\omega) = \omega \cup \{\omega\}=\omega+1$, $S(S(\omega))= \omega+1\  \cup \ \{\omega+1 \}=\omega+2$, etc.
Is the process as straightforward as defining the following set:
$T = \{ \omega + n\,|\, n\in \omega\}$
And then taking the union $\bigcup T$? (Knowing that such a union yields the supremum \ least upper bound of the set $T$)

If the above construction is the standard construction, then my once concern is, "From which set am I selecting the $\omega + n$ elements?".
The strategy I am familiar with is invoking the Separation / Comprehension schema to carve away subsets. But I think that must not be what I am doing above...because that would presuppose the existence of $\omega + \omega$ (or at least some ordinal that is larger than $\omega + \omega$).
So what is the method that I am actually using to create $T$ in the first place?
 A: You're right that Separation doesn't do the job. Instead, this is exactly what the axiom (scheme) of Replacement does!
We first write down a formula $\varphi(x,y)$ in two free variables which intuitively says "$y=\omega+x$." We then prove that for each $x\in\omega$ there is a unique $y$ such that $\varphi(x,y)$ holds - at which point Replacement lets us form $$\{y:\exists x\in\omega(\varphi(x,y))\}=\{\omega+n: n\in\omega\}.$$ Applying the Union axiom then finishes the job.
Meanwhile, to see that Separation won't suffice, it's a good exercise to check that $V_{\omega+\omega}\models\mathsf{ZC}$ (= the $\mathsf{ZFC}$ axioms except Replacement). Since $\omega+\omega\not\in V_{\omega+\omega}$, this means that $\mathsf{ZC}$ alone can't prove that $\omega+\omega$ exists. (See here for further discussion of this point.)
A: For each $n$ you construct by successively applying the successor function ordinals $\omega+n$ for each $n \in \omega$. Then the axiom of replacement tells us that
$$\{\omega+n \mid n \in \omega\}$$ is a set too and we can take its union (which order-theoretically is the sup) of that set to form $\omega+\omega$.
In that case it’s also enough to have one uncountable ordinal (which exists by power set and AC, or use Hartog’s trick) and note that all the above countable ordinals must be elements (and initial segments) of it, and apply separation. The way one goes about it depends on your text’s setup, I suppose.
