So say given $x\in WF$, with the property tr cl$(x)$ is finite.
I want to say that any elements $z\in$ tr cl$(x)$ has finite rank.
This seems to be true (intuitively speaking), because the construction of tr cl$(x)$ basically involves collecting all descendants of $x$ and do a union on that collection. So if some members in the transitive closure has infinite rank (of some ordinal), then "we would have collected all it's infinite descendants and hence the closure cannot be finite"
So is my intuition correct ?
If no, are there any simple counter-examples ?
Thanks and cheers.
This is true. In fact
$$ \tag{$\dagger$}\mathrm{rank}_\in (\mathrm{trcl}(x))= \sup \{ \mathrm{rank}_\in (z) +1 \mid y \in \mathrm{trcl}(z) \}$$
Now, since $\mathrm{trcl}(x)$ is finite it follows (by an $\in$-induction) that $\mathrm{rank}_\in(\mathrm{trcl}(x))$ is finite and hence that, for any $z \in \mathrm{trcl}(x)$, $\mathrm{rank}_\in(z)$ is finite.
Finally $(\dagger)$ can be proved by an $\in$-induction over all sets in $\mathrm{WF}$, i.e. prove that for all $x \in \mathrm{WF}$ $$ \mathrm{rank}_\in(x) = \sup \{ \mathrm{rank}_\in(y) +1 \mid y \in x \}.$$