[proofplan]
For each natural number $n$, we choose a maximal antichain deciding the statement $\check{n} \in \dot{x}$, then keep only the conditions that force membership. The countable chain condition makes each retained antichain countable, so the resulting name is nice. The proof then compares the forcing truth of $\check{n} \in \dot{x}$ and $\check{n} \in \dot{y}$ below an arbitrary condition, using maximality of the deciding antichain and compatibility to rule out the wrong decision. Since both names are forced to be subsets of $\check{\omega}$, agreement on every natural number gives forced equality.
[/proofplan]
[step:Choose countable deciding antichains for each natural number]
Fix $n \in \omega$. Let $D_n \subseteq \mathbb{P}$ be the set of conditions deciding the formula $\check{n} \in \dot{x}$:
\begin{align*}
D_n = \{p \in \mathbb{P} : p \Vdash_{\mathbb{P}} \check{n} \in \dot{x} \text{ or } p \Vdash_{\mathbb{P}} \check{n} \notin \dot{x}\}.
\end{align*}
By the definition of the forcing relation, $D_n$ is dense in $\mathbb{P}$. Choose a maximal antichain $B_n \subseteq D_n$. Since $\mathbb{P}$ satisfies the countable chain condition, every antichain in $\mathbb{P}$ is countable, so $B_n$ is countable.
Define the positive part of $B_n$ by
\begin{align*}
A_n = \{p \in B_n : p \Vdash_{\mathbb{P}} \check{n} \in \dot{x}\}.
\end{align*}
Then $A_n$ is a countable antichain, because $A_n \subseteq B_n$.
[guided]
We need a separate antichain for each integer $n$ because a nice name for a subset of $\omega$ records, independently for each $n$, which conditions force $n$ to belong to the interpreted set.
Fix $n \in \omega$. Define
\begin{align*}
D_n = \{p \in \mathbb{P} : p \Vdash_{\mathbb{P}} \check{n} \in \dot{x} \text{ or } p \Vdash_{\mathbb{P}} \check{n} \notin \dot{x}\}.
\end{align*}
This is the set of conditions that decide the membership question for $n$. The forcing relation has the density property for deciding a formula: below every condition there is a stronger condition deciding that formula. Hence $D_n$ is dense in $\mathbb{P}$.
Choose a maximal antichain $B_n \subseteq D_n$. Since $B_n$ is an antichain in $\mathbb{P}$ and $\mathbb{P}$ satisfies the countable chain condition, $B_n$ is countable. Now split $B_n$ according to which side of the decision it gives, and keep only the membership-forcing conditions:
\begin{align*}
A_n = \{p \in B_n : p \Vdash_{\mathbb{P}} \check{n} \in \dot{x}\}.
\end{align*}
The set $A_n$ is still an antichain because it is a subset of the antichain $B_n$, and it is countable because it is a subset of the [countable set](/page/Countable%20Set) $B_n$. These are exactly the two properties needed for the $n$th slice of a nice name.
[/guided]
[/step]
[step:Define the nice name from the positive antichains]
Define the $\mathbb{P}$-name $\dot{y}$ by
\begin{align*}
\dot{y} = \{(\check{n}, p) : n \in \omega \text{ and } p \in A_n\}.
\end{align*}
For each $n \in \omega$, the set $A_n$ is a countable antichain. Therefore $\dot{y}$ is a nice name for a subset of $\omega$. Also, by construction, every first coordinate appearing in $\dot{y}$ is some canonical name $\check{n}$ with $n \in \omega$, so
\begin{align*}
\Vdash_{\mathbb{P}} \dot{y} \subseteq \check{\omega}.
\end{align*}
[/step]
[step:Show that forcing membership in $\dot{x}$ implies forcing membership in $\dot{y}$]
Let $p \in \mathbb{P}$ and $n \in \omega$, and assume
\begin{align*}
p \Vdash_{\mathbb{P}} \check{n} \in \dot{x}.
\end{align*}
We prove that $p \Vdash_{\mathbb{P}} \check{n} \in \dot{y}$.
Let $q \leq p$ be arbitrary. Since $B_n$ is a maximal antichain, there exists $r \in B_n$ compatible with $q$. Choose $s \in \mathbb{P}$ such that $s \leq q$ and $s \leq r$. Because $s \leq q \leq p$, monotonicity of forcing gives
\begin{align*}
s \Vdash_{\mathbb{P}} \check{n} \in \dot{x}.
\end{align*}
If $r \Vdash_{\mathbb{P}} \check{n} \notin \dot{x}$, then monotonicity also gives
\begin{align*}
s \Vdash_{\mathbb{P}} \check{n} \notin \dot{x},
\end{align*}
contradicting consistency of forcing below a single condition. Hence $r \Vdash_{\mathbb{P}} \check{n} \in \dot{x}$, so $r \in A_n$. Since $(\check{n}, r) \in \dot{y}$ and $s \leq r$, the condition $s$ forces $\check{n} \in \dot{y}$ by the definition of forcing membership for names.
Thus below every $q \leq p$ there is $s \leq q$ such that
\begin{align*}
s \Vdash_{\mathbb{P}} \check{n} \in \dot{y}.
\end{align*}
By the density characterization of forcing, $p \Vdash_{\mathbb{P}} \check{n} \in \dot{y}$.
[/step]
[step:Show that forcing membership in $\dot{y}$ implies forcing membership in $\dot{x}$]
Let $p \in \mathbb{P}$ and $n \in \omega$, and assume
\begin{align*}
p \Vdash_{\mathbb{P}} \check{n} \in \dot{y}.
\end{align*}
We prove that $p \Vdash_{\mathbb{P}} \check{n} \in \dot{x}$.
Suppose not. Then there exists $q \leq p$ such that
\begin{align*}
q \Vdash_{\mathbb{P}} \check{n} \notin \dot{x}.
\end{align*}
Since $p \Vdash_{\mathbb{P}} \check{n} \in \dot{y}$, monotonicity gives
\begin{align*}
q \Vdash_{\mathbb{P}} \check{n} \in \dot{y}.
\end{align*}
By the definition of forcing membership in the name $\dot{y}$, there are a condition $s \leq q$ and a condition $r \in A_n$ such that $s \leq r$. Since $r \in A_n$, the definition of $A_n$ gives
\begin{align*}
r \Vdash_{\mathbb{P}} \check{n} \in \dot{x}.
\end{align*}
By monotonicity, $s \leq r$ implies
\begin{align*}
s \Vdash_{\mathbb{P}} \check{n} \in \dot{x}.
\end{align*}
Also $s \leq q$, so
\begin{align*}
s \Vdash_{\mathbb{P}} \check{n} \notin \dot{x}.
\end{align*}
This contradiction shows that no such $q$ exists. Therefore
\begin{align*}
p \Vdash_{\mathbb{P}} \check{n} \in \dot{x}.
\end{align*}
[guided]
The point of this direction is that the name $\dot{y}$ contains only pairs coming from conditions that already force membership in $\dot{x}$. We show that this prevents $\dot{y}$ from adding any new integer.
Let $p \in \mathbb{P}$ and $n \in \omega$, and assume
\begin{align*}
p \Vdash_{\mathbb{P}} \check{n} \in \dot{y}.
\end{align*}
We want to prove
\begin{align*}
p \Vdash_{\mathbb{P}} \check{n} \in \dot{x}.
\end{align*}
Assume toward a contradiction that this fails. By the negation clause for forcing, there is a stronger condition $q \leq p$ such that
\begin{align*}
q \Vdash_{\mathbb{P}} \check{n} \notin \dot{x}.
\end{align*}
Since forcing is monotone and $q \leq p$, the assumption on $p$ also gives
\begin{align*}
q \Vdash_{\mathbb{P}} \check{n} \in \dot{y}.
\end{align*}
Now unpack what it means for $q$ to force membership in $\dot{y}$. The name $\dot{y}$ has pairs only of the form $(\check{m}, r)$ with $m \in \omega$ and $r \in A_m$. For $q$ to force $\check{n} \in \dot{y}$, there must be a stronger condition $s \leq q$ witnessing membership through some pair with first coordinate $\check{n}$. Thus there is $r \in A_n$ such that $s \leq r$.
Because $r \in A_n$, the construction of $A_n$ says exactly that
\begin{align*}
r \Vdash_{\mathbb{P}} \check{n} \in \dot{x}.
\end{align*}
Since $s \leq r$, monotonicity gives
\begin{align*}
s \Vdash_{\mathbb{P}} \check{n} \in \dot{x}.
\end{align*}
But $s \leq q$, and $q$ was chosen to force non-membership, so monotonicity also gives
\begin{align*}
s \Vdash_{\mathbb{P}} \check{n} \notin \dot{x}.
\end{align*}
A single condition cannot force both a statement and its negation. This contradiction proves that the assumed counterexample $q$ cannot exist. Hence
\begin{align*}
p \Vdash_{\mathbb{P}} \check{n} \in \dot{x}.
\end{align*}
[/guided]
[/step]
[step:Conclude equality of the two names]
The previous two steps show that for every $p \in \mathbb{P}$ and every $n \in \omega$,
\begin{align*}
p \Vdash_{\mathbb{P}} \check{n} \in \dot{x}
\end{align*}
if and only if
\begin{align*}
p \Vdash_{\mathbb{P}} \check{n} \in \dot{y}.
\end{align*}
Moreover,
\begin{align*}
\Vdash_{\mathbb{P}} \dot{x} \subseteq \check{\omega}
\end{align*}
by hypothesis, and
\begin{align*}
\Vdash_{\mathbb{P}} \dot{y} \subseteq \check{\omega}
\end{align*}
by construction. Therefore every condition forces that $\dot{x}$ and $\dot{y}$ have the same elements of $\check{\omega}$ and no elements outside $\check{\omega}$. By extensionality,
\begin{align*}
\Vdash_{\mathbb{P}} \dot{x} = \dot{y}.
\end{align*}
This proves the nice name lemma for subsets of $\omega$.
[/step]
