Why $V$ and $V^B$ have the same ordinals In chapter 14 of Jech's Set Theory, he writes the following (for the definition of $V^B$, see my question here):

The next lemma states that $V$ and $V^B$ "have the same ordinals."
Lemma 14.23. For every $x\in V^B$,
$$||x\text{ is an ordinal}||=\sum_{\alpha\in\text{Ord}}||x=\check \alpha||.$$
Proof.  Since "$x$ is an ordinal" is $\Delta_0$, we have, by Lemma 14.21,
$$\sum_{\alpha\in\text{Ord}}||x=\check \alpha||\leq ||x\text{ is an ordinal}||.$$
On the other hand, let $||x\text{ is an ordinal}||=u$. We first observe that if $\gamma$ is an ordinal, then
$$||\text{$x$ is an ordinal and $x\in\check \gamma$}||\leq \sum_{\alpha\in\gamma}||x=\check \alpha||.$$
Also, for every $\alpha$ we have
$$u\leq ||x\in \check \alpha||+||x=\check \alpha||+||\check \alpha\in x||.$$
However, there is only a set of $\alpha$'s such that $||\check \alpha\in x||\neq 0$ (because $||\check \alpha\in x||=\sum_{t\in\text{dom}(x)}(||\check \alpha=t||\cdot x(t))$). Hence there is $\gamma$ such that $u\leq ||x\subseteq \check\gamma||$ and we have $u\leq \sum_{\alpha\leq \gamma} ||x=\check \alpha||$.

For definitions of $\check \alpha$ and Lemma 14.21 (as a side note, is there a way to do enumerate or align environments in MathJax?):

Definition 14.20 (By $\in$-Induction).
(i) $\check \varnothing=\varnothing\quad$ (ii) for every $x\in V$, let $\check x\in V^B$ be the function whose domain is the set $\{\check y:y\in x\}$, and for all $y\in x$, $\check x(\check y)=1$.
Lemma 14.21. If $\varphi(x_1,\dots,x_n)$is a $\Delta_0$ formula, then
$$\text{$\varphi(x_1,\dots,x_n)$ if and only if $||\varphi(\check x_1,\dots,\check x_n)||=1.$}$$

I have a few questions about this proof:

*

*How does this establish that "$V$ and $V^B$ have the same ordinals?" I'm assuming this is  supposed to imply that $||\text{$x$ is an ordinal}||=1$ if and only if there is some ordinal $\alpha$ (in $V$) such that $||x=\check \alpha||=1$. Assuming I am understanding correctly, I don't understand why this sum condition is enough to conclude that if $x$ is an ordinal, then such an $\alpha$ must exist. Why isn't it possible for there to be some sequence of $\alpha$'s such that $||x=\check \alpha||$ increases to $1$ without ever equaling it, or am I just entirely misunderstanding what is going on?



*Why is it the case that $||\text{$x$ is an ordinal and $x\in\check \gamma$}||\leq \sum_{\alpha\in\gamma}||x=\check \alpha||$? More specifically, it seems like both sides should be equal, so why is this not the case?


*Why does $||\check \alpha\in x||=\sum_{t\in\text{dom}(x)}(||\check \alpha=t||\cdot x(t))$ imply there is only a set of $\alpha$'s such that $||\check \alpha\in x||\neq 0$? I don't really understand this step at all.
 A: For (1): In fact, it is absolutely possible to have for example $\lVert x \mathrm{~is~an~ordinal} \rVert = 1$ without there existing any particular ordinal $\alpha$ such that $\lVert x = \check \alpha \rVert$.  Instead, the way I would think about the interpretation of this lemma as "$V$ and $V^B$ have the same ordinals" is: using this lemma, you can prove that
$$\lVert (\forall x) (x \mathrm{~is~an~ordinal} \leftrightarrow x \in \dot V \wedge \dot V \models x \mathrm{~is~an~ordinal}) \rVert = 1.$$
Here $\dot V$ is not strictly speaking a name (in fact the above axiom implies $\dot V$ cannot be a set -- otherwise you would be able to take the sup of the ordinals of $\dot V$ and get another ordinal in $\dot V$, resulting in a contradiction along the lines of the Burali-Forti paradox).  Instead, you take "$\cdot \in \dot V$" as being syntactic sugar for a unary predicate extension to the language of ZFC, whose interpretation is $\lVert x \in \dot V \rVert := \sum_{y\in V} \lVert x = \check y \rVert$.
For (2): You're correct, the two sides are equal.  Presumably, Jech wants to emphasize the direction of the inequality he will be using in the following parts of the proof.  (And this direction is in fact probably the easiest part of the proof that the two sides are equal.)
For (3): I'm also not sure what Jech is getting at here.  (Maybe some sort of inductive proof, which involves mutual induction with showing that the class of $\alpha$ with $\lVert \check \alpha = t \rVert \ne 0$ is also a set?)  To me, the essential point is: by the construction of $V^B$, any name has an upper bound on its rank.  Namely, if $x \in V^B_\alpha$, then by induction on $\alpha$, you can prove that $\lVert \operatorname{rank}(x) < \check\alpha \rVert = 1$.  On the other hand, you also have that if $\alpha$ is an ordinal of $V$, then $\lVert \operatorname{rank}(\check\alpha) = \check\alpha \rVert = 1$ (more generally, in fact, for any $x\in V$, you have $\lVert \operatorname{rank}^{V^B}(\check x) = (\operatorname{rank}^V(x)) \check{} \rVert = 1$).  Therefore, if $x \in V^B_\gamma$, and $\alpha \in ORD^V$ with $\alpha \ge \gamma$, then $\lVert \check\alpha \in x \rVert = 0$.
(Here, we are treating "$\operatorname{rank}(\cdot) < \cdot$" and "$\operatorname{rank}(\cdot) = \cdot$" as representing formulas in the language of ZFC, involving the existence of a function on the transitive closure of the first free variable satisfying the recursive definition of rank.)
