The Prikry property

For each $n<\omega$ and $t\in [A{]}^n$, listed increasingly, colour $t$ by $0$ if some upper part $B_t$ makes $(s^{⌢}t,B_t)$ a condition forcing $\phi$, by $1$ if some such condition forces $\mathrm{\neg }\phi$, and by $2$ if neither exists. Colours $0$ and $1$ cannot both apply: two witnesses have the same stem, so F1 gives a common extension, while persistence would make that extension force both alternatives. By F2, shrink $A$ to one $A^{\mathrm{\prime }}\in U$ on which every arity-colouring is constant, and set $q=(s,A^{\mathrm{\prime }}){\le }^{\ast }p$.

Decision density below $q$ gives a condition $r\le q$ deciding $\phi$. Let $n$ be the number of entries which the stem of $r$ adds after $s$, and let $t$ be that increasing $n$-tuple. Then $t\in [A^{\mathrm{\prime }}{]}^n$ and its colour is $0$ or $1$, according to the decision made by $r$; it is not $2$. Write $\epsilon \in \{0,1\}$ for this homogeneous colour at arity $n$.

For every $m<\omega$, the homogeneous colour at arity $n+m$ is also $\epsilon$. Indeed, start with a witness at $t$ having colour $\epsilon$ and choose $m$ further increasing points from its measure-one upper part intersected with $A^{\mathrm{\prime }}$; strengthening by those points preserves its decision, so the resulting $(n+m)$-tuple has colour $\epsilon$. Homogeneity at that arity gives the claim, including $m=0$. Only finite selection is made here; the arbitrary simultaneous measure-one choices occurred inside F2 and are the precise AC use propagated from The Axiom of Choice.

Let $a\le q$ be arbitrary and let $m$ be the number of its new stem entries after $s$. Extend that stem by $n$ points from its upper part. Its resulting $(m+n)$-tuple has colour $\epsilon$ by step 3.1, so a same-stem witness forces the corresponding alternative. Intersecting the two upper parts as in F1 gives a common strengthening of $a$ which forces that alternative. Thus that alternative is dense below $q$, and F3 implies that $q$ itself forces it. Hence $q$ decides $\phi$ without changing the stem of $p$. [F1, F3, step 3.1] $\mathrm{\square }$