Directed progressive products have club continuous chains

Properness implies $A\mathrm{\ne }\mathrm{\varnothing }$, and the product is nonempty because it contains the zero function. Every $a\in A$ is a limit ordinal, so $v(a)+1<a$ for $v\in \prod A$. If $v$ weakly bounds a family, $v+1$ strictly bounds it, by the coordinate inequality and F1. AC fixes a choice function on the nonempty subsets of the set $\prod A$, hence specifies one bound whenever directedness supplies a nonempty bound set. For every nonzero limit $\delta <\lambda$ also fix a club $E_{\delta }\subseteq \delta$ of order type $\mathrm{cf}(\delta )$: continuously enumerate a cofinal subset from F5, keeping successor values increasing and taking suprema at limits, as authorized by F6. Intermediate suprema stay below $\delta$ by F5; its continuous range is the required club. AC selects the initial cofinal enumerations simultaneously.

Define $f$ by recursion. Set $f_0=0$. At every $0<\delta <\lambda$, the earlier family has size at most $\mathrm{\mid }\delta \mathrm{\mid }<\lambda$; directedness and step 1.1 provide a specified weak bound $b_{\delta }\in \prod A$. At a successor $\delta =\xi +1$ set $f_{\delta }(a)=\max \{b_{\delta }(a),f_{\xi }(a),g_{\xi }(a)\}+1$. At a limit whose cofinality is ${\kappa }^{++}$ for an eligible uncountable regular $\kappa$, set

For every $\xi <\delta <\lambda$, $f_{\xi }{\le }_I{b}_{\delta }{<}_I{f}_{\delta }$; hence F1 gives $f_{\xi }{<}_I{f}_{\delta }$. At successors the explicit maximum gives $g_{\xi }(a)<f_{\xi +1}(a)$ at every coordinate, not just modulo $I$. Fix any eligible $\kappa$. At every $\delta <\lambda$ of cofinality ${\kappa }^{++}$ the special rule was used, and ${\sup }_{\xi \in E_{\delta }}{f}_{\xi }(a)=v_{\delta }(a)<f_{\delta }(a)$ for all $a>{\kappa }^{++}$. The possible failures lie in the assumed $I$-small set of remaining coordinates. This proves precisely the club-continuity premise, with the bound index equal to $\delta$. If $A$ is infinite, F2 gives $(\ast {)}_{\kappa }$. If $A$ is finite, let $S$ be the union of all sets in $I$; this finite union belongs to $I$, and $S\mathrm{\ne }A$. Every strict comparison holds at every $a\mathrm{\notin }S$. Thus the entire chain is strongly increasing with the constant witness $S$, and every unbounded subset of regular $\lambda$ has an order-type-$\kappa$ subset by choosing successive least larger indices, using F5–F6 at limits. Hence $(\ast {)}_{\kappa }$ also holds in the finite case.

Suppose $A$ is infinite and put $\tau =\mathrm{\mid }A\mathrm{\mid }$. For each eligible $\kappa >\tau$, step 3.1 and F3 give the $\kappa$ projection property. If the ${\tau }^{+}$ projection property holds and $\lambda >{\tau }^{+}$, F4 gives the stated exact bound and all its coordinate-cofinality conclusions. In particular, if an eligible $\kappa \ge {\tau }^{+}$ exists, restrict each strong order-type-$\kappa$ subsequence supplied in step 3.1 to its first ${\tau }^{+}$ terms. This proves $(\ast {)}_{{\tau }^{+}}$; ${\tau }^{+}$ is regular by F7, so F3 gives its projection property. Also ${\tau }^{+}\le \kappa <{\kappa }^{++}<\lambda$. Thus every hypothesis of F4 holds. The strict chain and prescribed domination were already proved in step 3.1, with no eligible $\kappa$ needed for that construction. QED.