TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)

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.

The well-ordering theorem implies the Axiom of Choice

Statement

Work in ZF and assume that every set can be well ordered (Well-order and well-ordered set). Then the Axiom of Choice holds (The Axiom of Choice): every family of nonempty sets has a choice function (Choice function).

Facts & Assumptions

Given: The axioms of ZF together with the hypothesis that every set carries a well-order. Let $\mathcal{F}$ be an arbitrary family of nonempty sets.

[A1]

By the Given, every set carries a well-order.

[L1]

A choice function for $\mathcal{F}$ is a function $g$ on $\mathcal{F}$ with $g(S) \in S$ for every $S \in \mathcal{F}$ (Choice function).

[L2]

The Axiom of Choice is the statement that every family of nonempty sets has a choice function (The Axiom of Choice).

[L3]

In a well-order every nonempty subset has a least element, and that least element is unique (Well-order and well-ordered set).

Proof

technique · direct

1.1

Let $U = \bigcup \mathcal{F}$ , which is a set by the Union axiom of ZF, available by the Given, and note that every member of $\mathcal{F}$ is a subset of $U$ .

givenconstruct

2.1

By hypothesis there is a well-order $<$ on $U$ ; fix one.

step 1.1A1choose

3.1

Every $S \in \mathcal{F}$ is a nonempty subset of $U$ , so it has a least element with respect to $<$ , and that element is unique.

step 2.1step 1.1L3

4.1

Hence $g = \{(S, y) \in \mathcal{F} \times U : y \text{ is the } < \text{-least element of } S\}$ is a function on $\mathcal{F}$ with $g(S) \in S$ for every $S$ , since uniqueness in step 3.1 gives exactly one $y$ for each $S$ .

step 3.1L1

5.1

So $g$ is a choice function for $\mathcal{F}$ , and since $\mathcal{F}$ was an arbitrary family of nonempty sets, the Axiom of Choice holds.

step 4.1L1L2∎

Remarks

One well-order, then no more choosing. The single act of naming a well-order of $U$ in step 2.1 is an existential instantiation, not a choice principle: one object is named, not one per member of $\mathcal{F}$ . After that, the rule "take the least element" is canonical, and the resulting $g$ is a set by Separation on $\mathcal{F} \times U$ . That is the entire content of the implication, and it is why "well order the union" is the standard way to manufacture choice functions.

The same trick, free of charge, on $\mathbb{N}$ . Nothing above needs the hypothesis when $U$ already carries a canonical well-order. Every family of nonempty subsets of $\mathbb{N}$ has the explicit choice function $S \mapsto \min S$ , by The well-ordering principle, with no axiom at all. The Axiom of Choice is exactly the assertion that this convenience is always available.

Direction matters. This item proves one implication only. The converse, that the Axiom of Choice yields a well-order of every set, is The well-ordering theorem and is the harder half; the two together give the equivalence recorded in Choice, Zorn and well-ordering are equivalent.

Depends on

Used by

Choice, Zorn and well-ordering are equivalent Corollary
FALSE: the well-ordering theorem is a theorem of ZF False statement

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 37 results over 11 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

Well-ordering theorem (Wikipedia) (standard reference, not scraped)
Axiom of choice (Wikipedia) (standard reference, not scraped)
The Well-Ordering Problem (Open Logic Project) (standard reference, not scraped)
Formalization of the Axiom of Choice and its Equivalent Theorems (standard reference, not scraped)