Note: this is cross-posted from MSE.

This question is about the following remark (modified to be self-contained), found in Donald Martin’s book on determinacy, page 340. The context is proving agreement between $V$ and some inner model $M$ containing a same extender (although this context doesn’t seem to matter). Here, $kappa$ is a cardinal and $zetageqkappa$ is any ordinal.

Any function $f:kappatozeta^+$ can be coded by a wellordering $R$ of $zeta$ of ordertype sup(range($f$)) and a $tilde g:kappato zeta$.

The pair $langle R, tilde g rangle$ can be coded by a $g:kappato V_{zeta+1}$. Such a $g$ can in turn be coded by an element of $V_{zeta+1}$.

I don’t see why the sentences in bold are true. Or more specifically, I don’t know how to construct such a coding (Gödel pairing might not work, because we don’t know if $zeta$ is closed under the Gödel pairing function). I’m particularly puzzled by the last statement, that we can code $g:kappato V_{zeta+1}$ by an element of $V_{zeta+1}$. The flat pairing construction in the style of Quine seems to only produce a subset of $V_{zeta+1}$, hence an element of $V_{zeta+2}$.

The coding referred to in the first sentence is something like this: assume without loss of generality that $f:kappato zeta^+$ has range bounded by an ordinal $alpha$ between $zeta$ and $zeta^+$. This is okay, because $zeta^+$ is regular and we can always modify $f$ so that it sends something above $zeta$. So $alpha$ is the ordertype of some wellordering $Rsubseteq(zetatimeszeta)$, and $alpha$ has cardinality $zeta$. Furthermore, if $g’$ is a bijection between $alpha$ and $zeta$, then we can define $tilde g:kappatozeta$ by setting $tilde g(x)=g'(f(x))$. So given such a wellordering $R$ and function $tilde g$, we can recover $f$ by asking for the ordertype of $R$, and then seeing the pointwise preimage of $g’$.