Given a strongly inaccessible cardinal $\kappa$, consider the stationary tower forcing $\mathbb{P}_{<\kappa}=\{a\in V_\kappa:\,a\;\text{stationary in}\;\mathcal{P}(\bigcup a)\}$ and $G\subseteq \mathbb{P}_{<\kappa}$ a $V-$generic filter. It is easy to see that given $X\in V_\kappa$ the sets $$U_X=\{b_X: b\in G,\;\bigcup b\supseteq X\}$$ are ultrafilters on $\mathcal{P}(X)$ extending the club filter $Club(\mathcal{P}(X))$ (here, by $b_X$ is meant the projection of $b$ onto $X$, $b_X=\{Z\cap X: Z\in b\}$). Therefore, every member of $U_X$ is stationary.
With this ultrafilters is possible to define the corresponding ultrapowers embeddings and then take the direct limit. The natural elementary embedding $j:V\longrightarrow M$ between the universe and the direct limit $M$ is the stationary tower embedding defined by $\mathbb{P}_{<\kappa}$.
My question is related with the forcing relation of $\mathbb{P}_{<\kappa}$. For instance, in Corollary 2.2.11 from Larsson's book the author states the following: $$a\Vdash j(\alpha)=\beta\;\Longleftrightarrow\;\{Z\subset \bigcup a:\,otp(Z\cap \beta)=\alpha\,\vee\, Z\notin a\}\;\;\text{is a club in}\;\mathcal{P}(\bigcup a) $$
for $a\in\mathbb{P}_{<\kappa}$, $\bigcup a\supset \beta$ and $\alpha\in\beta$. This is a consequece of the fact that every ordinal $\beta$ is represented in the directed limit by the order type function $otp:\mathcal{P}(\beta)\longrightarrow \beta$. Regarding to this equivalence, I am willing to see that
$$a\Vdash j(\alpha)=\beta\;\Longleftrightarrow\;\{Z\subset \bigcup a:\,otp(Z\cap \beta)=\alpha\}\in U_{\bigcup a}$$
simply by definition of direct limit. My question is, how to prove the following equivalence
$$\{Z\subset \bigcup a:\,otp(Z\cap \beta)=\alpha\}\in U_{\bigcup a}\;\Longleftrightarrow\;\{Z\subset \bigcup a:\,otp(Z\cap \beta)=\alpha\,\vee\, Z\notin a\}\;\;\text{is a club in}\;\mathcal{P}(\bigcup a) $$
Any help or comment would be gratefull.
Here is one way of verifying Cor 2.2.11, we verify the following equivalence:
$ \forall G,P_{\kappa} \text{-generic} \ ( a \in G \rightarrow \{ Z \subseteq \bigcup a \ | \ otp(Z \cap \beta ) = \alpha \} \ \in U_{\bigcup a} ) \\ \longleftrightarrow \\\ \{ Z \subseteq \bigcup a \ | \ otp(Z \cap \beta) = \alpha \ \vee Z \not\in a \} \text{ is a club in } \ \mathcal{P}(\bigcup a) $
$(\rightarrow)$ If $Y = \{ Z \subseteq \bigcup a \ | \ otp(Z \cap \beta) = \alpha \ \vee Z \not\in a \}$ is not a club, then we can find $b \subseteq \mathcal{P}(\bigcup a) $ which is stationary and $ b \cap Y = \emptyset $. It follows that $b \leq a$ in the $\mathbb{P}_{<\kappa}$ order, but $b\in G $ implies $\{Z \subseteq \mathcal{P}(\bigcup b) \ | \ otp(Z \cap \beta) \neq \alpha \} \in U_{\bigcup b}$, so $b \Vdash j(\check{\alpha}) \neq \check{\beta} $ which is a contradiction.
$(\leftarrow)$
if $a \in G$, then $U_{\bigcup a} $ extends the club filter, so $\{ Z \subseteq \bigcup a \ | \ otp(Z \cap \beta) = \alpha \ \vee Z \not\in a \} \in U_{\bigcup a}$, on the other hand $a \in G $ implies $a \in U_{\bigcup a}$ so $\{Z \subseteq \mathcal{P}(\bigcup a) \ | \ otp(Z \cap \beta ) = \alpha \} = Y \cap a \in U_{\bigcup a} $.