Sealing a named maximal antichain

First distinguish the two objects. For a ground condition $p$, a set $B\subseteq T_p$ is already a ground antichain and its membership is settled. By contrast, $\dot{A}$ is a name for a subset of the eventual union: $p_0$ need not decide its members, and its value need not be contained in $T_{p_0}$. Maximality of $\dot{A}$ says that every node of $\dot{T}$ is comparable with some named member, not that the intersection $\dot{A}\cap {\check{T}}_{p_0}$ is already maximal in $T_{p_0}$.

Put $p_0^{\ast }=r_0$. At outer round $n$, enumerate the countable tree $T_{p_n^{\ast }}$ as $(t_{n,m}{)}_{m<\omega }$. Starting with $p_{n,0}=p_n^{\ast }$, construct a descending sequence. Because $p_{n,m}$ still forces $\dot{A}$ maximal, it forces that some member of $\dot{A}$ is comparable with $t_{n,m}$. The existential forcing clause from [F7], dense decision from [F5], and [F4] let us strengthen to $p_{n,m+1}$ and decide such a member as a ground countable sequence $a_{n,m}$. The atomic clause [F6] permits a further strengthening whose tree actually contains $a_{n,m}$. Thus $p_{n,m+1}⊩{\check{a}}_{n,m}\in \dot{A}\text{ and }{\check{a}}_{n,m}\parallel {\check{t}}_{n,m}\mathrm{.}$ Countable closure gives a lower bound ${\bar{p}}_n$ for the inner sequence. Strengthen once more to $p_{n+1}^{\ast }\le {\bar{p}}_n$ with strictly larger top height. Use [F9] and [A1] for all $n,m<\omega$.

Let $U={\bigcup }_{n<\omega }{T}_{p_n^{\ast }},A^{\ast }=\{a_{n,m}:n,m<\omega \}\mathrm{.}$ The strictly increasing top heights make $U$ a normal splitting tree of nonzero countable limit height; $U$ itself has no top and is not yet a forcing condition. It is countable by [F8]. Every $t\in U$ lies in some $T_{p_n^{\ast }}$ and appears in that round's enumeration, so it is comparable with the corresponding $a_{n,m}\in A^{\ast }$. If two distinct elements of $A^{\ast }$ were comparable, a sufficiently late condition would contain them both and, by persistence in [F5], force both into the antichain $\dot{A}$, a contradiction. Hence $A^{\ast }$ is an antichain and the preceding coverage makes it maximal in $U$. Repeated decisions may yield the same $a_{n,m}$; set formation removes repetitions.

Apply [F3] to $(U,A^{\ast })$. Choose a countable covering family of cofinal branches of $U$, each meeting $A^{\ast }$, and add one distinct top node for each distinct branch. The result is a countable normal splitting tree $T_q$ with a genuine new top, hence a condition $q$. It end extends every fusion condition, so $q\le r_0$, and persistence gives $q⊩{\check{A}}^{\ast }\subseteq \dot{A}\mathrm{.}$ Every node of $T_q$ is comparable with a member of $A^{\ast }$, including each new top by construction.

Let $s\le q$. Literal end extension [F2] preserves $T_q$. Any node of $T_s$ already in $T_q$ is comparable with $A^{\ast }$ by step 4.1. Any new node has a unique predecessor on the top level of $T_q$; that top extends a member of $A^{\ast }$, so the new node does too. Thus every future node remains comparable with $A^{\ast }$, and density plus [F5] gives $q⊩{\check{A}}^{\ast }\text{ is maximal in }\dot{T}\mathrm{.}$ Since $q$ also forces that $\dot{A}$ is an antichain containing $A^{\ast }$, no distinct member can be added to $A^{\ast }$; therefore $q⊩\dot{A}={\check{A}}^{\ast }$.

The root handles a starting tree with only one node and shows that the forced maximal antichain cannot be empty. The indices $n=m=0$ give the first actual decision; zero outer rounds would not cover even the starting tree and are not used. The omega-union deliberately loses a top, and step 4.1 restores one. Empty or repeated branch/decision lists are not silently counted as new nodes: repetitions are removed, while nonemptiness follows from the root comparison. All names and assertions remain inside the forcing relation of [F7]; no universe-generic is claimed. Choice is spent in [A1] on the evolving tree enumerations and deciding extensions and through [F8], while the ground sealing operation [F3] itself is choice-free.