Transitivity and a valuation rank bound

If $x\in y\in M[G]$, write $y={\mathrm{val}}_G(\tau )$ for a name $\tau \in M$. By F1 some $⟨\sigma ,p⟩\in \tau$ has $p\in G$ and $x={\mathrm{val}}_G(\sigma )$. Transitivity of M, applied through the Kuratowski pair, gives $\sigma \in M$; F2 says that sigma is a name. Thus $x\in M[G]$, proving transitivity.

Induct on the subname relation. Every member of the valuation of tau is the valuation of some sigma below tau, so F3 gives its rank as the supremum of their value-ranks plus one. By induction this is at most the supremum of ${\mathrm{rk}}_P(\sigma )+1$ over all subnames sigma, which F2 identifies with ${\mathrm{rk}}_P(\tau )$. With no selected subnames the value rank is zero and the inequality still holds. This includes both the empty name and empty G.