How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Basic closure properties of ordinals
Statement
Let and be ordinals (Ordinal (von Neumann)). Then:
(a) every element of is an ordinal;
(b) ;
(c) is an ordinal;
(d) if is a nonempty set of ordinals then is an ordinal;
(e) if is any set of ordinals then is an ordinal;
(f) if and only if or ;
(g) any two ordinals are comparable under inclusion: or .
Everything here is a theorem of ZF and uses no choice principle.
Facts & Assumptions
Given: Ordinals , and, where stated, a set all of whose members are ordinals. Claim (g) is not in the usual list of basic facts, but claim (e) needs it, so it is proved here rather than deferred; the trichotomy statement is then read off from it on the next item of this page.
An ordinal is a transitive set on which is a strict well-order: irreflexive, transitive as a relation, trichotomous, and with a least element in every nonempty subset (Ordinal (von Neumann)).
The restriction of a strict well-order to a subset is again a strict well-order, since totality and least elements are inherited by subsets (Well-order and well-ordered set).
Proof
Claim (a): let ; then by transitivity of , so strictly well-orders by [L1], and is transitive, because gives and by transitivity of , whence by transitivity of the relation on ; so is an ordinal.
Claim (b): if then is an element of satisfying , contradicting irreflexivity of on ; hence .
Claim (f), the easy direction: gives by transitivity of , and gives trivially.
Claim (f), the substantial direction: assume and , let be the -least element of the nonempty set , and check ; indeed forces by transitivity of and then , since otherwise with contradicts minimality, so ; conversely compared with by trichotomy in cannot satisfy or , since each would put , using transitivity of in the second case, so and ; hence .
Claim (c): is transitive, because means , whence , or ; the relation is irreflexive on by [A1] and step 1.2, transitive there because with gives and with reduces to transitivity in , and trichotomous there because two elements of are comparable in while satisfies and neither nor , both of which would give ; finally a nonempty has an -least element, namely the -least element of when that is nonempty and otherwise.
Claim (d): is transitive, since gives and hence for every , so ; and is a subset of any fixed member of the nonempty set , so strictly well-orders it by [L1].
Claim (g): is an ordinal by claim (d) applied to , and and , so claim (f) gives or , and likewise for ; both memberships at once would give , contradicting claim (b), so or , that is or .
Claim (e): is transitive, since gives ; its elements are ordinals by claim (a), so is irreflexive on it by claim (b) and transitive on it because with puts all in the ordinal ; any two of its elements lie in a common member of by claim (g) and are therefore comparable, which gives trichotomy by claim (b) and claim (f); and a nonempty has an -least element, namely the -least element of for any meeting , since an element of lying -below it would lie in by transitivity and contradict minimality.
Claims (a) to (g) are established.
Remarks
The successor is the immediate successor. Claim (c) makes an ordinal, and it is the least ordinal strictly above : any with satisfies , hence by claim (f). So the ordinals have no gaps immediately above a given point, which is what makes the successor and limit dichotomy of Successor and limit ordinals exhaustive.
Suprema come for free. Claim (e) says a set of ordinals always has a least upper bound, namely : it contains every member of as a subset, hence lies weakly above each by claim (f), and any ordinal weakly above all of them contains . Claim (d) gives the dual statement for a nonempty set. Neither needs any completeness assumption, in sharp contrast with the situation for .
Nonemptiness in claim (d) is essential. The intersection of the empty family is not a set, so the hypothesis cannot be dropped. The union of the empty family, by contrast, is , which is why claim (e) needs no such hypothesis.
Claim (g) is a departure from the usual bookkeeping. It is normally derived alongside trichotomy. It is proved here because claim (e) cannot be proved without it, and separating them would either duplicate the argument or create a circular dependency between this lemma and Trichotomy and well-ordering of the ordinals.
The naturals are the model case. Every natural number is a transitive set and satisfies (Every natural number is a transitive set and is not a member of itself), which is exactly claims (a) and (b) in the situation this definition abstracts, and is the successor operation of claim (c). That every natural number, and itself, really is an ordinal is proved in is the least limit ordinal.