Using Replacement to prove transitive closure is a set without recursion

In the course on set theory I'm doing, I'm told that one of the main motivations behind the axiom of replacement is that the Axiom of Infinity asserts the existence of an infinite set, namely $\omega = \{\emptyset, \emptyset^+,\emptyset^{++},\dots\}$ where $a^+ = a \cup \{a\}$, but doesn't in general show the existence of other infinite sets that we'd like.

In particular, I'm told that the transitive closure $TC(x)$ of $x$ is defined as $$TC(x) = \bigcup\{x,\cup x, \cup\cup x,\dots\}$$, and we can use Replacement to be able to say that the set $\{x,\cup x, \cup\cup x,\dots\}$ actually exists.

My question is: assuming the existence of $\omega$ as given above, what function-class can we use with Replacement to prove the existence of the iterated-union set? It would clearly suffice to come up with a formula $\phi$ such that $\phi(n,y)$ asserts that $y$ is the $n^\mathrm{th}$ iteration of the union operation on $x$.

But the only ways I can think of to define such a formula are recursive, and that's no good because the proof I've seen that recursion works uses the transitive closure operation. So there must be either some restricted and easier-to-prove form of recursion, or some non-recursive definition that is just as good.

Edit: here's some legwork to get you started:

$$\mathrm{Fun}(f) = \forall x.(\exists y.(x,y)\in f\wedge(\forall z. (x,z)\in f \Rightarrow z = y))$$ so $\mathrm{Fun}(f)$ means $f$ is a function.

$$\mathrm{Rec}(f) = \forall nxy. ((n,x),y)\in f\Rightarrow ((n = \emptyset\wedge x = y) \vee (\exists m. m^+=n\wedge ((m,\cup x),y)\in f$$ so $\mathrm{Rec}(f)$ means $f$ satisfies a recursion equation for an iterated-union function.

Then $$\phi((n,x),y) = \exists f. \mathrm{Fun}(f) \wedge \mathrm{Rec}(f) \wedge ((n,x),y) \in f$$ is close to what I want, but it's not completely obvious that $\phi$ itself is a function-class. I think I'd need to prove using Foundation that the recursion terminates, possibly by requiring that some things are members of $\omega$ (which I understand exists by using Separation to take the intersection of all sets of the kind described by Infinity). But normal $\epsilon$-induction is still not available, since it depends on $TC$.

-
You can prove the specific case of $\varphi(x,y,n)$ that $y$ is the $n$-th iteration of union from $x$, then $TC(x)$ is something like $\bigcup\{y\mid\exists n\in\omega:\varphi(x,y,n)\}$ –  Asaf Karagila May 27 '12 at 18:31
@AsafKaragila, it's pretty much that specific case that I'm stuck on :) I can't see how to deal with $n$ except recursively. –  Ben Millwood May 27 '12 at 18:33
Well, I meant prove the recursion is valid for this particular case. I'll give it some thought on how this can be bypassed. I think I once knew the answer. –  Asaf Karagila May 27 '12 at 18:41
I can show that there is a formula defining $TC(x)$ which do not go through $\{x,\bigcup x,\bigcup\bigcup x,\ldots\}$ construction. I'm not sure if this is what you're looking for, though. –  Asaf Karagila May 27 '12 at 18:55
That would solve my problem, as long as you didn't assume anything that I normally use $TC$ to prove, but I'd still be interested in an answer to the original question. –  Ben Millwood May 27 '12 at 18:58

You employ the following formula:

$$\exists f(x\in\omega\land f\textrm{ is a function }\land\textrm{dom}(f)=x\cup\{x\}\land f(\varnothing)=\{A\}\\\land(\forall m< x)( f(m\cup\{m\})=\bigcup f(m))\land y=f(x))$$

It's easy to check that this function is unique. To prove that it exists proceed by induction on $n$.

-
Hmm. This might work. My first instinct was "eek, induction, that uses closure" but you're not talking about $\epsilon$-induction, you're talking about induction on the naturals, so we don't need $TC$ but just the set of predecessors of any given natural number. But the set of predecessors is just the number itself, so that's no problem. Give me a bit of time to think about this, and I'll accept it if I don't see any problems with it. –  Ben Millwood May 27 '12 at 21:01
@benmachine: Induction is trivial for $\omega$ since it is by definition the least inductive set that contains $\varnothing$. Hence, if something is a subset of $\omega$ that contains $\varnothing$ and if it contains $x$ then it contains $x\cup\{x\}$ then it is inductive, and thus has $\omega$ as its subset (since $\omega$ is least). –  Apostolos May 27 '12 at 21:09
Okay, I'm convinced I can work out the rest of the details, thank you :) –  Ben Millwood May 27 '12 at 21:16

The proof of recursion with which I’m familiar does not use transitive closure. A version of it can be found on-line in Don Monk’s Advanced Set Theory notes, specifically, as Theorem 4.12 in Chapter 4:

Suppose that $\mathbf G$ is a class function with domain the class of all (ordinary) functions. Then there is a unique class function $\mathbf F$ with domain $\mathrm{On}$ such that for every ordinal $\alpha$ we have $\mathbf F(\alpha)=\mathbf G(\mathbf F\upharpoonright\alpha)$.

This starts on page 19. Roughly speaking the proof is by showing that for each ordinal $\alpha$ there is an approximation $f_\alpha$ to $\mathbf F$ with domain $\alpha$, that these approximations are unique, and that they ‘fit together’ properly, so that one may define $\mathbf F(\alpha)$ as $f_{\alpha+1}(\alpha)$.

-
If we've got as far as ordinals, my instinct is we've probably already proven something as basic as what I want, and it'll take a good bit of reading to work out how, so I'll look at this maybe tomorrow. –  Ben Millwood May 27 '12 at 20:57