The adjoint functor theorem for ordered sets

For each $a\in A$, let $S_a=\{b\in B:a\le g(b)\}$. It is nonempty: because $g$ preserves the empty meet, $g({\mathrm{\top }}_B)={\mathrm{\top }}_A$, so $a\le g({\mathrm{\top }}_B)$. Completeness [L3] therefore supplies $f(a)=\bigwedge S_a$.

If $a\le a^{\mathrm{\prime }}$, then $S_{a^{\mathrm{\prime }}}\subseteq S_a$, so $\bigwedge S_a\le \bigwedge S_{a^{\mathrm{\prime }}}$. Hence $f$ is monotone and therefore a functor under [L1].

If $a\le g(b)$, then $b\in S_a$, so $f(a)=\bigwedge S_a\le b$.

Conversely, since $g$ preserves the meet of $S_a$, one has $g(f(a))={\bigwedge }_{c\in S_a}g(c)$. Every $g(c)$ on the right lies above $a$, hence $a\le g(f(a))$. Thus $f(a)\le b$ implies $a\le g(f(a))\le g(b)$ by monotonicity.

Steps 2.2 and 2.3 give the equivalence in [L2] for every $a,b$, so $f⊣g$. The empty-meet case in step 1.1 is what prevents the defining set from being empty.