Scott ultrapowers and class-embedding conventions

In ZF let U be a proper ultrafilter on nonempty I, with completeness conventions as in Complete ultrafilters and measurable cardinals. For set functions $f,g:I\to V$ put $f{\sim }_{U}g$ iff $\{i:f(i)=g(i)\}\in U$. Let rho(f) be the least membership rank of any function equivalent to f, and define the Scott representative

$[f{]}_U=\{g:g:I\to V,g{\sim }_{U}f,\mathrm{rank}(g)=\rho (f)\}\mathrm{.}$

Use Membership rank under Foundation. Existence as a nonempty set and quotient invariance are proved in the following lemma. The universe ultrapower is the definable class of these representatives, with

$[f{]}_{U}E[g{]}_U⟺\{i:f(i)\in g(i)\}\in U\mathrm{.}$

Its constant map is $x\mapsto [c_x{]}_U$, where $c_x(i)=x$. The class of all equivalent functions is not used as a set representative.

A supplied definable elementary embedding $j:V\to M$ means a definable class function into a definable transitive class M, with set parameters allowed, satisfying elementarity separately for each fixed first-order formula. Its restriction to every set is a set by Replacement. Relativization and class language use Relativization agrees with induced set satisfaction; there is no uniform satisfaction predicate for V and no quantification over arbitrary class embeddings. Converse embedding characterizations retain this definability and set-restriction convention. No Global Choice or class-set theory is assumed.