I am looking at Zermelo's 1930a proof that if $\kappa$ is strongly inaccessible, then $V_{\kappa}$ is a model of ZF. To show that Powerset holds he takes an arbitrary set $x \in V_\kappa$ and assumes that $x$ can be well-ordered in type $\sigma <$ $\kappa$, whereby $2^{|\sigma|} = \wp(X) < \kappa$. I don't understand why the assumption is true: why can't the order type of $x$ be greater than $\kappa$, hence outside the model, given that the proof of well-ordering is a proof in the metatheory.
More generally, my question is: if we are using ZFC to prove results about some transitive set model, then by Choice in the metatheory, every set in our model can be well-ordered. Those well-orderings need only exist in the metatheory and not necessarily in our model. So then does it follow that the order type of a set in our model is itself in the model?
The fact that $\sigma<\kappa$ here isn't a general fact about transitive models; it's a consequence of the very special situation we are considering. Specifically, $\kappa$ is an inaccessible cardinal, so every element of $V_\kappa$ has cardinality less than $\kappa$ (see, for instance, my answer to an earlier question of yours). Therefore $x$ has cardinality less than $\kappa$, and therefore so does the order-type of any well-ordering of $x$.