Supercompactness and closed elementary embeddings

From a normal fine U take j and s=j``lambda as in F1. Every map from its index set into eta<kappa has a constant U-large fibre, for otherwise kappa-completeness intersects all fibre complements to empty. Induct on alpha<kappa. Each predecessor of the constant-alpha class, for alpha>0, can be modified outside its U-large membership set to take values in alpha; the fibre argument makes it constant. For alpha=0 there are no predecessors. The collapse equation then gives j(alpha)=alpha. F1 gives j(kappa)>lambda>=kappa, so the critical point is exactly kappa.

Let $⟨a_{\alpha }:\alpha <\lambda ⟩$ be an ambient sequence of elements of M. The collapse has a unique Scott preimage for each a_alpha. Replacement therefore collects these nonempty set representatives; F3 chooses f_alpha from each one, so $\pi ([f_{\alpha }{]}_U)=a_{\alpha }$. Define the set function $F(x)=\{(\alpha ,f_{\alpha }(x)):\alpha \in x\}$. Its collapsed class G is exactly $\{(j(\alpha ),a_{\alpha }):\alpha <\lambda \}$. For the inclusion from right to left use fineness: on the alpha-cone the pair (alpha,f_alpha(x)) belongs to F(x), and coordinate pairing transfers through the collapse. Conversely, any represented member of [F] selects on a U-large set a unique pair with first component alpha(x) in x. Normality makes alpha(x) a fixed alpha on a U-large subset. The selected pair is then equivalent to (alpha,f_alpha(x)), giving the required collapsed pair. This proves both inclusions.

G belongs to M, and M has the increasing enumeration e of s of order type lambda by F1. Externally this enumeration is precisely alpha maps to j(alpha), by uniqueness of ordinal order type. Inside M compose the function with graph G with e. Its value at alpha is a_alpha, so the original ambient sequence belongs to M. The reindexing is essential: G itself has domain j``lambda, not generally lambda. Thus M has the asserted lambda-sequence closure.

Conversely suppose j satisfies the embedding and closure conditions. Each j(alpha) for alpha<lambda lies in M, so the set-restriction convention and closure put $j\upharpoonright \lambda$ in M. Its domain lambda and range s=j``lambda consequently belong to M. This increasing map exhibits there the order type lambda, so M regards |s| as at most |lambda| and hence below j(kappa), since lambda<j(kappa) and j(kappa) is a cardinal of M. Also s is a subset of j(lambda). Thus s belongs to j(P_kappa(lambda)). Define U by the displayed formula using Separation. Elementarity for empty, whole index set, complements and finite intersections makes U a proper ultrafilter. For eta<kappa, j fixes eta and maps a sequence of U-members to a sequence with those j-images at each fixed index; s belongs to their intersection, proving kappa-completeness. Each point cone is large because s contains every j(alpha), proving fineness.

For normality let f:S to lambda select an element of x for x in S, with S in U. Then s belongs to j(S), so j(f)(s) belongs to s=j``lambda. It equals j(alpha) for some alpha<lambda. Elementarity for that fibre gives $s\in j(\{x\in S:f(x)=\alpha \})$, so the fibre belongs to U. Hence U is normal, fine and kappa-complete, which is precisely lambda-supercompactness. All derived sets use the definable embedding convention; no Global Choice is required.