In Jech Set Theory, while proving that for every well-founded relation $E$ on a set $P$ there exists a unique function $\rho$ from $P$ into the ordinals satisfying $\rho(x) = \sup\{\rho(y)+1 : y E x \}$, he defines the following sets: $$P_0=\emptyset, \hspace{1mm} P_{\alpha+1}=\{ x\in P : \forall y \hspace{1mm} (yEx \rightarrow y\in P_{\alpha} \}, \hspace{1mm} P_{\alpha}=\bigcup_{\xi<\alpha}{P_{\xi}}$$ if $\alpha$ is limit. Then $P_0 \subset P_1 \subset \ldots \subset P_\theta = P$ for some $\theta$ and $\rho(x)$ is defined to be the least $\alpha$ such that $x \in P_{\alpha+1}$. Since $x E y$ implies $\rho(x) < \rho(y)$, he claims that it is easy to verify that this function $\rho$ satisfies $\rho(x) = \sup\{\rho(y)+1 : y E x \}$. To verify this, I have done the following:
Clearly, $\rho(y)+1 \leq \rho(x)$ for all $y E x$. If $\alpha = \rho(x)$ and $\alpha = \beta +1$, then, $x \in P_{\alpha+1}$, but $x \not \in P_\alpha=P_{\beta+1}$. So, there is some $y E x$ such that $y \not \in P_\beta$. For that $y$, $\rho(y)=\beta$ and so $\rho(y)+1=\alpha$. So, $\rho(x) = \alpha = \sup\{\rho(y)+1 : y E x \}$. If $\alpha$ is limit, then $\forall \xi < \alpha$, $x \not \in P_\xi$ and so all $P_\xi$'s miss some $y E x$, so these $\xi$'s cannot be the supremum. So, $\rho(x) = \alpha = \sup\{\rho(y)+1 : y E x \}$ and we are done.
Is this reasoning correct? I think I have overcomplicated it a lot so I would be happy if you can show some easier ways, thank you.
It appears to be correct, though your argument for limit $\alpha$ could be expressed more clearly. However, the division into two cases isn’t actually necessary.
If $\rho(x)=\alpha$, then $x\in P_{\alpha+1}\setminus P_\alpha$. Let $\beta=\sup\{\rho(y)+1:yEx\}$. If $yEx$, then $y\in P_\alpha$, so $\rho(y)<\alpha$, and hence $\rho(y)+1\le\alpha$. Thus, $\beta\le\alpha$. On the other hand, $y\in P_{\rho(y)+1}\subseteq P_\beta$ for each $yEx$, so $x\in P_{\beta+1}$, and therefore $\beta\ge\alpha$. Thus,
$$\rho(x)=\alpha=\beta=\sup\{\rho(y)+1:yEx\}\,.$$