Finite Suprema Set and Lower Closure is Ideal

Theorem

Let $P = \left({S, \vee, \preceq}\right)$ be a join semilattice.

Let $X$ be a non-empty subset of $S$.

Then

${\operatorname{finsups}\left({X}\right)}^\preceq$ is ideal in $P$.

where

$\operatorname{finsups}\left({X}\right)$ denotes the finite suprema set of $X$,
$X^\preceq$ denotes the lower closure of $X$.

Proof

$X \subseteq {\operatorname{finsups}\left({X}\right)}^\preceq$

By definition of non-empty set:

${\operatorname{finsups}\left({X}\right)}^\preceq$ is a non-empty set.

We will prove that

$\operatorname{finsups}\left({X}\right)$ is directed.

Let $x, y \in \operatorname{fininfs}\left({X}\right)$

By definition of finite suprema set:

$\exists A \in \mathit{Fin}\left({X}\right): x = \sup A \land A$ admits a supremum

and

$\exists B \in \mathit{Fin}\left({X}\right): y = \sup B \land B$ admits an supremum

where $\mathit{Fin}\left({X}\right)$ denotes the set of all finite subsets of $X$.

Define $C = A \cup B$.

$C \subseteq X$
$C$ is finite.

Then

$C \in \mathit{Fin}\left({X}\right)$
$C \ne \varnothing \implies C$ admits a supremum.
$C = \varnothing \implies A = \varnothing$

So

$C$ admits a supremum.

By definition of finite suprema set:

$\sup C \in \operatorname{finsups}\left({X}\right)$
$A \subseteq C$ and $B \subseteq C$

Thus by Supremum of Subset:

$x \preceq \sup C$ and $y \preceq \sup C$

Hence $\operatorname{finsups}\left({X}\right)$ is directed.

$\Box$

${\operatorname{finsups}\left({X}\right)}^\preceq$ is directed.
${\operatorname{finsups}\left({X}\right)}^\preceq$ is lower.

Hence ${\operatorname{finsups}\left({X}\right)}^\preceq$ is ideal in $P$.

$\blacksquare$