Up-Complete Product/Lemma 2

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\left({S, \preceq_1}\right)$, $\left({T, \preceq_2}\right)$ be non-empty ordered sets.

Let $\left({S \times T, \preceq}\right)$ be Cartesian product of $\left({S, \preceq_1}\right)$ and $\left({T, \preceq_2}\right)$.


Let $X$ be a directed subset of $S \times T$.

Then

$\operatorname{pr}_1^\to\left({X}\right)$ and $\operatorname{pr}_2^\to\left({X}\right)$ are directed

where

$\operatorname{pr}_1$ denotes the first projection on $S \times T$
$\operatorname{pr}_2$ denotes the second projection on $S \times T$
$\operatorname{pr}_1^\to\left({X}\right)$ denotes the image of $X$ under $\operatorname{pr}_1$


Proof

Let $x, y \in \operatorname{pr}_1^\to\left({X}\right)$.

By definitions of image of set and projections:

$\exists x' \in T: \left({x, x'}\right) \in X$

and

$\exists y' \in T: \left({y, y'}\right) \in X$

By definition of directed:

$\exists \left({a, b}\right) \in X: \left({x, x'}\right) \preceq \left({a, b}\right) \land \left({y, y'}\right) \preceq \left({a, b}\right)$

By definition of Cartesian product of ordered sets:

$\exists a \in \operatorname{pr}_1^\to\left({X}\right): x \preceq_1 a \land y \preceq_1 a$

Thus by definition

$\operatorname{pr}_1^\to\left({X}\right)$ is directed.

By mutatis mutandis:

$\operatorname{pr}_2^\to\left({X}\right)$ is directed.

$\blacksquare$


Sources