CH makes the nice refinement strongly hereditarily separable

A space $Y$ is hereditarily separable exactly when it has no left-separated sequence $⟨y_{\xi }:\xi <{\omega }_1⟩$, where $y_{\xi }\mathrm{\notin }\overline{\{y_{\zeta }:\zeta <\xi \}}$. If a subspace $A$ is nonseparable, recursively choose $y_{\xi }\in A$ outside the closure of its countable set of predecessors; otherwise those predecessors would be a countable dense subset of $A$. Conversely, for a left-separated sequence and a countable subset $D$ of its range, choose $\xi$ above every index represented in $D$; the separating neighbourhood of $y_{\xi }$ misses $D$, so $D$ is not dense in the sequence subspace.

We will use the following standard Vietoris reduction, whose proof is included. Let $B,F$ be compact in a zero-dimensional space, with $F⊊B$, and let $\mathcal{G}$ be a standard-form local base at $F$. For $G=N(U_0,\dots ,U_r)$ put $S\downarrow G=\{K\setminus \bigcup G:K\in S,K\cap U_i\mathrm{\ne }\mathrm{\varnothing }(i\le r),K\setminus \bigcup G\mathrm{\ne }\mathrm{\varnothing }\}$. Then $B\in \bar{S}$ iff $B\setminus \bigcup G\in \overline{S\downarrow G}$ for every $G\in \mathcal{G}$ with nonempty remainder. Forward, combine any standard neighbourhood of the remainder, chosen disjoint from $\bigcup G$, with the cells of $G$ to obtain a neighbourhood of $B$. Reverse, refine any standard neighbourhood of $B$ so its cells meeting $F$ contain some $G\in \mathcal{G}$, retain the cells disjoint from $F$, and add the finitely many remainders of the former cells; the assumed closure of the remainder then supplies an element of $S$ in this refinement. For $F=\{p\}$ this says that, along any clopen local base $V$ at $p$ that splits $B$, $B\in \bar{S}$ iff every $B\setminus V$ lies in the closure of $\{K\setminus V:K\in S,V\text{ splits }K\}$.

The original topology $\mathcal{T}$ is zero-dimensional Hausdorff, hence regular and $T_1$; [F5] therefore gives a metric inducing it. Since $\tilde{\mathcal{T}}$ refines $\mathcal{T}$, this metric topology is a coarser topology on the final space.

For each countable $\delta <{\omega }_1$, ${\mathring{\mathcal{T}}}_{\delta }$ is second countable: add the countably many sets $V_n^{\xi }$ with $\xi <\delta$ to a countable base for $\mathcal{T}$ and close under finite intersections. Finite lists from this base form a countable standard Vietoris base for $K({\omega }_1,{\mathring{\mathcal{T}}}_{\delta })$. Every subspace of a second-countable space is second countable and, under [F10], separable by choosing one point from every nonempty basic trace. Thus this hyperspace is hereditarily separable by step 1.1.

The first closure-transfer claim is the stage case. Let $\max B=\beta$, let $S\in M_{\beta +1}$ be countable with $S\subseteq K(\beta ,\tilde{\mathcal{T}}\upharpoonright \beta )$, and suppose $B\in \bar{S}$ for the ${\mathring{\mathcal{T}}}_{\beta }$ Vietoris topology. The final-open neighbourhood $V_0^{\beta }$ of $\beta$ leaves a compact remainder $B\setminus V_0^{\beta }$ in the coarser intermediate topology; the decreasing $W_n^{\beta }$-base and compactness give $r$ with $B\cap W_r^{\beta }\subseteq V_0^{\beta }$, so every ring intersection of index at least $r$ lies in its $H$-piece. If $r=0$, each finite danger zone is clopen and misses $B$, hence $B$ is in the intermediate closure of every ${\mathrm{\Gamma }}_{\beta }(S,\nu )$. Choose infinitely large $\nu$ from $({\star }_{\beta })$ and then $K\in {\mathrm{\Gamma }}_{\beta }(S,\nu )$ close to $B$ and $J\in {\mathrm{\Gamma }}_{\beta }(S,\omega )$ with $d_{\beta }(K,J)\le 2^{-\nu }$. The triangle inequality makes such $J$ arbitrarily Hausdorff-close to $B$, and the intermediate and final point-bases agree on $\{\beta \}\cup {\bigcup }_{\mathrm{\ell }}{H}_{\mathrm{\ell }}^{\beta }$, so $B$ is in the final closure of $S$. If an earlier ring is bad, increase $r$ beyond it, put $W=W_r^{\beta }$, and use standard neighbourhoods $G$ of the nonempty compact part $B\setminus W$, all with cells below $\beta$ and hence in $M_{\beta +1}$. The family $S\downarrow G$ is in the model, while the tail $B\cap W$ has no danger-zone intersections; apply the $r=0$ argument to every such tail and then the reduction of step 1.2 to recover $B$.

