CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 $\alpha$ (Ordinal (von Neumann)). There is exactly one class function $\beta \mapsto \mathrm{p}_\alpha(\beta)$ , defined at every ordinal $\beta$ , satisfying the three clauses

$\mathrm{p}_\alpha(0) = 0, \qquad \mathrm{p}_\alpha(\beta^{+}) = \mathrm{p}_\alpha(\beta) + \alpha, \qquad \mathrm{p}_\alpha(\lambda) = \bigcup\{\, \mathrm{p}_\alpha(\beta) : \beta \in \lambda \,\} \ \ (\lambda \text{ a limit ordinal}),$

where $+$ is ordinal addition (Ordinal addition $\alpha + \beta$ ), and every value $\mathrm{p}_\alpha(\beta)$ 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 $\alpha$ and the axioms of ZF. No choice principle is assumed. For a function $h$ , $\operatorname{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(\beta) = G(F \restriction \beta)$ for all $\beta$ (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 $\delta^{+}$ with $\delta$ uniquely determined, or a limit ordinal (Successor and limit ordinals).

[L3]

$\bigcup 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]

$\mu + \alpha$ is an ordinal whenever $\mu$ and $\alpha$ are (Ordinal addition $\alpha + \beta$ , 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 $\{\xi \in \beta_0^{+} : P(\xi)\}$ is such a set whenever $P(\beta_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 $\beta$ by: $G(h) = 0$ if $\beta = 0$ ; $G(h) = h(\delta) + \alpha$ if $\beta = \delta^{+}$ ; and $G(h) = \bigcup \operatorname{ran}(h)$ if $\beta$ is a limit ordinal.

construct

1.2

The three cases are exhaustive and mutually exclusive by [L2], and $\delta$ is determined by $\beta = \delta^{+}$ , 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 $\mathrm{p}_\alpha$ , defined at every ordinal, with $\mathrm{p}_\alpha(\beta) = G(\mathrm{p}_\alpha \restriction \beta)$ for every ordinal $\beta$ .

step 1.1step 1.2L1

3.1

Unwinding the three cases of $G$ : $\mathrm{p}_\alpha(0) = G(\varnothing) = 0$ ; $\mathrm{p}_\alpha(\delta^{+}) = (\mathrm{p}_\alpha \restriction \delta^{+})(\delta) + \alpha = \mathrm{p}_\alpha(\delta) + \alpha$ , since $\delta \in \delta^{+}$ ; and for a limit $\lambda$ , $\mathrm{p}_\alpha(\lambda) = \bigcup \operatorname{ran}(\mathrm{p}_\alpha \restriction \lambda) = \bigcup\{\mathrm{p}_\alpha(\beta) : \beta \in \lambda\}$ .

step 2.1step 1.1

4.1

Every value is an ordinal: were $\mathrm{p}_\alpha(\beta_0)$ not an ordinal for some $\beta_0$ , [L5] would give a least $\mu \in \beta_0^{+}$ with $\mathrm{p}_\alpha(\mu)$ not an ordinal, and each of the three cases refutes that, since $0$ is an ordinal, $\mathrm{p}_\alpha(\delta^{+}) = \mathrm{p}_\alpha(\delta) + \alpha$ is an ordinal by [L4] because $\delta \in \mu$ makes $\mathrm{p}_\alpha(\delta)$ an ordinal, and $\mathrm{p}_\alpha(\lambda)$ is a union of a set of ordinals, hence an ordinal by [L3].

step 3.1L2L3L4L5

4.2

Uniqueness: a class function $\mathrm{t}$ defined at every ordinal and satisfying the three displayed clauses satisfies $\mathrm{t}(\beta) = G(\mathrm{t} \restriction \beta)$ for every $\beta$ , one case at a time, so $\mathrm{t} = \mathrm{p}_\alpha$ 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 $\alpha$ on the right. $\mathrm{p}_\alpha(\beta^{+}) = \mathrm{p}_\alpha(\beta) + \alpha$ , not $\alpha + \mathrm{p}_\alpha(\beta)$ . Since ordinal addition is not commutative, this is a genuine choice of convention, and it is the one that makes $\alpha \cdot \beta$ come out as " $\beta$ copies of $\alpha$ " rather than " $\alpha$ copies of $\beta$ " ( $\alpha \cdot \beta$ is the order type of $\alpha \times \beta$ ordered by last differences, that is $\beta$ copies of $\alpha$ ).

Nothing here uses a property of $+$ . The proof needs only that $\mu + \alpha$ 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 32 results over 16 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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)