[proofplan] We first verify that the derived collection $U_j$ is a proper filter on $\kappa$ by using that $j(\kappa)$ is an ordinal strictly above $\kappa$ and that elementary embeddings preserve inclusion and finite intersections. The ultrafilter property follows from preservation of complements inside $\kappa$: exactly one of $X$ and $\kappa \setminus X$ contains $\kappa$ after applying $j$. Non-principality follows because $j$ fixes every ordinal below $\kappa$, so it fixes every singleton $\{\alpha\}$ for $\alpha < \kappa$. Finally, $\kappa$-completeness is obtained by applying elementarity to an indexed intersection of length $\lambda < \kappa$, using $j(\lambda)=\lambda$ and $j(s)(\alpha)=j(s(\alpha))$ for each $\alpha < \lambda$. [/proofplan] [step:Use the critical point to place $\kappa$ inside $j(\kappa)$] Since $\kappa = \operatorname{crit}(j)$, the embedding $j$ fixes every ordinal $\alpha < \kappa$ and satisfies $j(\kappa) > \kappa$. Because $j(\kappa)$ is an ordinal and ordinals are transitive, $j(\kappa) > \kappa$ implies $\kappa \in j(\kappa)$. For every $X \subset \kappa$, elementarity applied to the statement $X \subset \kappa$ gives $j(X) \subset j(\kappa)$. Let $\mathcal{P}(\kappa)$ denote the power set of $\kappa$. Hence the condition $\kappa \in j(X)$ is meaningful for every $X \subset \kappa$, and $U_j \subset \mathcal{P}(\kappa)$. [/step] [step:Show that $U_j$ is a proper filter on $\kappa$] Because $\kappa \in j(\kappa)$, we have $\kappa \in j(\kappa)$ with $\kappa \subset \kappa$ understood as the whole underlying set of the filter, so $\kappa \in U_j$. Also $\varnothing \notin U_j$, since elementarity gives $j(\varnothing)=\varnothing$, and therefore $\kappa \notin j(\varnothing)$. To prove upward closure, let $X,Y \subset \kappa$ satisfy $X \in U_j$ and $X \subset Y$. By definition of $U_j$, $\kappa \in j(X)$. Elementarity applied to $X \subset Y$ gives $j(X) \subset j(Y)$, so $\kappa \in j(Y)$. Therefore $Y \in U_j$. To prove closure under finite intersections, let $X,Y \in U_j$. Then $\kappa \in j(X)$ and $\kappa \in j(Y)$. Elementarity applied to the Boolean operation of intersection gives \begin{align*}j(X \cap Y)=j(X)\cap j(Y).\end{align*} Thus $\kappa \in j(X)\cap j(Y)=j(X\cap Y)$, so $X\cap Y \in U_j$. Therefore $U_j$ is a proper filter on $\kappa$. [guided] We verify the filter axioms directly from the definition \begin{align*} U_j=\{X\subset \kappa:\kappa\in j(X)\}. \end{align*} First, the whole set $\kappa$ belongs to $U_j$. The critical point hypothesis gives $j(\kappa)>\kappa$. Since $j(\kappa)$ is an ordinal, the inequality $\kappa<j(\kappa)$ means precisely that $\kappa\in j(\kappa)$. Hence $\kappa\in U_j$. Second, the empty set does not belong to $U_j$. Elementary embeddings preserve the empty set, so $j(\varnothing)=\varnothing$. Since $\kappa\notin\varnothing$, we get $\varnothing\notin U_j$. This proves properness at the level of the two extreme sets. Now let $X,Y\subset \kappa$ with $X\in U_j$ and $X\subset Y$. The membership $X\in U_j$ means $\kappa\in j(X)$. Elementarity preserves inclusion, so from $X\subset Y$ we obtain $j(X)\subset j(Y)$. Therefore $\kappa\in j(Y)$, which is exactly $Y\in U_j$. This proves upward closure. Finally, let $X,Y\in U_j$. Then $\kappa\in j(X)$ and $\kappa\in j(Y)$. Elementarity preserves intersections, hence \begin{align*}j(X\cap Y)=j(X)\cap j(Y).\end{align*} Since $\kappa$ belongs to both $j(X)$ and $j(Y)$, it belongs to their intersection. Therefore \begin{align*}\kappa\in j(X)\cap j(Y)=j(X\cap Y).\end{align*} By the definition of $U_j$, this says $X\cap Y\in U_j$. Thus $U_j$ is a proper filter on $\kappa$. [/guided] [/step] [step:Use complements to prove the ultrafilter property] Let $X \subset \kappa$. Elementarity applied to relative complement inside $\kappa$ gives \begin{align*} j(\kappa \setminus X)=j(\kappa)\setminus j(X). \end{align*} Since $j(X)\subset j(\kappa)$ and $\kappa\in j(\kappa)$, exactly one of the two alternatives holds: \begin{align*} \kappa\in j(X) \end{align*} or \begin{align*} \kappa\in j(\kappa)\setminus j(X)=j(\kappa\setminus X). \end{align*} Thus exactly one of $X$ and $\kappa\setminus X$ lies in $U_j$. Since $U_j$ is already a proper filter, this proves that $U_j$ is an ultrafilter on $\kappa$. [/step] [step:Show that no singleton belongs to $U_j$] Let $\alpha<\kappa$. Since $\kappa$ is the critical point of $j$, we have $j(\alpha)=\alpha$. Elementarity preserves singleton formation, so \begin{align*}j(\{\alpha\})=\{j(\alpha)\}=\{\alpha\}.\end{align*} Because $\alpha<\kappa$, we have $\kappa\ne \alpha$, and hence $\kappa\notin \{\alpha\}=j(\{\alpha\})$. Therefore $\{\alpha\}\notin U_j$. Since no singleton subset of $\kappa$ belongs to $U_j$, the ultrafilter $U_j$ is non-principal. [/step] [step:Take fewer than $\kappa$ many sets in $U_j$ and intersect them] Let $\lambda<\kappa$, and let \begin{align*} s:\lambda \to U_j \end{align*} be a sequence of members of $U_j$. For each $\alpha<\lambda$, define \begin{align*} X_\alpha=s(\alpha). \end{align*} Define the indexed intersection inside the ambient set $\kappa$ by \begin{align*} X=\{\beta\in\kappa: \beta\in X_\alpha \text{ for every } \alpha<\lambda\}. \end{align*} Equivalently, $X=\bigcap_{\alpha<\lambda}X_\alpha$, with the convention that the empty intersection for $\lambda=0$ is the ambient set $\kappa$. We prove $X\in U_j$. Since $\lambda<\kappa$, the critical point property gives $j(\lambda)=\lambda$ and $j(\alpha)=\alpha$ for every $\alpha<\lambda$. For each $\alpha<\lambda$, elementarity of function evaluation gives \begin{align*} j(s)(\alpha)=j(s)(j(\alpha))=j(s(\alpha))=j(X_\alpha). \end{align*} Because $X_\alpha\in U_j$, we have $\kappa\in j(X_\alpha)$ for every $\alpha<\lambda$. Therefore \begin{align*} \kappa\in \bigcap_{\alpha<\lambda}j(X_\alpha). \end{align*} Using the preceding identity for the terms of $j(s)$, this is the same as \begin{align*} \kappa\in \bigcap_{\alpha<j(\lambda)}j(s)(\alpha). \end{align*} Since $s$ is a set-sized function with domain $\lambda$ and range contained in $\mathcal{P}(\kappa)$, the definition \begin{align*} X=\{\beta\in\kappa: \beta\in s(\alpha) \text{ for every } \alpha<\lambda\} \end{align*} is a first-order set definition from the parameters $s$, $\lambda$, and $\kappa$. Elementarity transfers this definition to \begin{align*} j(X)=\{\beta\in j(\kappa): \beta\in j(s)(\alpha) \text{ for every } \alpha<j(\lambda)\}. \end{align*} Thus $j(X)=\bigcap_{\alpha<j(\lambda)}j(s)(\alpha)$ as an intersection inside $j(\kappa)$. We conclude $\kappa\in j(X)$. Hence $X\in U_j$. [guided] The goal is to prove closure under intersections indexed by any ordinal $\lambda<\kappa$. So fix such a $\lambda$, and let \begin{align*}s:\lambda\to U_j\end{align*} be a sequence of sets in the filter. For each $\alpha<\lambda$, write $X_\alpha=s(\alpha)$. Since the range of $s$ is contained in $U_j\subset\mathcal{P}(\kappa)$, each $X_\alpha$ is a subset of $\kappa$. Define the indexed intersection inside the ambient set $\kappa$ by \begin{align*}X=\{\beta\in\kappa: \beta\in X_\alpha \text{ for every } \alpha<\lambda\}.\end{align*} This is the same as $X=\bigcap_{\alpha<\lambda}X_\alpha$, with the convention that when $\lambda=0$ the empty intersection is $\kappa$. To prove $X\in U_j$, we must prove $\kappa\in j(X)$. The key point is that the index length is below the critical point. Since $\lambda<\kappa$, the embedding fixes $\lambda$ and every smaller ordinal: \begin{align*}j(\lambda)=\lambda.\end{align*} For each $\alpha<\lambda$, we also have $j(\alpha)=\alpha$. Applying elementarity to function evaluation gives \begin{align*}j(s)(\alpha)=j(s)(j(\alpha))=j(s(\alpha))=j(X_\alpha).\end{align*} This identity says that the $\alpha$-th set in the transformed sequence $j(s)$ is exactly the image under $j$ of the original $\alpha$-th set. Now use the hypothesis that every $X_\alpha$ lies in $U_j$. By definition of $U_j$, for every $\alpha<\lambda$ we have \begin{align*}\kappa\in j(X_\alpha).\end{align*} Using the identity $j(s)(\alpha)=j(X_\alpha)$, this becomes \begin{align*}\kappa\in j(s)(\alpha)\end{align*} for every $\alpha<j(\lambda)$. Therefore $\kappa$ belongs to the indexed intersection: \begin{align*}\kappa\in \bigcap_{\alpha<j(\lambda)}j(s)(\alpha).\end{align*} Finally, elementarity preserves the first-order definition of this indexed intersection. The relevant definition is not a vague external convention: it is the set formula \begin{align*}X=\{\beta\in\kappa: \beta\in s(\alpha) \text{ for every } \alpha<\lambda\}.\end{align*} Because $s$ is a set-sized function from $\lambda$ into $\mathcal{P}(\kappa)$, this formula defines a set from the parameters $s$, $\lambda$, and $\kappa$. Applying $j$ to that definition gives \begin{align*}j(X)=\{\beta\in j(\kappa): \beta\in j(s)(\alpha) \text{ for every } \alpha<j(\lambda)\}.\end{align*} Thus $j(X)=\bigcap_{\alpha<j(\lambda)}j(s)(\alpha)$ as an intersection inside $j(\kappa)$, and the previous membership becomes \begin{align*}\kappa\in j(X).\end{align*} By the definition of $U_j$, this proves $X\in U_j$. Thus every intersection of fewer than $\kappa$ many members of $U_j$ again lies in $U_j$. [/guided] [/step] [step:Conclude that the derived measure has all required properties] We have shown that $U_j$ is a proper filter on $\kappa$, that for every $X\subset\kappa$ exactly one of $X$ and $\kappa\setminus X$ belongs to $U_j$, that no singleton subset of $\kappa$ belongs to $U_j$, and that $U_j$ is closed under intersections of length $\lambda$ for every $\lambda<\kappa$. Therefore $U_j$ is a non-principal $\kappa$-complete ultrafilter on $\kappa$. [/step]