LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)

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.

Trichotomy and well-ordering of the ordinals

Statement

For ordinals $α$ and $β$ (Ordinal (von Neumann)), exactly one of

$α \in β, α = β, β \in α$

holds. Moreover every nonempty set $A$ of ordinals has an $\in$ -least element, and consequently $A$ ordered by $α \leq β : ⟺ α \subseteq β$ is a well-order (Well-order and well-ordered set) whose strict part is membership.

So the ordinals are linearly ordered by $\in$ , every set of them is well ordered, and Transfinite induction is available on any such set. No choice principle is used.

Facts & Assumptions

Given: Ordinals $α$ , $β$ , and a nonempty set $A$ whose members are all ordinals.

[A1]

An ordinal is a transitive set on which $\in$ is a strict well-order (Ordinal (von Neumann)).

[L1]

Every element of an ordinal is an ordinal; $α \notin α$ ; $α \subseteq β$ if and only if $α \in β$ or $α = β$ ; and any two ordinals are comparable under inclusion (Basic closure properties of ordinals).

[L2]

A partial order is a reflexive, antisymmetric and transitive relation; a total order is a partial order any two of whose elements are comparable; and the strict part of $\leq$ is $x < y : ⟺ (x \leq y$ and $x \neq y)$ (Partial order and partially ordered set).

[L3]

A well-order is a total order in which every nonempty subset has a least element (Well-order and well-ordered set).

[L4]

Transfinite induction holds on every well-order (Transfinite induction).

Proof

technique · direct

1.1L1

At least one alternative holds: by [L1] either $α \subseteq β$ or $β \subseteq α$ , and in the first case [L1] gives $α \in β$ or $α = β$ , in the second $β \in α$ or $β = α$ .

2.1step 1.1A1L1

At most one alternative holds: $α \in β$ together with $α = β$ gives $α \in α$ ; $β \in α$ together with $α = β$ gives $α \in α$ ; and $α \in β$ together with $β \in α$ gives $β \subseteq α$ by transitivity of $α$ and hence $α \in α$ ; each contradicts [L1].

3.1step 1.1step 2.1A1L1

Least elements: fix $α \in A$ ; if $α \cap A = \emptyset$ then $α$ is $\in$ -least in $A$ , because $β \in A$ with $β \in α$ would lie in $α \cap A$ , so trichotomy leaves $α \in β$ or $α = β$ ; otherwise $α \cap A$ is a nonempty subset of $α$ and has an $\in$ -least element $γ$ there, and $γ$ is $\in$ -least in $A$ , because $β \in A$ with $β \in γ$ would satisfy $β \in α$ by transitivity of $α$ and so lie in $α \cap A$ strictly below $γ$ , and trichotomy again leaves $γ \in β$ or $γ = β$ .

4.1step 1.1step 3.1L1L2L3L4

On $A$ the relation $α \leq β : ⟺ α \subseteq β$ satisfies the three axioms of [L2], since inclusion is reflexive, antisymmetric by extensionality, and transitive, so it is a partial order; it is total by [L1] and step 1.1; its strict part in the sense of [L2] is membership, since $α \subseteq β$ with $α \neq β$ is $α \in β$ by [L1]; and every nonempty subset of $A$ has a least element by step 3.1, so $(A, \subseteq)$ is a well-order in the sense of [L3] and [L4] applies to it.

5.1step 2.1step 3.1step 4.1∎

Exactly one of the three alternatives holds, every nonempty set of ordinals has an $\in$ -least element, and every set of ordinals is well ordered by inclusion.

Remarks

Why this is not circular. The trichotomy of $\in$ on a single ordinal is part of Ordinal (von Neumann); what is proved here is trichotomy between arbitrary ordinals, which is a statement about the whole class and not about any one set. The bridge is inclusion comparability, proved in Basic closure properties of ordinals by intersecting the two ordinals, and the intersection argument is where the two levels meet.

The class of ordinals behaves like a well-order without being a set. Every nonempty set of ordinals has a least element, and in fact so does every nonempty definable collection of them: if $φ (α)$ holds for some $α$ , apply the statement to the set ${ξ \in α^{+} : φ (ξ)}$ , which is nonempty. That the collection of all ordinals is nevertheless not a set is Burali-Forti: there is no set of all ordinals.

A set of ordinals need not be an ordinal. Well-ordering by $\in$ is only half of the definition; transitivity is the other half. The set ${1, 3}$ , that is ${{\emptyset}, {\emptyset, {\emptyset}, {\emptyset, {\emptyset}}}}$ , is well ordered by membership but is not transitive, so it is not an ordinal. A transitive set of ordinals is one, which is the form in which this lemma gets used in Every well-order has a unique order type and Hartogs: an ordinal that does not inject into a given set.

Trichotomy and well-ordering of the ordinals

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources