Successor set

Set

context $X$
definiendum $ {\mathrm{succ}}\ X \equiv X \cup \{X\} $

Discussion

Theorems

$ X\in {\mathrm{succ}}\ X $
$ ({\mathrm{succ}}\ X={\mathrm{succ}}\ Y)\Rightarrow (X=Y) $
$ (Y\in {\mathrm{succ}}\ X)\Leftrightarrow (Y=X\lor Y=\{X\}) $
$ X\neq {\mathrm{succ}}\ X $

Reference

Wikipedia: Successor ordinal

ProofWiki: Successor set

Parents

Requirements

Singleton, Union