Recall that *Mathias forcing* is the poset $\mathbb{M}$ whose elements are pairs $(s,A)$, where $s$ is a finite subset of $\omega$, $A$ an infinite subset of $\omega$, and $\max(s)<\min(A)$. Extension is defined by $(s,A)\leq(t,B)$ if and only if $s\supseteq t$, $A\subseteq B$ and $s\setminus t\subset B$. If $U$ is an ultrafilter, then one can define *Mathias forcing* relative to $U$, $\mathbb{M}_U$, likewise by ensuring that the side condition $A\in U$.

By a *Mathias real* over $M$, I mean an infinite $x\subset\omega$ such that $x=\bigcup\{s:(s,A)\in G\}$, where $G$ is $M$-generic for $\mathbb{M}$.

I have a question about the proof of the following theorem, 26.35 in Jech's Set Theory:

Theorem (Mathias): Let $M$ be a transitive model of ZFC. An infinite set $x\subset\omega$ is a Mathias real over $M$ if and only if for every maximal almost disjoint family $\mathcal{A}\in M$ of subsets of $\omega$, there exists an $X\in\mathcal{A}$ such that $x\setminus X$ is finite.

The forward direction is an easy density argument. For the converse, fix $D\in M$ a dense open subset of $\mathbb{M}$. Given $s$, we say that an infinite set $X\subset\omega$ *captures* $(s,D)$ if $\max(s)<\min(X)$ and for every infinite $Y\subset X$, there is an initial segment $t$ of $Y$ such that $(s\cup t,X\setminus|t|)\in D$, where $|t|=\sup\{n+1:n\in t\}$.

A key lemma to proving the above theorem is:

Lemma: For every infinite set $A\subset\omega$ and finite $s\subset\omega$, there exists an infinite set $X\subset A\setminus|s|$ such that $X$ captures $(s,D)$.

The proof proceeds by constructing a sequence $Y_0\supset Y_1\supset\cdots$ of infinite sets, and $m_0<m_1<\cdots$, with $m_n=\min(Y_n)$ as follows:

Let $Y_0=A\setminus|s|$. For the inductive case, the proof claims that given $Y_n$, we can find $Y_{n+1}\subset Y_n\setminus\{m_n\}$ such that for any $t\subset\{m_0,\ldots,m_n\}$, if there exists $Y\subset Y_n$ such that $(s\cup t,Y)\in D$, then $(s\cup t,Y_{n+1})\in D$.

This I do not see. In the case of the analogous claim for $\mathbb{M}_U$, where $U$ is a Ramsey ultrafilter (as in section 2 of Mathias' *Happy Families* paper), one can do this, because the witnesses $Y$ for $(s\cup t,Y)\in D$, will have $U$-large intersection, and $D$ is open. However, for $\mathbb{M}$, isn't it possible that there are $t_0,t_1\subset\{m_0,\ldots,m_n\}$ with $(s\cup t_0,Y),(s\cup t_1,Y')\in D$ for some $Y,Y'\subset Y_n$, but so that the only such witnesses are (almost) disjoint?

Edit: For context, here is how the rest of the proof of the lemma proceeds. Once we have such a sequence of $Y_n$ and $m_n$, let $Y=\{m_n:n\in\omega\}$. Let $O=\bigcup\{[t,S]^\omega:(t,S)\in D\}$, where $[t,S]^\omega=\{X\in[\omega]^\omega:t\subset X \land X\setminus|t|\subset S\}$. This is a dense open set in the Ellentuck topology (hence, its complement is *Ramsey null*), thus there is an infinite $X\subset Y$ such that $[s,X]^\omega\subset O$. We claim that $X$ captures $(s,D)$. Let $Z\subset X$ be infinite, then $s\cup Z\in O$, so there is an initial segment $t$ of $Z$ and infinite $S\subset\omega$ such that $(s\cup t,S)\in D$, and $s\cup Z\in[s\cup t,S]^\omega$. Since $D$ is open in $\mathbb{M}$, it follows that $(s\cup t,Z\setminus|t|)\in D$, and if $\max(t)=m_n$, then $Z\setminus|t|$ is an infinite subset of $Y_n$, and so, by the claimed choice of $Y_{n+1}$, we have that $(s\cup t,Y_{n+1})\in D$. $X\setminus|t|\subset Y_{n+1}$, so it follows that $(s\cup t,X\setminus|t|)\in D$, as desired.

Edit: The question seems to have been answered by Francois Dorais in the comments.