Generic Boolean filters select ground-model joins

Every element of $\mathbb{B}$ and each of its Boolean operation values lies in $M$, by transitivity. The operation tables and their finite identities agree internally and externally. Since $G$ is nonempty and upward closed, $1\in G$; by its domain $0\mathrm{\notin }G$. If $a,b\in G$, F2 gives a nonzero $r\in G$ below both. The Boolean meet bounds $r$ above and is nonzero, so $a\wedge b\in G$. Thus $G$ is a proper Boolean filter.

Let $A\in M$ be a subset of $\mathbb{B}$ and set $a=\bigvee {}^{M}A$. This is also the least upper bound among the actual elements of $\mathbb{B}$: every candidate upper bound lies in $M$ and the bounding relation quantifies only over the identical sets $A$ and $\mathbb{B}$. Put $D=\{p\mathrm{\ne }0:p\le \mathrm{\neg }a\text{ or }\mathrm{\exists }b\in A(p\le b)\}$, a set in $M$. To prove density, fix $p\mathrm{\ne }0$. If $p\wedge a=0$, then $p\le \mathrm{\neg }a$. If $p\wedge a\mathrm{\ne }0$, some $b\in A$ satisfies $p\wedge b\mathrm{\ne }0$: otherwise every $b\le \mathrm{\neg }p$, making $a\le \mathrm{\neg }p$ by leastness and contradicting this case. The nonzero meet $p\wedge b$ extends $p$ into $D$. Thus $D$ is dense.

Fix $b\in \mathbb{B}$. The set $D_b=\{p\mathrm{\ne }0:p\le b\text{ or }p\le \mathrm{\neg }b\}$ belongs to $M$ by Separation. It is dense: if $p\wedge b\mathrm{\ne }0$, this meet extends $p$ into $D_b$; otherwise distributivity gives $p\le \mathrm{\neg }b$. F1 makes $G$ meet $D_b$, and upward closure implies $b\in G$ or $\mathrm{\neg }b\in G$. Both cannot hold, since their meet is zero. Hence $G$ decides every element and is a proper ultrafilter.

If $a\in G$, meet $D$ using F1. A member of $G$ below $\mathrm{\neg }a$ would contradict properness, so the meeting condition lies below some $b\in A$ and upward closure gives $b\in G$. Conversely $b\in A\cap G$ and $b\le a$ imply $a\in G$. This proves both join directions. If $A=\mathrm{\varnothing }$, $a=0\mathrm{\notin }G$ and $A\cap G=\mathrm{\varnothing }$, as required.

Put $d=\bigwedge {}^{M}A=\mathrm{\neg }\bigvee {}^M\{\mathrm{\neg }b:b\in A\}$. The complemented family belongs to $M$ by Replacement. If $d\in G$, every $b\in A$ is above $d$, so $A\subseteq G$. Conversely suppose $A\subseteq G$ but $d\mathrm{\notin }G$. Step 2.1 puts $\mathrm{\neg }d$ in $G$, and step 2.2 gives some $b\in A$ with $\mathrm{\neg }b\in G$, contradicting $b\in G$. For empty $A$ this says $1\in G$; for singleton $A$ the equivalence is immediate. The only family to which join selection was applied is a member of $M$, so this proves no assertion for arbitrary external subsets of $G$. Every witness was used individually in an existence proof; no family of witnesses was selected.