Diamond implies clubsuit

Fix the ordinal enumerations in F2 using A1. At a nonzero countable limit $\alpha$, if $A_{\alpha }$ is cofinal in $\alpha$, apply the explicit minimum recursion in F2 to it and call its range $C_{\alpha }$. Otherwise apply the same recursion to $\alpha$ itself. In both situations $C_{\alpha }$ is cofinal of order type $\omega$; when $A_{\alpha }$ is cofinal we also have $C_{\alpha }\subseteq A_{\alpha }$. This defines the whole ladder sequence from the fixed parameters.

Let $X\subseteq {\omega }_1$ be uncountable. It is unbounded, since a bounded subset lies inside a countable ordinal and is countable. F5 and A1 give $\mathrm{cf}({\omega }_1)={\omega }_1>\omega$, so F3 makes $E={\mathrm{acc}}_{{\omega }_1}(X)$ club. Let $S=\{\alpha :X\cap \alpha =A_{\alpha }\}$, stationary by F1. For any club $D$, F4 makes $D\cap E$ club, so it meets $S$. Thus $S\cap E$ is stationary.

If $\alpha \in S\cap E$, then $\alpha$ is a nonzero limit and $A_{\alpha }=X\cap \alpha$ is cofinal in $\alpha$. The first alternative of step 1.1 therefore applies, giving $C_{\alpha }\subseteq A_{\alpha }\subseteq X$. Hence the containment-guess set contains the stationary set $S\cap E$ and itself meets every club. This is exactly F2's club principle.