# Singleton of Bottom is Ideal

Jump to navigation
Jump to search

## 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 set.

$\Box$

Thus by definition:

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

$\blacksquare$

## Sources

- Mizar article WAYBEL_4:21