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$.
Best Answer
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:
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)$.