Is there a detailed and/or rigorous proof that the transitive closure of a set exists? I provide my own answer below, but I welcome any other proofs.
In Existence of the transitive closure for sets, How to prove in ZF that every set has a transitive closure, and Using Replacement to prove transitive closure is a set without recursion users attempt to prove the existence of the transitive closure of a set in ZF. The proofs which involve the axiom of regularity use facts which typically assume the existence of transitive closures. The proofs which do not use the axiom of regularity attempt to use the recursion theorem or something similar, but they omit nontrivial steps. The versions of the recursion theorem I most often see are not strong enough to prove the existence of the transitive closure, so I think further explanation would be needed.
Best Answer
I assume the fact that $\omega$ exists and satisfies induction, which follows from the axiom of infinity and specification. Note that I do not use the axiom of regularity which means that this proof is valid in ZF without regularity. I avoid using the recursion theorem here, although a logical form of the recursion theorem could be used to give an alternative proof.
Let $s$ be a fixed set. First, we wish to prove the existence of the set $\{s,\cup s,\cup\cup s,\ldots\}$. We define some notational shortcuts.
$$\text{Func}(f)=\forall p(p\in f\Rightarrow \exists x\exists y[p=(x,y)])\land\forall x\forall y\forall z([(x,y)\in f\wedge(x,z)\in f]\Rightarrow y=z)$$
This simply says that $f$ is a function on some domain.
$$\text{Rec}(f)=\forall n\forall y((n,y)\in f\Rightarrow$$
$$[(n=0\wedge y=s)\vee(\exists m\exists z[m\in\omega\wedge n=m+1\wedge y=\cup z\wedge(m,z)\in f])])$$
This says that $f(0)=s$ and $f(m+1)=\cup f(m)$ whenever $m+1$ is in the domain of $f$. Note also that, if $f$ is a function, then $\text{Rec}(f)$ implies that the domain of $f$ is a subset of $\omega$. Finally, we have
$$\varphi(n,y)=\exists f(\text{Func}(f)\wedge\text{Rec}(f)\wedge(n,y)\in f)$$ We will use $\varphi$ with the axiom schema of replacement to obtain the set $\{s,\cup s,\cup\cup s,\ldots\}$. First, we must show that $\varphi$ is a functional relation (more formally, we want to prove $\forall n\in\omega\exists!y\varphi(n,y)$).
We proceed by induction. We see immediately that $\varphi(0,s)$ is true since $f=\{(0,s)\}$ is a function which satisfies $\text{Rec}(f)$. Suppose $\varphi(0,y)$. Then there exists a function $g$ such that $\text{Rec}(g)$ and $g(0)=y$. Because, $\text{Rec}(g)$ is true and there does not exist $m\in\omega$ such that $0=m+1$, we must have $y=s$.
Now let $n\in\omega$ and suppose there exists a unique $y$ such that $\varphi(n,y)$. Suppose that $\varphi(n+1,v)$ is true. Then there exists a function $g$ such that $\text{Rec}(g)$ and $(n+1,v)\in g$. Because $\text{Rec}(g)$ and $n+1\neq 0$, there exists $u$ such that $v=\cup u$ and $(n,u)\in g$ so that $\varphi(n,u)$. By the inductive hypothesis, this implies $u=y$ and hence $v=\cup y$. So, $v$ is unique, if it exists. Since $\varphi(n,y)$, there exists a function $f$ such that $\text{Rec}(f)$ and $(n,y)\in f$. Note that $n+1$ may or may not be in the domain of $f$. Let $f'=f\cup\{(n+1,\cup y)\}$. I claim $f'$ is a function such that $\text{Rec}(f)$. If $(n+1,w)\in f$ then $\varphi(n+1,w)$ which implies $w=\cup y$ by uniqueness. It then follows that $f'$ is a function since $f$ is. Now suppose $(n',y')\in f'$. If $n'\neq n+1$, then $(n',y')\in f$ so that either $n'=0$ and $y'=s$ or there exists $m'$ and $z'$ such that $n'=m'+1$, $y'=\cup z'$, and $(m',z')\in f\subset f'$. If $n'=n+1$, then this still holds since $y'=\cup y$ and $(n,y)\in f'$. Thus, $\text{Rec}(f)$ is true and hence $\varphi(n+1,\cup y)$ is true.
So, by induction, for every $n\in\omega$, there exists a unique $y$ such that $\varphi(n,y)$. Then, by the axiom schema of replacement, there exists a set $S$ such that $y\in S$ if and only if there exists $n\in\omega$ such that $\varphi(n,y)$ (i.e. $S=\{s,\cup s,\cup\cup s,\ldots\}$). Let $T=\cup S$. I claim that $T$ is the transitive closure of $s$.
First note that $s\in S$ since $\varphi(0,s)$, which implies $s\subset T$. Let $x_1\in x_2\in T$. Then there exists $y\in S$ such that $x_2\in y$. So, by the construction of $S$, there exists $n\in\omega$ such that $\varphi(n,y)$. Then, by the same reasoning as before, $\varphi(n+1,\cup y)$ so that $\cup y\in S$. However, since $x_1\in x_2\in y$, we know $x_1\in\cup y$ and hence $x_1\in T$. So, $T$ is transitive.
Suppose $T'$ is a transitive set containing $s$ and assume $T\not\subset T'$. Then $$A=\{n\in\omega:\exists x\exists y(x\in y\wedge\varphi(n,y)\wedge x\notin T')\}$$ is nonempty and therefore has a minimum element, $n_{min}$, by the well-ordering principle. Let $x$ and $y$ be such that $x\in y$, $\varphi(n_{min},y)$, and $x\notin T'$. Since $\varphi(n_{min},y)$, there exists a function $f$ such that $\text{Rec}(f)$ and $(n_{min},y)\in f$. If $n_{min}=0$ then $y=s$ and hence $s\not\subset T'$, a contradiction. If $n_{min}\neq 0$, then there exists $z$ and $m\in\omega$ such that $n_{min}=m+1$, $y=\cup z$, and $(m,z)\in f$ so that $\varphi(m,z)$. Since $x\in y=\cup z$, there exists $w\in z$ such that $x\in w$. Note that $w\notin T'$ since otherwise, we would have $x\in T'$ by transitivity. Thus, we see $w\in z$, $\varphi(m,z)$, and $w\notin T'$. So $m\in A$ and $m<n_{min}$, a contradiction. Hence, by way of contradiction, $T\subset T'$. This proves that $T$ is the transitive closure of $s$. The uniqueness of $T$ follows from the fact the minimality of the transitive closure under the subset relation.