Preceding implies Image is Subset of Image

Theorem

Let $\struct {S, \precsim}$ be a preordered set.

Let $x, y \in S$ such that

$x \precsim y$

Then $\map \precsim y \subseteq \mathord {\map \precsim x}$

where $\map \precsim y$ denotes the image of $y$ under $\precsim$.

Proof

Let $z \in \mathord {\map \precsim y}$

By definition of image of element:

$y \precsim z$

By definition of transitivity:

$x \precsim z$

Thus by definition of image of element:

$z \in \mathord {\map \precsim x}$

$\blacksquare$

Sources

• Mizar article WAYBEL_0:22