I've a problem with a passage of the proof of Claim 14.7 of the paper "Cofinality spectrum theorems in model theory, set theory, and general topolgy" by Malliaris and Shelah, or equivalently Proposition 4D of Fremlin "p=t, following Malliaris-Shelah and Steprans", https://www1.essex.ac.uk/maths/people/fremlin/n14528.pdf (I'll refer to this second one). I have problems with the argument by contradiction inside the proof (starting from "P?"). In particular, I don't understand why $D\in G$: I know that by definition $D\Vdash \check{D}\in F$ for every $F$ generic over $\mathfrak{M}$ with $D\in F$, but in this case to me it seems that $G$ was fixed at the beginning, and then the sequence $\langle \dot{p}_\varepsilon\rangle_{\varepsilon<\alpha}$ was fixed accordingly to the chosen $G$ and thus we cannot chose again a different $G$ so that $D\in G$.
I will explain my difficulty with an example:
Let $\mathfrak{M}$ be a (CT) model of ZFC, $(B,\leq,\land,\lor,\neg,0,1)\in\mathfrak{M}$ a complete boolean algebra and let $G\subset B$ be a fixed ultrafilter generic over $\mathfrak{M}$ and $\mathfrak{M}[G]$ the generic model extending $\mathfrak{M}$ and containing $G$ obtained using forcing. Then $\mathfrak{M}[G]$ is also a model of ZFC and $G\in\mathfrak{M}[G]$.
Given $A\subset B$ and $x\in B$, use the notation $x\leq A$ to denote $\forall a\in A[x\leq a]$. Working in $\mathfrak{M}[G]$, find a subset $A\subset G$ such that $A$ is unbounded in $G$, that is $\forall x\in B[x\leq A\to x\notin G]$ (e.g. by induction or taking $A$ to be a maximal chain in $G$). Let $\check{A}$ be the $B$-name of $A$ and $\check{G}$ be the $B$-name of $G$. Then by forcing theorem, $\mathfrak{M}[G]\vDash A\subset G$ if and only if there exists a $p\in G$ such that $p\Vdash \check{A}\subset \check{G}$.
Since it is not possible that $p\leq A$, hence $p\nleq A$ that means there exists $a\in A$ such that $(p\land a)<p$ and thus $((\neg a)\land p)>0$. But now $((\neg a)\land p)<p$ and thus $((\neg a)\land p) \Vdash \check{A}\subset \check{G}$ although $((\neg a)\land p)\notin G$.
So here for example we should have a formula that depended on a certain fixed $G$, true in $\mathfrak{M}[G]$, and is forced true also by $p\notin G$ and this does not cause contradiction.
I don't understand if there is a mistake in my example or if the situation in the proof of Fremlin (and Malliaris-Shelah) is a different context so things behave differently from the example, and why. Can someone give me a hint?
In particular, to me the context in Fremlin's (Malliaris-Shelah's) proof seems closely related to the previous example for the following reason:
Define $D_{\eta,\varepsilon}=\{n\in\omega:(p_{\eta})_n<(p_{\varepsilon})_n\}$, and $A=\{D_{\eta,\varepsilon}:\eta<\varepsilon<\alpha\}$ (they depend on the starting sequence). To ask that $\langle \dot{p}_\varepsilon\rangle_{\varepsilon<\alpha}$ is an increasing sequence in $\prod_{n\in\omega} \dot{P}_n|G$ means to ask $A\subset G$. If I understood correctly, if $E_\varepsilon$ are the sets defined in the proof by contradiction of Fremlin, we have $E_\eta\setminus E_\varepsilon$ finite for every $\varepsilon<\eta<\alpha$ if and only if $A$ is not unbounded in $G$ and $C$ (defined in Fremlin) is a bound for $A$. I cannot see why for any starting sequence $\langle \dot{p}_\varepsilon\rangle_{\varepsilon<\alpha}$ is impossible for such an $A$ to be unbounded in $G$. I know this would be trivial if $A\in\mathfrak{M}$, but this should not be always the case if I'm not wrong.
EDIT: For Malliaris-Shelah notation, the problem is the following: at the end of Claim 14.7, it is said that $Y_\beta\subseteq^\ast Y_\alpha$ for every $\alpha<\beta$. The argument is that otherwise that would be $B'\subseteq^\ast B$ contradicting $B\Vdash_\mathcal{Q}(\mathcal{N}\vDash "f_\alpha/G\trianglelefteq f_\beta/G")$. I don't get why such a $B'$ should contradict that statement: if $B'\in G$ this would cause contradiction. But I cannot figure out why this should be so.
The translation "Malliaris-Shelah$\to$Fremlin" should be the following: $B$ is $C$, $B'$ is $D$, $Y_\beta$ is $E_\beta$, $f_\beta/G$ is $\dot{p}_\beta$ and $\langle f_\alpha/G:\alpha<\theta\rangle$ is $\langle \dot{p}_\varepsilon\rangle_{\varepsilon<\alpha}$, while the definable downward closed subtree of $({\omega}^{<\omega})$ in which Malliaris and Shelah are working has been replaced by $\prod_{n\in\omega} \dot{P}_n|G$ and $s_n$ intuitively should be $\dot{P}_n$.