CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29

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.

Ordinal multiplication exists and is unique, and its values are ordinals

Statement

Fix an ordinal $α$ (Ordinal (von Neumann)). There is exactly one class function $β \mapsto p_{α} (β)$ , defined at every ordinal $β$ , satisfying the three clauses

$p_{α} (0) = 0, p_{α} (β^{+}) = p_{α} (β) + α, p_{α} (λ) = ⋃ {p_{α} (β) : β \in λ} (λ a limit ordinal),$

where $+$ is ordinal addition (Ordinal addition $α + β$ ), and every value $p_{α} (β)$ is an ordinal.

The three clauses are exhaustive and mutually exclusive because every ordinal is exactly one of $0$ , a successor, or a limit (Successor and limit ordinals). This is the well-definedness obligation discharged before ordinal multiplication is written down; the operation itself is named in the definition that follows. The proof is a theorem of ZF and uses no choice principle.

Facts & Assumptions

Given: A fixed ordinal $α$ and the axioms of ZF. No choice principle is assumed. For a function $h$ , $ran (h)$ is its range.

[L1]

Recursion along the ordinals: for a class function $G$ assigning a set to every function whose domain is an ordinal there is exactly one class function $F$ , defined at every ordinal, with $F (β) = G (F ↾ β)$ for all $β$ (Transfinite recursion along the ordinals: a class rule determines exactly one operation defined at every ordinal).

[L2]

Every ordinal is exactly one of: $0$ , a successor ordinal $δ^{+}$ with $δ$ uniquely determined, or a limit ordinal (Successor and limit ordinals).

[L3]

$⋃ A$ is an ordinal for every set $A$ of ordinals, and is its least upper bound (claim (e) of Basic closure properties of ordinals).

[L4]

$μ + α$ is an ordinal whenever $μ$ and $α$ are (Ordinal addition $α + β$ , Ordinal addition exists and is unique: the clauses at $0$ , at a successor and at a limit determine one operation, and its values are ordinals).

[L5]

Every nonempty set of ordinals has an $\in$ -least element (Trichotomy and well-ordering of the ordinals), and ${ξ \in β_{0}^{+} : P (ξ)}$ is such a set whenever $P (β_{0})$ holds and $P$ is a property of ordinals.

Proof

technique · direct

1.1

Define a class function $G$ on functions $h$ whose domain is an ordinal $β$ by: $G (h) = 0$ if $β = 0$ ; $G (h) = h (δ) + α$ if $β = δ^{+}$ ; and $G (h) = ⋃ ran (h)$ if $β$ is a limit ordinal.

construct

1.2

The three cases are exhaustive and mutually exclusive by [L2], and $δ$ is determined by $β = δ^{+}$ , so $G (h)$ is a well-determined set for every such $h$ and the rule is a formula.

L2L4

2.1

By [L1] there is exactly one class function $p_{α}$ , defined at every ordinal, with $p_{α} (β) = G (p_{α} ↾ β)$ for every ordinal $β$ .

step 1.1step 1.2L1

3.1

Unwinding the three cases of $G$ : $p_{α} (0) = G (\emptyset) = 0$ ; $p_{α} (δ^{+}) = (p_{α} ↾ δ^{+}) (δ) + α = p_{α} (δ) + α$ , since $δ \in δ^{+}$ ; and for a limit $λ$ , $p_{α} (λ) = ⋃ ran (p_{α} ↾ λ) = ⋃ {p_{α} (β) : β \in λ}$ .

step 2.1step 1.1

4.1

Every value is an ordinal: were $p_{α} (β_{0})$ not an ordinal for some $β_{0}$ , [L5] would give a least $μ \in β_{0}^{+}$ with $p_{α} (μ)$ not an ordinal, and each of the three cases refutes that, since $0$ is an ordinal, $p_{α} (δ^{+}) = p_{α} (δ) + α$ is an ordinal by [L4] because $δ \in μ$ makes $p_{α} (δ)$ an ordinal, and $p_{α} (λ)$ is a union of a set of ordinals, hence an ordinal by [L3].

step 3.1L2L3L4L5

4.2

Uniqueness: a class function $t$ defined at every ordinal and satisfying the three displayed clauses satisfies $t (β) = G (t ↾ β)$ for every $β$ , one case at a time, so $t = p_{α}$ by the uniqueness half of [L1].

step 3.1step 2.1L1L2

5.1

Hence exactly one class function on the ordinals satisfies the three clauses, and all its values are ordinals.

step 4.1step 4.2step 3.1∎

Remarks

The successor clause adds $α$ on the right. $p_{α} (β^{+}) = p_{α} (β) + α$ , not $α + p_{α} (β)$ . Since ordinal addition is not commutative, this is a genuine choice of convention, and it is the one that makes $α \cdot β$ come out as " $β$ copies of $α$ " rather than " $α$ copies of $β$ " ( $α \cdot β$ is the order type of $α \times β$ ordered by last differences, that is $β$ copies of $α$ ).

Nothing here uses a property of $+$ . The proof needs only that $μ + α$ is an ordinal, which is the content of Ordinal addition exists and is unique: the clauses at $0$ , at a successor and at a limit determine one operation, and its values are ordinals. Associativity, monotonicity and the rest are proved later and are not presupposed.

Depends on

Used by

Dependency tree · two levels

17 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Ordinal arithmetic (Wikipedia) (standard reference, not scraped)
T. Jech, Set Theory, 3rd millennium ed., Ch. 2 (Ordinal numbers) (standard reference, not scraped)
R. Moosa, Set Theory course notes (standard reference, not scraped)