A more classical construction of the Feferman Levy model (without symmetric models) I'm trying to produce $\aleph_1$ singular using a more classical version of Feferman Levy and $HOD$ models without going to symmetric models. I would like some help.
Assume $V = L$ and let $\mathbb{P} = \prod_{\text{finite support}, n <\omega} \text{Coll}(\omega, \aleph_n)$ and let $G$ be $V$-generic. Let $A = \cup_{n <\omega}\mathcal{P}(\omega) \cap V[G^{<n}]$. Let $W = HOD(A \cup \{A\})^{V[G]}$. I want to show that $(\omega_1$ is singular)$^{W}$.
I'm afraid I haven't gotten very far. It is clear enough that $A \neq \mathcal{P}(\omega)$ (in $V[G]$), but I need to show that $A = \mathcal{P}(\omega) \cap W$. The hint I was told was to see that for each $n <\omega$, there is a name for $A$, $\dot A_n \in V[G^{<n}]$ such that $\mathbb{P}^{\geq n}$ is $\{\dot A_n\}$-homogeneous in $V[G^{<n}]$, but I'm not sure how to see this name, and I'm not sure how it helps either. I also think that we're eventually meant to show that $(\omega_1 = \aleph_{\omega}^L)^{W}$ like the original argument.
Edit: I have managed to show that $A = \mathcal{P}(\omega) \cap W$ - I might edit it into this answer later but it's fairly routine and tedious.
I now just have to show that $(\omega_1 = \aleph_{\omega}^L)^{W}$ and then that $(\omega_1$ has cofinality $\omega)$.
 A: It is trivial to show that $\aleph_\omega^L\leq\aleph_1^W$, since we collapsed all the $\aleph_n^L$ to be countable. It is enough to show that $\aleph_\omega^L$ was not collapsed in $W$ to conclude that it is the new $\aleph_1$, and thereofre the cofinality is countable: $\{\aleph_n^L\mid n<\omega\}$ is a witness of that.
For this, suppose that $A$ is a set of ordinals in $W$, then there is some $\varphi(x,\alpha,g_1,\dots,g_n)$ which defines it (here $\alpha$ is an ordinal parameter and $g_i$ is the collapsing generic of $\aleph_i^L$). We want to show that there is a name $\dot A$ for $A$ such that $\dot A$ is actually a name in $\prod_{i\leq n}\operatorname{Coll}(\omega,\omega_i)$.
If we can do that, it is easy to see that $\aleph_\omega^L$ was not collapsed, since no initial segment of the product collapses it by the usual chain condition arguments (i.e. it's too small). So that will complete our proof.
Now let $p$ in the product be a condition such that $p\Vdash\varphi(\check\xi,\check\alpha,\dot g_1,\dots,\dot g_n)$. Let $m$ be the largest such that $p\in\prod_{i<m}\operatorname{Coll}(\omega,\omega_i)$ (without loss of generality $m>n$); and let $\vec\pi$ be a sequence of automorphisms of this product such that $\pi_i=\operatorname{id}$ for all $i\leq n$.
It is very easy to see that $\vec\pi p$, the condition obtained by pointwise application of $\pi_i$ to the $i$th coordinate of $p$, also forces that $\varphi(\check\xi,\check\alpha,\dot g_1,\dots,\dot g_n)$, because $\dot g_i$ is not moved by any $\pi_j$ for $j\neq i$, and $\pi_i$ was the identity; and $\check\xi$ and $\check\alpha$ are not moved by any automorphism.
Now use the homogeneity to argue that if $p\Vdash\varphi(\check\xi,\check\alpha,\dot g_1,\dots,\dot g_n)$, then $p\cap\prod_{i\leq n}\operatorname{Coll}(\omega,\omega_i)=p\restriction n+1$ also forces the same thing: otherwise there is some $q\leq p\restriction n+1$ such that $q\Vdash\lnot\varphi(\check\xi,\check\alpha,\dot g_1,\dots,\dot g_n)$, but we can find $\vec\pi$ as above such that $\vec\pi p$ is compatible with $q$, which is impossible.
Therefore, if $\dot A$ is any name for $A$, we can define $\{(p\restriction n+1,\check\xi)\mid p\Vdash\varphi(\check\xi,\check\alpha,\dot g_1,\dots,\dot g_n)\}$ as our name, and we are done.