The full closure-transfer claim follows by induction on $\max B$. Fix $\alpha$ and suppose $S\in M_{\alpha +1}$ is countable in $K(\alpha ,\tilde{\mathcal{T}}\upharpoonright \alpha )$, every assigned $W_n^{\beta }$ for $\beta \in B$ belongs to $M_{\alpha +1}$, and $B\in \bar{S}$ for ${\mathring{\mathcal{T}}}_{\alpha }$. If $\max B<\alpha$, the intermediate and final bases already agree on $B$; if $\max B=\alpha$, step 2.2 applies. If $\beta =\max B>\alpha$ and $B=\{\beta \}$, the common $W_n^{\beta }$ bases transfer closure first to ${\mathring{\mathcal{T}}}_{\beta }$, then step 2.2 transfers it to the final topology. Otherwise, for every sufficiently small splitting $W_n^{\beta }$, step 1.2 gives $B\setminus W_n^{\beta }\in \overline{S_n}$ in ${\mathring{\mathcal{T}}}_{\alpha }$, where $S_n=\{K\setminus W_n^{\beta }:K\in S,W_n^{\beta }\text{ splits }K\}\in M_{\alpha +1}$. Its maximum is below $\beta$ and it inherits the model condition, so the induction hypothesis transfers this closure to the final topology, hence to the coarser ${\mathring{\mathcal{T}}}_{\beta }$ topology. Step 1.2 reconstructs $B\in \bar{S}$ there, and step 2.2 finishes the transfer to $\tilde{\mathcal{T}}$.

Suppose there were a left-separated sequence $⟨B_{\xi }:\xi <{\omega }_1⟩$ of sets of one fixed finite size $0<n<\omega$ in $K({\omega }_1,\tilde{\mathcal{T}})$ and a fixed $\gamma <{\omega }_1$ such that the $B_{\xi }\setminus \gamma$ were pairwise disjoint. Every $B_{\xi }$ has a maximum. Using step 2.1, thin so the maxima $a_{\xi }=\max B_{\xi }$ are strictly increasing; bounded maxima would put an uncountable left-separated sequence in one of the second-countable intermediate hyperspaces.

For finite target compacta, the model condition in step 3.1 can be removed. Induct on $k=\mathrm{\mid }B\mathrm{\mid }$. If $B\subseteq M_{\alpha +1}$, the global assigned-base map and finiteness put all its $W$-bases in the model, so step 3.1 applies. For $k=1$ outside the model, transfer the singleton first to its own intermediate stage, where its $W$-base is in the model, and use step 3.1 there. Let $k>1$, assume the claim below $k$, and put $\lambda =M_{\alpha +1}\cap {\omega }_1$. After moving $\alpha$ to the first point of $B$ above it when necessary, either $B$ is captured by the next model or $\alpha \in B$ and $B=B^{-}\cup B^{+}$, where $B^{-}=B\cap \lambda$ and $B^{+}=B\setminus \lambda$ are both nonempty and smaller than $B$. With $\zeta =\max B^{-}$, let $E$ consist of the $\mathrm{\mid }{B}^{+}\mathrm{\mid }$-element $H\subseteq (\zeta ,{\omega }_1)$ for which $B^{-}\cup H\in \bar{S}$ in ${\mathring{\mathcal{T}}}_{\alpha }$. The set $E$ belongs to $M_{\alpha +1}$, and step 2.1 gives in that model a countable dense $F\subseteq E$. Every $H\in F$ lies in the model, so step 3.1 puts $B^{-}\cup H$ in the final closure of $S$. Meanwhile $B^{+}\in \bar{F}$ transfers to the intermediate stage $\beta =\min B^{+}$ because those topologies have the same point-bases on $B^{+}$; the induction hypothesis, applied to the smaller target $B^{+}$, transfers it to the final topology. Given a standard neighbourhood of $B^{-}\cup B^{+}$ with one disjoint cell at each point, first choose $H\in F$ whose points enter the $B^{+}$-cells, then use the final closure of $B^{-}\cup H$ to choose an element of $S$ in all cells. Thus $B$ is in the final closure of $S$.

