[proofplan]
Use the axiom of infinity to obtain one inductive set $I$. Then use separation inside $I$ to form the subset of elements that belong to every inductive subset of $I$; call this subset $\omega$. We prove that $\omega$ is itself inductive by testing the defining universal property against arbitrary inductive subsets of $I$. Finally, if $A$ is any inductive set, then $A \cap I$ is an inductive subset of $I$, so the definition of $\omega$ forces every element of $\omega$ to lie in $A$.
[/proofplan]
[step:Choose an ambient inductive set]
By the axiom of infinity, there exists a set $I$ such that
\begin{align*}
\varnothing \in I
\quad \text{and} \quad
\forall x \, \bigl(x \in I \implies x \cup \{x\} \in I\bigr).
\end{align*}
Fix such a set $I$ for the rest of the proof. For any set $B$, say that $B$ is inductive if
\begin{align*}
\varnothing \in B
\quad \text{and} \quad
\forall x \, \bigl(x \in B \implies x \cup \{x\} \in B\bigr).
\end{align*}
[/step]
[step:Separate the elements common to all inductive subsets of $I$]
Apply separation to the set $I$ with the formula
\begin{align*}
\Phi(a) \iff \forall J \, \bigl((J \subset I \text{ and } J \text{ is inductive}) \implies a \in J\bigr).
\end{align*}
This gives a set
\begin{align*}
\omega := \{a \in I : \forall J \, ((J \subset I \text{ and } J \text{ is inductive}) \implies a \in J)\}.
\end{align*}
Thus $\omega \subset I$, and an element $a$ lies in $\omega$ exactly when $a \in I$ and $a$ belongs to every inductive subset of $I$.
[guided]
The purpose of working inside $I$ is that separation forms subsets of an already existing set. The phrase “the set of all elements that belong to every inductive set” is too large to form directly, because it quantifies over the whole universe. Instead, we first use infinity to obtain one inductive set $I$, and then define $\omega$ as a subset of $I$.
Precisely, separation applied to $I$ and to the formula
\begin{align*}
\Phi(a) \iff \forall J \, \bigl((J \subset I \text{ and } J \text{ is inductive}) \implies a \in J\bigr)
\end{align*}
produces the set
\begin{align*}
\omega := \{a \in I : \forall J \, ((J \subset I \text{ and } J \text{ is inductive}) \implies a \in J)\}.
\end{align*}
Therefore $\omega$ is a set, $\omega \subset I$, and its defining property is: an element $a \in I$ belongs to $\omega$ exactly when every inductive subset of $I$ contains $a$.
[/guided]
[/step]
[step:Show that $\varnothing$ belongs to $\omega$]
Since $I$ is inductive, $\varnothing \in I$. Let $J$ be any set such that $J \subset I$ and $J$ is inductive. By the definition of inductive, $\varnothing \in J$. Hence $\varnothing$ belongs to every inductive subset of $I$. By the definition of $\omega$, we conclude that
\begin{align*}
\varnothing \in \omega.
\end{align*}
[/step]
[step:Show that $\omega$ is closed under successors]
Let $x \in \omega$. Since $\omega \subset I$, we have $x \in I$. Because $I$ is inductive,
\begin{align*}
x \cup \{x\} \in I.
\end{align*}
Now let $J$ be any set such that $J \subset I$ and $J$ is inductive. Since $x \in \omega$, the defining property of $\omega$ gives $x \in J$. Since $J$ is inductive, it follows that
\begin{align*}
x \cup \{x\} \in J.
\end{align*}
Thus $x \cup \{x\}$ lies in every inductive subset of $I$, and it also lies in $I$. By the definition of $\omega$,
\begin{align*}
x \cup \{x\} \in \omega.
\end{align*}
Therefore
\begin{align*}
\forall x \, \bigl(x \in \omega \implies x \cup \{x\} \in \omega\bigr).
\end{align*}
[guided]
Fix $x \in \omega$. To prove $x \cup \{x\} \in \omega$, we must verify both parts of the definition of membership in $\omega$: first, the successor $x \cup \{x\}$ must belong to $I$; second, it must belong to every inductive subset of $I$.
The first condition follows from the inductiveness of $I$. Since $x \in \omega$ and $\omega \subset I$, we have $x \in I$. Hence
\begin{align*}
x \cup \{x\} \in I.
\end{align*}
For the universal condition, let $J$ be an arbitrary inductive subset of $I$. Because $x \in \omega$, the defining property of $\omega$ says that $x$ belongs to every inductive subset of $I$, so $x \in J$. Since $J$ is inductive, membership of $x$ in $J$ implies membership of its successor:
\begin{align*}
x \cup \{x\} \in J.
\end{align*}
The set $J$ was arbitrary among inductive subsets of $I$, so $x \cup \{x\}$ belongs to every such $J$. Together with $x \cup \{x\} \in I$, this is exactly the definition of
\begin{align*}
x \cup \{x\} \in \omega.
\end{align*}
[/guided]
[/step]
[step:Compare $\omega$ with an arbitrary inductive set]
Let $A$ be an arbitrary inductive set. By separation applied to $I$, the intersection
\begin{align*}
K := I \cap A
\end{align*}
is a set and satisfies $K \subset I$.
We show that $K$ is inductive. Since $\varnothing \in I$ and $\varnothing \in A$, we have
\begin{align*}
\varnothing \in K.
\end{align*}
If $x \in K$, then $x \in I$ and $x \in A$. Since both $I$ and $A$ are inductive,
\begin{align*}
x \cup \{x\} \in I
\quad \text{and} \quad
x \cup \{x\} \in A.
\end{align*}
Hence $x \cup \{x\} \in K$. Thus $K$ is an inductive subset of $I$.
Now let $a \in \omega$. Since $K$ is an inductive subset of $I$, the defining property of $\omega$ gives $a \in K$. Therefore $a \in A$. Since $a \in \omega$ was arbitrary,
\begin{align*}
\omega \subset A.
\end{align*}
[guided]
Now we prove the minimality property. Let $A$ be any inductive set. The set $A$ need not be a subset of $I$, so we cannot directly use it in the definition of $\omega$, which only quantifies over inductive subsets of $I$. The way to bring $A$ into the definition is to intersect it with $I$.
By separation inside $I$, define
\begin{align*}
K := I \cap A.
\end{align*}
Then $K \subset I$. We verify that $K$ is inductive. Since $I$ is inductive and $A$ is inductive,
\begin{align*}
\varnothing \in I
\quad \text{and} \quad
\varnothing \in A,
\end{align*}
so $\varnothing \in K$. Next, suppose $x \in K$. Then $x \in I$ and $x \in A$. Applying the successor closure of $I$ and of $A$ gives
\begin{align*}
x \cup \{x\} \in I
\quad \text{and} \quad
x \cup \{x\} \in A.
\end{align*}
Therefore $x \cup \{x\} \in I \cap A = K$. Hence $K$ is an inductive subset of $I$.
Now take any $a \in \omega$. Since $\omega$ was defined to consist of the elements of $I$ that lie in every inductive subset of $I$, and since $K$ is an inductive subset of $I$, we get $a \in K$. In particular, $a \in A$. Because this holds for every $a \in \omega$, we have
\begin{align*}
\omega \subset A.
\end{align*}
[/guided]
[/step]
[step:Conclude the existence of the minimal inductive set]
We have constructed a set $\omega$ such that
\begin{align*}
\varnothing \in \omega,
\end{align*}
\begin{align*}
\forall x \, \bigl(x \in \omega \implies x \cup \{x\} \in \omega\bigr),
\end{align*}
and, for every inductive set $A$,
\begin{align*}
\omega \subset A.
\end{align*}
Thus $\omega$ satisfies the required properties.
[/step]