Set of Finite Suprema is Directed

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\struct {S, \vee, \preceq}$ be a join semilattice.

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


Then

$\set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$ is directed.

where $\map {\operatorname {Fin} } X$ denotes the set of all finite subsets of $X$.


Proof

By Existence of Non-Empty Finite Suprema in Join Semilattice:

for every $A \in \map {\operatorname {Fin} } S$ if $A \ne \O$, then $A$ admits a supremum.

By definition of non-empty set:

$\exists a: a \in X$

By definitions of subset and singleton:

$\set x \subseteq X$

By Singleton is Finite:

$\set x$ is finite

By definitions of non-empty set and singleton:

$\set x \ne \O$

By definition of $\operatorname {Fin}$:

$\sup {\set x} \in \set {\sup A: A \in \map {\operatorname{Fin} } X \land A \ne \O}$

Thus by definition:

$\set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$ is a non-empty set.

Let $x, y \in \set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$

Then

$\exists A \in \map {\operatorname {Fin} } X: x = \sup A$ and $A \ne \O$

and

$\exists B \in \map {\operatorname {Fin} } X: y = \sup B$ and $B \ne \O$

By Finite Union of Finite Sets is Finite:

$A \cup B$ is finite

By Union of Subsets is Subset:

$A \cup B \subseteq X$

By definitions of non-empty set and union:

$A \cup B \ne \O$

By definition of $\operatorname {Fin}$:

$\map \sup {A \cup B} \in \set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$

By Set is Subset of Union:

$A \subseteq A \cup B$ and $B \subseteq A \cup B$

Thus by Supremum of Subset:

$x \preceq \map \sup {A \cup B}$ and $y \preceq \map \sup {A \cup B}$

Thus by definition:

$\set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$ is directed.

$\blacksquare$


Sources