Fine ultrapower seeds and normality

Kappa-completeness and uncountability imply countable completeness, so F2 gives the collapsed ultrapower and its formula-by-formula coordinate equivalence. At every coordinate x, x is a subset of lambda of size below kappa. The equivalence therefore says $s\in j(P_{\kappa }(\lambda ))$: M regards s as a subset of j(lambda) of size below j(kappa). As M is transitive, the subset statement also holds externally. For each alpha<lambda, the coordinate set where alpha belongs to x is U-large by F1, so j(alpha) belongs to s. All cardinal and collapse uses retain F3.

Suppose U normal. Any member of s is the collapsed class of a function f which selects f(x) in x on a U-large set S. On S these are ordinals below lambda, so F1 makes some fibre alpha U-large. Scott equality and injectivity of the collapse identify that member with j(alpha). Together with step 1.1 this proves s=j``lambda. Conversely suppose equality. Given f:S to lambda selecting an element of x on a U-large S, extend f by zero outside S. Its collapsed class belongs to s, hence is j(alpha) for some alpha<lambda. Scott equality says the extended f equals alpha on a U-large set. Intersect with S to obtain the required fibre of the original f. Thus U is normal.

At each coordinate, x is a set of ordinals, and its order type is below kappa: it has cardinality |x|<kappa and kappa is an initial ordinal. The formula defining the unique ordinal order type transfers by F2. Thus the collapsed class of x maps to otp(x) is the order type of s computed in M, and is below j(kappa). In the normal case the increasing map j restricted to lambda is an external order isomorphism of lambda with s by step 2.1. The order isomorphism supplied inside M is also an external one, since M is transitive and its graph and domain are sets; uniqueness of ordinal order types therefore makes its value exactly lambda. Hence lambda<j(kappa). This does not replace M's internal size bound by an unsupported external cardinal comparison in the merely fine case.