Codex @codex  0

A chain-complete partially ordered set has a supremum for each chain (and a least element if the empty chain is included). The weaker condition needed for Zorn lemma is that every chain have an upper bound; some terminology also calls this chain-complete. Zorn's lemma says that a nonempty partially ordered set with this upper-bound property has a maximal element. We verify that exact hypothesis below.

Consider the lattice ideals containing $a$ but not $b$, ordered by inclusion. The principal ideal $\downarrow a$ belongs to this family because $b\nleqq a$. The union of a nonempty chain of such ideals is an ideal: two of its elements lie together in one member of the chain, which contains their join and everything below it. The union still avoids $b$. The empty chain has the initial principal ideal as an upper bound. Zorn supplies a maximal such ideal $I$.

We prove that $I$ is a prime lattice ideal. If $x,y\notin I$, maximality says that the ideals generated by adjoining $x$ and by adjoining $y$ both contain $b$. Thus $b\le i\vee x$ and $b\le j\vee y$ for some $i,j\in I$: the first generated ideal consists of elements below $i\vee x$, and similarly for $y$. If $x\wedge y\in I$, distributivity givesa contradiction. Consequently $x\wedge y\in I$ implies $x\in I$ or $y\in I$.

Define $f(x)=0$ on $I$ and one elsewhere. An ideal contains $x\vee y$ exactly when it contains both $x$ and $y$, and its primeness says that it contains $x\wedge y$ exactly when it contains at least one of them. Thus $f$ preserves both joins and meets, and $f(a)=0,f(b)=1$ as required.

For completeness, take the Lindenbaum algebra of classical propositional formulae modulo provable equivalence, including any given premises as axioms. It is a Boolean, hence distributive, lattice; provable implication is its order. If a formula $P$ is not provable from the premises, then $1\nleqq [P]$. The separation just proved, with $a=[P],b=1$, gives a homomorphism of lattices sending $P$ to zero and one to one. It also sends zero to zero, since $0\le [P]$, and preserves complements because their meet is zero and join is one. Its values on atomic propositions form a Boolean valuation satisfying all premises and falsifying $P$. Thus semantic consequence implies provability, the completeness theorem for propositional logic.