A supported Boolean algebra has an ideal maximal in its supported-definability class

Let $\mathcal{D}$ be the set of all proper ideals $J\subseteq B$ which are ordinal-definable from $A,f$. This is a set by Separation from $\mathcal{P}(B)$, because existence of a rank, formula code, and finite ordinal tuple giving a unique definition is the first-order property in F2. It is nonempty: nontriviality makes $\{0_B\}$ a proper ideal, and $0_B$ is uniquely definable from the supported algebra $B$. Assign to each member of $\mathcal{D}$ its unique least code in the rank–formula–fixed-arity tuple order of F2. Replacement makes the range a set; restriction of that setlike class order well-orders the range and therefore well-orders $\mathcal{D}$. Enumerate its order type as $⟨J_{\xi }:\xi <\theta ⟩$.

By F3 define an increasing sequence $⟨I_{\xi }:\xi \le \theta ⟩$. Put $I_0=\{0_B\}$. Given $I_{\xi }$, set

We prove by transfinite induction that every $I_{\xi }$ is a proper ideal and that $I_{\eta }\subseteq I_{\xi }$ for $\eta <\xi$. The initial ideal is proper by nontriviality. [F1, step 1.2, base] At a successor, either the value is unchanged or it is the proper ideal $J_{\xi }$ containing the preceding value. At a limit, the union of an increasing chain of ideals contains $0_B$, is downward closed, and is closed under binary joins because any two of its elements already occur together at some later one of their two stages. If $1_B$ belonged to the union, it would belong to one earlier $I_{\xi }$, contradicting that stage's propriety.

Put $I=I_{\theta }$. The recursion and its input well-order are uniquely definable from $A,f$ and the fixed definition of $B$, so F2 and F3 make $I$ ordinal-definable from $A,f$. Step 2.1 makes it a proper ideal. Moreover $\mathrm{TC}(I)\subseteq \{I\}\cup \mathrm{TC}(B)$ because $I\subseteq B$. The set $I$ has the displayed supported definition, while every descendant in $\mathrm{TC}(B)$ has the hereditary definability required by $B\in C$. The parameter-HOD convention in the Statement therefore gives $I\in C$ directly; no theorem about ordinary parameter-free HOD is being substituted.

Suppose $J\in \mathcal{D}$ and $I\subseteq J$. Write $J=J_{\beta }$. Since $I_{\beta }\subseteq I\subseteq J_{\beta }$, the successor rule gives $I_{\beta +1}=J_{\beta }$. Monotonicity then gives $J\subseteq I$, and hence $J=I$. This proves the asserted maximality within $\mathcal{D}$. It neither applies Zorn's lemma nor chooses a maximal member of an arbitrary partially ordered set; every stage is forced by a fixed definable well-order and a yes-or-no inclusion test, as F4 permits.