Extending Operation is a Strictly Progressing Mapping

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $S$ denote the class of all ordinal sequences.

Let $E: S \to S$ be an extending operation on $S$.


Then $E$ is a strictly progressing mapping.


Proof

Let $\theta \in S$ be an $\alpha$-sequence.

By definition of extending operation:

$\map E \theta = \theta \cup \tuple {\alpha, x}$

where $x$ is arbitrary.

From Extending Operation is a Slowly Progressing Mapping we have a fortiori that $E$ is a progressing mapping.

By definition of $\alpha$-sequence:

$\alpha \notin \Dom \theta$

and so:

$\tuple {\alpha, x} \notin \theta$

Hence:

$\theta \subsetneqq \map E \theta$

demonstrating that $E$ is a strictly progressing mapping.

$\blacksquare$


Sources