Inverse Image under Order Embedding of Strict Upper Closure of Image of Point

Theorem

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

Let $\phi: S \to T$ be an order embedding of $\struct {S, \preceq}$ into $\struct {T, \preceq'}$

Let $p \in S$.

Then:

$\map {\phi^{-1} } {\map \phi p^{\succ'} } = p^\succ$

where $\cdot^\succ$ and $\cdot^{\succ'}$ represent strict upper closure with respect to $\preceq$ and $\preceq'$, respectively.

Proof

Let $x \in \map {\phi^{-1} } {\map \phi p^{\succ'} }$.

By the definition of inverse image:

$\map \phi x \in \map \phi p^{\succ'}$

By the definition of strict upper closure:

$\map \phi p \prec' \map \phi x$

Since $\phi$ is an order embedding:

$p \prec x$

Thus by the definition of strict upper closure:

$x \in p^\succ$

and so:

$\map {\phi^{-1} } {\map \phi p^{\succ'} } \subseteq p^\succ$

Let $x \in p^\succ$.

By the definition of strict upper closure:

$p \prec x$

Since $\phi$ is an order embedding:

$\map \phi p \prec' \map \phi x$

Thus by the definition of strict upper closure:

$\map \phi x \in \map \phi p^{\succ'}$

Thus by the definition of inverse image:

$x \in \map {\phi^{-1} } {\map \phi p^{\succ'} }$

and so:

$p^\succ \subseteq \map {\phi^{-1} } {\map \phi p^{\succ'} }$

Thus by definition of set equality:

$\map {\phi^{-1} } {\map \phi p^{\succ'} } = p^\succ$

$\blacksquare$