For each $\delta <{\omega }_1$, step 2.1 gives an ordinal ${\rho }_{\delta }>\delta$ such that $\{B_{\xi }:\xi <{\rho }_{\delta }\}$ is dense in the whole sequence for the ${\mathring{\mathcal{T}}}_{\delta }$ Vietoris topology; choose the least such ordinal. Refinement gives ${\rho }_{\delta }\le {\rho }_{ϵ}$ when $\delta <ϵ$. The simultaneous closure points of $\delta \mapsto {\rho }_{\delta }$ and $\xi \mapsto a_{\xi }$ contain a club $C$ by [F9]. Choose a limit $\eta \in C$ above $\gamma$. Then $S=\{B_{\xi }:\xi <\eta \}$ is a subset of $K(\eta ,\tilde{\mathcal{T}}\upharpoonright \eta )$ and is dense in the whole sequence for ${\mathring{\mathcal{T}}}_{\eta }$: any basic neighbourhood mentions finitely many switched coordinates and therefore already belongs to some earlier intermediate topology.

Every hereditarily countable set is coded by a relation on a subset of $\omega$, so $\mathrm{\mid }H({\mathrm{\aleph }}_1)\mathrm{\mid }\le 2^{{\mathrm{\aleph }}_0}$; the reverse inequality follows because every subset of $\omega$ is hereditarily countable. Thus [F3] gives $\mathrm{\mid }H({\mathrm{\aleph }}_1)\mathrm{\mid }={\mathrm{\aleph }}_1$. Elementarity puts a bijection from ${\omega }_1$ onto $H({\mathrm{\aleph }}_1)$ in $M_1$, and the chain contains every countable ordinal, so $H({\mathrm{\aleph }}_1)\subseteq M_{{\omega }_1}={\bigcup }_{\alpha <{\omega }_1}{M}_{\alpha }$. Hence choose $\alpha >\eta$ with $S\in M_{\alpha +1}$. Only countably many $B_{\xi }\setminus \gamma$ meet the countable interval $[\eta ,\alpha ]$, because those free parts are pairwise disjoint; choose $\xi >\alpha +1$ with $B_{\xi }\cap [\eta ,\alpha ]=\mathrm{\varnothing }$. The point-bases of ${\mathring{\mathcal{T}}}_{\eta }$ and ${\mathring{\mathcal{T}}}_{\alpha }$ agree at every point of $B_{\xi }$ (points below $\eta$ use $V$, points above $\alpha$ use $W$), so their standard Vietoris local bases agree there and step 4.2 yields $B_{\xi }\in \bar{S}$ for ${\mathring{\mathcal{T}}}_{\alpha }$. The finite-target transfer in step 4.1 gives $B_{\xi }\in \bar{S}$ in the final topology. But $S$ consists entirely of predecessors of $B_{\xi }$, contradicting left separation.

Therefore no left-separated sequence of one fixed nonzero finite size can have pairwise-disjoint parts above one fixed countable ordinal.

Fix $0<n<\omega$. If $[{\omega }_1{]}^n$ in the final Vietoris topology were not hereditarily separable, step 1.1 would give a left-separated sequence of $n$-element sets. By [F6], thin it to a $\mathrm{\Delta }$-system with finite root $R$ and put $\gamma =\sup \{\rho +1:\rho \in R\}$, taking $\gamma =0$ when $R=\mathrm{\varnothing }$. The parts above $\gamma$ are pairwise disjoint, contradicting step 6.1. Thus $[{\omega }_1{]}^n$ is hereditarily separable for every positive $n$.

Fix $0<n<\omega$ and suppose the final product $({\omega }_1,\tilde{\mathcal{T}}{)}^n$ were not hereditarily separable. By step 1.1 choose a left-separated sequence of $n$-tuples and thin so its coordinate-equality pattern is fixed. Retain one representative of each of its $m$ coordinate classes; intersecting the finitely many product coordinates belonging to one class shows that the resulting $m$-tuple sequence is still left separated. Using the coarser metric topology from step 1.3, choose pairwise closure-disjoint basic cells around the $m$ distinct coordinates and thin, by second countability, until the cells are fixed. For each tuple intersect a final-product separating neighbourhood with those cells. The corresponding standard Vietoris neighbourhood then separates its underlying $m$-element set from all earlier such sets: disjoint cells force membership in the Vietoris neighbourhood to match coordinatewise membership in the product neighbourhood. This produces a left-separated sequence in $[{\omega }_1{]}^m$, contradicting step 7.1.

Therefore every nonempty finite power is hereditarily separable, exactly as asserted. The zero power is excluded by [F8]; $n=1$ is included; empty standard neighbourhood families and empty $\mathrm{\Delta }$-roots were handled in steps 1.2 and 7.1. CH is used only in step 5.1 to capture the countable dense segment in a later model, while all other selections are the ZFC uses recorded by [F10].