Definable subsets of the J-hierarchy in fine structure theory So there is a lemma in Ralf Schindler's book, which is said to be an immediate consequence of a previous lemma, but it is not really immediate to me. So let me give some context.
Let $E$ be a set or a proper class. We say a function or relation is $\text{rud}_E,$ if it is rudimentary in $E$. And for any transitive set $U$, $\text{rud}_E(U)$ denotes the closure of $U$ under $\text{rud}_E$ functions. And for a structure $(U, \in, E)$,  $\tilde{\Sigma}_n^{(U, \in, E)}$ denotes the set of $\Sigma_n$-definable relations with parameters from $U$ and $\tilde{\Sigma}_\omega^{(U, \in, E)} = \bigcup_{n\in\omega}\tilde{\Sigma}_n^{(U, \in, E)}$. Also we index the J-hierarchy with limit ordinals. 
And the following is the lemma which we will quote:

$(*)$ Let $U$ be a transitive set and $E \subseteq U$. Then $P(U)\cap\text{rud}_E(U\cup\{U\}) = P(U)\cap\tilde{\Sigma}_\omega^{(U, \in, E)}$.

And below is the lemma which is said to be a direct consequence of $(*)$:

Let $E$ be a set or a proper class. Assume that $E \subseteq Lim \times V$, where $Lim$ is the class of all limit ordinals. Let us write $E_\alpha = \{x: (\alpha, x) \in E\}$ and $E|\alpha = E \cap (\alpha \times V)$ for limit ordinals $\alpha$. Let assume that $E_\alpha \subseteq J_\alpha[E]$ and that $(J_\alpha[E], \in, E_\alpha)$ is amenable for every limit ordinal $\alpha$. Then 
  $$P(J_\alpha[E])\cap J_{\alpha + \omega}[E] = P(J_\alpha[E])\cap\tilde{\Sigma}_\omega^{(J_\alpha[E], \in, E|\alpha, E_\alpha)}.$$

So proving that the lhs is a subset of the rhs is not that hard because of the lemma, since $E\cap J_\alpha[E] = E|\alpha$. What I can't prove, is the converse and it's because of the $E_\alpha$ predicate. The best thing I tried was to modify the proof of $(*)$, but there I had to show that membership in $E_\alpha$ was $\text{rud}_E$, which isn't really clear to me. 
So I looked this up in the handbook of set theory, there the equivalent result was mentioned, without this $E_\alpha$ predicate. To me, the thing that seems to be the main obstacle, is that there is no clear connection between $E \cap J_\alpha[E]$ and $E_\alpha$. And that we have less information to work with, in the structure $(J_\alpha[E], \in, E)$.
I hope someone can clarify the situation and tell me how this lemma is proven.
 A: First, we can strenghen $(\ast)$ a bit in the following sense: If $F$ satisfies the same assumption as $E$ then $$\mathcal P(U)\cap\operatorname{rud}_{E, F}(U\cup\{U\})=\mathcal P(U)\cap\bar\Sigma_\omega^{(U, \in, E, F)}$$
where $\operatorname{rud}_{E, F}$ closes under functions that are rudimentary in $E$ or $F$. 
You can see that even with this relaxed assumption we cannot immediately apply $(\ast)$ to calculate $\mathcal P(J_{\alpha}[E])\cap J_{\alpha+\omega}[E]$ as elements of the form $(\alpha, x)\in E$ are not in $J_\alpha[E]$. This is why we need to consider $E_\alpha$. The following holds true:
$$\mathcal P(J_\alpha[E])\cap J_{\alpha+\omega}[E]=\mathcal P(J_\alpha[E])\cap\operatorname{rud}_{E|\alpha, E_\alpha}(J_\alpha[E]\cup\{J_\alpha[E]\})=\mathcal P(J_\alpha[E])\cap\bar\Sigma_\omega^{(J_\alpha[E],\in, E|\alpha, E_\alpha)}$$
The second equality is true by the revised version of $(\ast)$ above, noting that $E_\alpha\subseteq J_\alpha[E]$. For the first equality we simply observe that $$J_{\alpha+\omega}[E]=\operatorname{rud}_E(J_\alpha[E]\cup\{J_\alpha[E]\})=\operatorname{rud}_{E|\alpha+1}(J_\alpha[E]\cup\{J_\alpha[E]\})=\operatorname{rud}_{E|\alpha, E_\alpha}(J_\alpha[E]\cup\{J_\alpha[E]\})$$
Here the first equality is by definition, the second one holds as in general 
$$\operatorname{rud}_E(U\cup\{U\})=\operatorname{rud}_{E\cap V_{\operatorname{rank}(U)+\omega}}(U\cup\{U\})$$
for transitive $U$ and $E\cap V_{\alpha+\omega}=E|\alpha+1$. Finally, we argue that the last equality holds: For $\subseteq$ note that both $E|\alpha$ and $E_\alpha$ are rudimentary in $E$ over $J_{\alpha+\omega}[E]$. Similar for $\supseteq$, $E|\alpha+1$ is rudimentary in $E|\alpha, E_\alpha$ over $\operatorname{rud}_{E|\alpha, E_\alpha}(J_\alpha[E]\cup\{J_\alpha[E]\})$.
Finally I want to mention that it is definately possible that 
$$\mathcal P(J_\alpha[E])\cap \bar\Sigma_\omega^{(J_\alpha[E],\in, E)}\subsetneq\mathcal P(J_\alpha[E])\cap J_{\alpha+\omega}[E]$$
It is a nice exercise to come up with such an example. (Hint: there are some with $\alpha=\omega$)
