[proofplan] The argument has two halves. **Uniqueness** is a soft observation: if at least one transitive set containing $x$ exists, then the intersection of all such sets is itself transitive and contains $x$, hence is the smallest such — this gives uniqueness and also characterises $TC(x)$ as the minimum of a family. **Existence** is the real work: we construct an explicit transitive superset of $x$ as the union of the iterated unions $x, \bigcup x, \bigcup \bigcup x, \ldots$. To make this formal in ZFC we cannot simply write down an infinite recursion and hope; we must justify the recursive definition using **attempts** — finite partial functions satisfying the recursive clause — together with the Axiom Schema of Replacement applied to $\omega$. The replacement image gives a set $\{f(n) : n \in \omega\}$, whose union is the desired transitive set. [/proofplan] [step:Establish uniqueness via intersection, conditional on existence] [claim:The intersection of transitive sets containing $x$ is transitive and contains $x$] Let $\mathcal{F}$ be any nonempty family of transitive sets, each containing $x$, and set $I := \bigcap \mathcal{F}$. Then $x \subseteq I$ and $I$ is transitive. [/claim] [proof] Since every $F \in \mathcal{F}$ contains $x$, we have $x \in F$ for every $F \in \mathcal{F}$, so $x \in I$. To see that $I$ is transitive, take $y \in I$ and $z \in y$. For any $F \in \mathcal{F}$, $y \in I \subseteq F$, so $y \in F$, and since $F$ is transitive, $z \in F$. As $F \in \mathcal{F}$ was arbitrary, $z \in \bigcap \mathcal{F} = I$. Hence $y \in I \Rightarrow y \subseteq I$, which is the definition of transitivity of $I$. [/proof] Assuming for the moment that some transitive set containing $x$ exists (this is Step 2), let \begin{align*} \mathcal{F}_x := \{F : F \text{ is transitive and } x \subseteq F\}. \end{align*} By the claim, $TC(x) := \bigcap \mathcal{F}_x$ is a transitive set containing $x$, and by construction it is contained in every member of $\mathcal{F}_x$ — it is therefore the unique smallest such set. [guided] The intersection trick converts uniqueness into a pure bookkeeping exercise. If we know that there is **at least one** transitive set containing $x$, then the family $\mathcal{F}_x$ is nonempty, and we can intersect it. The intersection is automatically transitive (the proof shown above is the standard argument: being transitive is a $\Pi_1$-property preserved under intersection) and still contains $x$ (because each member does). The result is the smallest transitive set containing $x$: any transitive $F \supseteq x$ lies in $\mathcal{F}_x$, hence the intersection is a subset of $F$. So the core problem is **existence**: without producing some transitive superset of $x$ first, the family $\mathcal{F}_x$ might be empty, and the intersection would be the universe (which is not a set). [/guided] [/step] [step:Define the iterated-union candidate informally] Intuitively, define \begin{align*} TC(x) = x \cup \bigcup x \cup \bigcup\bigcup x \cup \bigcup\bigcup\bigcup x \cup \cdots, \end{align*} equivalently, the union of the sequence $f(0) = x$, $f(n+1) = \bigcup f(n)$ for $n \in \omega$. The next steps make this definition rigorous inside ZFC. [/step] [step:Formalise the recursion using attempts] We cannot define $f: \omega \to V$ by the recursive clause \begin{align*} f(0) = x, \qquad f(n+1) = \bigcup f(n) \end{align*} and simply declare $f$ exists, because the class function underlying the recursion is not automatically a legitimate set-theoretic function. We instead work with **attempts**. [definition:Attempt] A set $g$ is an **attempt** if: (i) $g$ is a function; (ii) $\operatorname{dom}(g) \in \omega$ and $\operatorname{dom}(g) \ne \varnothing$; (iii) $g(0) = x$; (iv) for every $n \in \operatorname{dom}(g)$ with $n \ne 0$, we have $g(n) = \bigcup g(n-1)$. [/definition] Note that an attempt with $\operatorname{dom}(g) = k + 1 \in \omega$ is a finite object: a finite set of ordered pairs. [claim:Any two attempts agree on the intersection of their domains] If $g_1, g_2$ are attempts, then $g_1(n) = g_2(n)$ for every $n \in \operatorname{dom}(g_1) \cap \operatorname{dom}(g_2)$. [/claim] [proof] By induction on $n \in \operatorname{dom}(g_1) \cap \operatorname{dom}(g_2)$. For $n = 0$, $g_1(0) = x = g_2(0)$ by clause (iii). For $n + 1 \in \operatorname{dom}(g_1) \cap \operatorname{dom}(g_2)$: by definition of $\operatorname{dom}$ for functions with domain an initial segment of $\omega$, we have $n \in \operatorname{dom}(g_1) \cap \operatorname{dom}(g_2)$ as well, so by induction $g_1(n) = g_2(n)$. By clause (iv), \begin{align*} g_1(n+1) = \bigcup g_1(n) = \bigcup g_2(n) = g_2(n+1). \end{align*} [/proof] [claim:For every $n \in \omega$ there exists an attempt defined at $n$] For every $n \in \omega$ there is an attempt $g$ with $n \in \operatorname{dom}(g)$. [/claim] [proof] By induction on $n$. For $n = 0$, take $g = \{(0, x)\}$; this is a function with domain $1 = \{0\} \in \omega$, $\operatorname{dom}(g) \ne \varnothing$, $g(0) = x$, and clause (iv) is vacuous. So $g$ is an attempt defined at $0$. Assume inductively that there is an attempt $g'$ with $n \in \operatorname{dom}(g')$. Let $k := \operatorname{dom}(g') \in \omega$; so $k \ge n + 1$, and in particular $g'(n)$ is defined. Set \begin{align*} g := g' \cup \{(k, \bigcup g'(k-1))\}. \end{align*} Then $g$ is a function with $\operatorname{dom}(g) = k + 1 \in \omega$, $g$ extends $g'$, and $g$ satisfies clause (iv) at $k$ by construction. So $g$ is an attempt with $k \in \operatorname{dom}(g)$. Since $k \ge n + 1$, $g$ is defined at $n + 1$ if $k \ge n + 1$; but we may iterate this extension procedure finitely many times if needed to ensure $n + 1 \in \operatorname{dom}(g)$, which concludes the inductive step. [/proof] [guided] The technique of **attempts** is the standard way to legitimise recursive definitions over $\omega$ in ZFC. The difficulty is this: the recursive clause "$f(n+1) = \bigcup f(n)$ with $f(0) = x$" is a **schema**, not a function — to apply the Axioms (specifically Replacement) we need a genuine first-order formula $q(n, z)$ that is **functional** (for each $n$ there is exactly one $z$ with $q(n, z)$). **Step (a): Define attempts.** An attempt is a finite function $g: k \to V$ (for some $k \in \omega$) that satisfies the recursive clause **as far as it is defined**. Each attempt is an honest set (a finite set of ordered pairs), so the property "is an attempt" is expressible by a first-order formula over ZFC. **Step (b): Uniqueness of attempts.** The claim that any two attempts agree on the intersection of their domains is proved by induction on that intersection. At stage $0$, both give $x$ by clause (iii). At stage $n+1$, both $g_1(n+1)$ and $g_2(n+1)$ are determined by clause (iv) to equal $\bigcup g_1(n) = \bigcup g_2(n)$ (using the inductive hypothesis). So values at shared indices coincide. **Step (c): Existence of attempts at every $n$.** Also by induction on $n$. The base case $n = 0$ has the obvious attempt $\{(0, x)\}$. The inductive step glues on one more pair $(n+1, \bigcup g'(n))$ — this is a legitimate set-theoretic operation because $\bigcup g'(n)$ exists by the Axiom of Union applied to the set $g'(n)$. **Step (d): Define the function-class.** Once (b) and (c) are in hand, the formula \begin{align*} q(n, z) :\iff (\exists g)\bigl[g \text{ is an attempt} \wedge n \in \operatorname{dom}(g) \wedge g(n) = z\bigr] \end{align*} is functional: (c) gives existence (some attempt defined at $n$ exists, so some $z$ satisfies $q(n, z)$), and (b) gives uniqueness (any two attempts defined at $n$ agree on $n$, so $z$ is determined). Now $q$ is a legitimate first-order formula to which we can apply Replacement. [/guided] [/step] [step:Apply Replacement to produce the range of the recursive function] By the two claims in Step 3, the formula \begin{align*} q(n, z) :\iff (\exists g)\bigl[g \text{ is an attempt} \wedge n \in \operatorname{dom}(g) \wedge g(n) = z\bigr] \end{align*} defines a functional relation on $\omega$: for every $n \in \omega$ there is a unique $z$ (call it $f(n)$) with $q(n, z)$. By the [Axiom Schema of Replacement](/theorems/???) applied to the set $\omega$ and the formula $q$, the image \begin{align*} R := \{f(n) : n \in \omega\} \end{align*} is a set. [/step] [step:Define $TC(x) := \bigcup R$ and verify it is a transitive set containing $x$] Set \begin{align*} T := \bigcup R = \bigcup_{n \in \omega} f(n), \end{align*} which is a set by the Axiom of Union applied to $R$. **$x \subseteq T$:** Since $f(0) = x \in R$, we have $x \subseteq \bigcup R = T$ by definition of union. **$T$ is transitive:** Let $y \in T$. Then $y \in f(n)$ for some $n \in \omega$. We must show $y \subseteq T$. Pick $z \in y$. Then $z \in \bigcup f(n) = f(n+1)$ (using clause (iv) of the definition of $f$). Hence $z \in f(n+1) \in R$, so $z \in \bigcup R = T$. This shows $y \subseteq T$, completing transitivity. [guided] Now that the recursion is legitimised, we can read off the candidate transitive set: $T := \bigcup_{n \in \omega} f(n)$, the union of $x, \bigcup x, \bigcup\bigcup x, \ldots$. **Why does $T$ contain $x$?** Because $f(0) = x$ is one of the sets being unioned — more explicitly, every element of $x$ is an element of $f(0) = x$, hence of $\bigcup R$. **Why is $T$ transitive?** This is where the choice of iteration matters. Suppose $y \in T$. Then $y$ belongs to some level $f(n)$ of the iteration. To show $y \subseteq T$, we must show every element of $y$ is also in $T$. But any element $z \in y$ lies in $\bigcup f(n)$ (that's the definition of union: $z \in y$ and $y \in f(n)$ together imply $z \in \bigcup f(n)$). By clause (iv), $\bigcup f(n) = f(n+1)$. So $z \in f(n+1) \subseteq \bigcup R = T$. This is the key point: taking unions at each stage ensures that the elements-of-elements get absorbed at the next level, and taking the countable union across all levels closes up the structure. [/guided] [/step] [step:Conclude existence and uniqueness of $TC(x)$] By Step 5, $T$ is a transitive set containing $x$. Therefore the family $\mathcal{F}_x$ from Step 1 is nonempty (it contains $T$), and Step 1 gives \begin{align*} TC(x) := \bigcap \mathcal{F}_x \end{align*} as the unique smallest transitive set containing $x$. Moreover $TC(x) \subseteq T$, so the intersection is a legitimate set (bounded by $T$). This completes the proof. $\square$ [guided] We have proven both halves: 1. **Existence** (Steps 2–5): The iterated-union construction, formalised via attempts and Replacement, yields an explicit transitive set $T$ containing $x$. 2. **Uniqueness** (Step 1): Given existence, the family $\mathcal{F}_x$ of transitive supersets of $x$ is nonempty. The intersection of this family is the unique smallest such set. The notation $TC(x)$ is therefore well-defined. As a bonus, the construction gives us two equivalent characterisations: \begin{align*} TC(x) = \bigcap \{F : F \supseteq x \text{ and } F \text{ transitive}\} = \bigcup_{n \in \omega} \underbrace{\bigcup \cdots \bigcup}_{n \text{ times}} x. \end{align*} The first characterisation is abstract and monotone; the second is concrete and computationally useful. In particular, the construction shows that $TC(x) \subseteq T$ — the intersection is bounded above by the explicit iterated-union set, so no foundational issues arise. **Where the axioms enter.** Pairing (to form $\{(n, f(n))\}$ pairs inside attempts), Union (to form $\bigcup f(n)$ at each stage and ultimately $\bigcup R$), Infinity (to obtain $\omega$ itself), and the **Replacement Schema** (the crucial one — to form $R = \{f(n) : n \in \omega\}$) are all needed. The Separation Schema is used implicitly when defining the family $\mathcal{F}_x$. The Axiom of Foundation is **not** used; Transitive Closure is a structural result that holds even in Foundation-free set theory. [/guided] [/step]