Subset and Image Admit Suprema and Mapping is Increasing implies Supremum of Image Precedes Mapping at Supremum

Theorem

Let $\struct {S, \preceq}$, $\struct {T, \precsim}$ be ordered sets.

Let $f: S \to T$ be a increasing mapping.

Let $D \subseteq S$ such that

$D$ admits a supremum in $S$ and $f \sqbrk D$ admits a supremum in $T$.

Then:

$\map \sup {f \sqbrk D} \precsim \map f {\sup D}$

Proof

By definition of supremum:

$\sup D$ is upper bound for $D$.

By Increasing Mapping Preserves Upper Bounds:

$\map f {\sup D}$ is upper bound for $f \sqbrk D$.

Thus by definition of supremum:

$\map \sup {f \sqbrk D} \precsim \map f {\sup D}$

$\blacksquare$

Sources

• Mizar article WAYBEL17:15