The Ultrafilter Lemma and BPI are not theorems of ZF

By F1, $T$ is consistent. Suppose for contradiction that $\mathrm{Z}\mathrm{F}⊢\mathrm{B}\mathrm{P}\mathrm{I}$. Because every axiom of ZF is an axiom of $T$, the same finite derivation is a $T$-derivation of BPI. But $\mathrm{\neg }\mathrm{B}\mathrm{P}\mathrm{I}$ is an axiom of $T$, so $T$ would be inconsistent, contradicting F1. Thus $\mathrm{Z}\mathrm{F}⊬\mathrm{B}\mathrm{P}\mathrm{I}$.

Suppose instead that $\mathrm{Z}\mathrm{F}⊢\mathrm{U}\mathrm{F}\mathrm{L}$. The UFL-to-BPI implication in F2 is itself a ZF theorem, so concatenating the two finite proofs would give $\mathrm{Z}\mathrm{F}⊢\mathrm{B}\mathrm{P}\mathrm{I}$, contradicting step 1.1. Hence $\mathrm{Z}\mathrm{F}⊬\mathrm{U}\mathrm{F}\mathrm{L}$.

Both nonprovability conclusions use the stated consistency hypothesis. They are syntactic consequences of a consistent countertheory; no completeness theorem, countable transitive model, or assertion of absolute truth is used.