Singleton of Bottom is Ideal

Theorem

Let $\struct {S, \preceq}$ be a bounded below ordered set.

Then

$\set \bot$ is an ideal in $\struct {S, \preceq}$

where $\bot$ denotes the smallest element in $S$.

Proof

Non-empty

By definition of singleton:

$\bot \in \set \bot$

By definition:

$\set \bot$ is a non-empty set.

$\Box$

Directed

Thus by Singleton is Directed and Filtered Subset:

$\set \bot$ is directed.

$\Box$

Lower

Let $x \in \set \bot, y \in S$ such that

$y \preceq x$

By definition of singleton:

$x = \bot$

By definition of smallest element:

$\bot \preceq y$

By definition of antisymmetry:

$y = \bot$

Thus by definition of singleton:

$y \in \set \bot$

Thus by definition:

$\set \bot$ is a lower section.

$\Box$

Thus by definition:

$\set \bot$ is an ideal in $\struct {S, \preceq}$

$\blacksquare$

Sources

• Mizar article WAYBEL_4:21