Any nonempty subset of a directed-complete partial order $(X,\leq)$ has a supremum if $X$ is a join-semilattice?

26 Views Asked by At

Let $(X,\leq)$ be a directed-complete partial order (dcpo), and let $W$ be a nonempty subset of $X$.

Suppose that $(X,\leq)$ is also a join-semilattice. Then the join $\vee A$ of any nonempty, finite subset $A$ of $W$ exists. Let \begin{equation*} U = \{\vee A:A\text{ is a nonempty, finite subset of }W\}. \end{equation*} Then $U$ is an upward directed subset of $X$, and as $X$ is a dcpo it follows that $U$ has a supremum $\vee U$.

Since $W$ is a subset of $U$, any upper bound of $U$ is an upper bound of $W$.

Conversely, if $x$ is an upper bound of $W$ then it is an upper bound of any nonempty, finite subset $A$ of $W$, and so it is an upper bound of $U$.

It follows that $W$ has a supremum, and it equals $\vee U$.

Is my reasoning correct? Thanks!