[proofplan]
We prove the two assertions simultaneously by induction on the usual rank of the set $x$. The recursive definition of $\check{x}$ only uses $\check{y}$ for elements $y \in x$, and every such $y$ has strictly smaller rank than $x$. Once the earlier check objects are known to be $\mathbb P$-names, $\check{x}$ is a set of ordered pairs whose first coordinates are earlier names and whose second coordinate is $1_{\mathbb P}$. The rank identity then follows by comparing the recursive formula for name rank with the usual recursive formula for set rank.
[/proofplan]
[step:Prove the name property and rank formula by rank induction]
Let $x$ be a set. Assume as the induction hypothesis that for every $y \in x$, the object $\check{y}$ is a $\mathbb P$-name and
\begin{align*}
\operatorname{rank}(\check{y}) = \operatorname{rank}(y).
\end{align*}
This induction hypothesis is available because every element $y \in x$ has smaller usual rank than $x$.
By definition,
\begin{align*}
\check{x} = \{(\check{y}, 1_{\mathbb P}) : y \in x\}.
\end{align*}
For each element $(\check{y},1_{\mathbb P})$ of $\check{x}$, the first coordinate $\check{y}$ is a $\mathbb P$-name by the induction hypothesis, and the second coordinate $1_{\mathbb P}$ belongs to $\mathbb P$ because it is the greatest element of $\mathbb P$. Therefore every element of $\check{x}$ is an ordered pair consisting of a $\mathbb P$-name and a condition in $\mathbb P$. Hence $\check{x}$ is a $\mathbb P$-name.
[guided]
We prove both desired conclusions at the same time, because the definition of a check name refers to earlier check names. Fix a set $x$, and suppose that the theorem has already been proved for every element $y \in x$. This means that for each $y \in x$, the object $\check{y}$ is already known to be a $\mathbb P$-name and its name rank agrees with the usual rank of $y$:
\begin{align*}
\operatorname{rank}(\check{y}) = \operatorname{rank}(y).
\end{align*}
This is legitimate in rank induction because membership lowers rank: if $y \in x$, then $y$ occurs at an earlier stage of the cumulative hierarchy than $x$.
Now use the recursive definition of the canonical check object:
\begin{align*}
\check{x} = \{(\check{y}, 1_{\mathbb P}) : y \in x\}.
\end{align*}
To verify that $\check{x}$ is a $\mathbb P$-name, we must check the defining shape of its elements. Let $(\tau,p)$ be an arbitrary element of $\check{x}$. By the displayed definition, there exists $y \in x$ such that
\begin{align*}
\tau = \check{y}
\end{align*}
and
\begin{align*}
p = 1_{\mathbb P}.
\end{align*}
The induction hypothesis says that $\check{y}$ is a $\mathbb P$-name. Also $1_{\mathbb P} \in \mathbb P$ because $1_{\mathbb P}$ is the greatest element of the partially ordered set $\mathbb P$. Therefore $(\tau,p)$ has first coordinate a $\mathbb P$-name and second coordinate a condition in $\mathbb P$. Since the element of $\check{x}$ was arbitrary, every element of $\check{x}$ has the required form, so $\check{x}$ is a $\mathbb P$-name.
[/guided]
[/step]
[step:Compare the recursive rank formulas]
The first coordinates appearing in elements of $\check{x}$ are precisely the check names $\check{y}$ with $y \in x$. Therefore the recursive definition of name rank gives
\begin{align*}
\operatorname{rank}(\check{x}) = \sup\{\operatorname{rank}(\check{y}) + 1 : y \in x\}.
\end{align*}
Using the induction hypothesis for each $y \in x$, this becomes
\begin{align*}
\operatorname{rank}(\check{x}) = \sup\{\operatorname{rank}(y) + 1 : y \in x\}.
\end{align*}
The right-hand side is exactly the usual recursive definition of the cumulative-hierarchy rank of $x$. Hence
\begin{align*}
\operatorname{rank}(\check{x}) = \operatorname{rank}(x).
\end{align*}
[/step]
[step:Handle the empty set and close the induction]
If $x=\varnothing$, then
\begin{align*}
\check{\varnothing} = \{(\check{y},1_{\mathbb P}) : y \in \varnothing\} = \varnothing.
\end{align*}
The empty set is a $\mathbb P$-name because it has no elements violating the defining condition. Its name rank is
\begin{align*}
\operatorname{rank}(\check{\varnothing}) = \sup \varnothing = 0,
\end{align*}
which agrees with the usual rank
\begin{align*}
\operatorname{rank}(\varnothing) = 0.
\end{align*}
Thus the base case and the induction step both hold. By rank induction, for every set $x$, the canonical check object $\check{x}$ is a $\mathbb P$-name and satisfies
\begin{align*}
\operatorname{rank}(\check{x}) = \operatorname{rank}(x).
\end{align*}
[/step]
