A description/proof of that ordinal number is limit ordinal number iff it is nonzero and is union of its all members
Topics
About: set
The table of contents of this article
Starting Context
Target Context
- The reader will have a description and a proof of the proposition that any ordinal number is a limit ordinal number if and only if it is nonzero and is the union of its all the members.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Description
For any ordinal number, \(o\), \(o\) is a limit ordinal number if and only if \(o \neq 0\) and \(o = \cup_{o' \in o} o'\).
2: Proof
Let us suppose that \(o \neq 0\) and \(o = \cup_{o' \in o} o'\).
If \(o\) was a successor ordinal number, \(o = o''^+\), \(o'' \in o\) and \(o'' \subset o\) by the proposition that the inclusion relation is equivalent with the membership relation for the ordinal numbers collection. For any \(o' \in o\), \(o' = o''\) or \(o' \in o''\) as \(o''\) is the largest smaller than \(o\). So, by the proposition that the inclusion relation is equivalent with the membership relation for the ordinal numbers collection, \(o' \subseteq o'' \subset o\). So, \(\cup_{o' \in o} o' \subset o\), a contradiction. So, \(o\) is a limit ordinal number.
Let us suppose that \(o\) is a limit ordinal number.
For any \(o' \in o\), by the proposition that the inclusion relation is equivalent with the membership relation for the ordinal numbers collection, \(o' \subset o\), so, \(\cup_{o' \in o} o' \subseteq o\). For any \(o'' \in o\), \(o''^+ \in o\), because \(o'' \in o''^+\), \(o''^+ \neq o\), and \(\lnot o'' \in o \in o''^+\). So, \(o'' \in \cup_{o' \in o} o'\), because \(o'' \in o''^+\) while \(o''^+\) is an \(o'\). So, \(o \subseteq \cup_{o' \in o} o'\). So, \(o = \cup_{o' \in o} o'\).
3: Note
If \(o = 0\), \(o = \cup_{o' \in o} o'\), because there is no \(o'\), and the union is supposed to be the empty set in that case, while \(0\) is the empty set. So, the nonzero-ness condition is required.
