TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-03 (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.

Zorn's lemma implies the Axiom of Choice

Statement

Assume Zorn's lemma: every nonempty poset in which every chain has an upper bound has a maximal element. Then every family of nonempty sets has a choice function (Choice function); that is, the Axiom of Choice holds.

Facts & Assumptions

Given: A family $F$ all of whose members are nonempty, and Zorn's lemma.

[A1]

Every member of $F$ is nonempty.

[A2]

By the assumed Zorn principle, a nonempty poset in which every chain has an upper bound has a maximal element.

[L2]

A choice function for a family $G$ is a function $h$ with domain $G$ such that $h (S) \in S$ for every $S \in G$ (Choice function).

[L3]

$m$ is maximal when there is no element strictly above it (Maximal element and greatest element).

[L4]

A partial order is a relation that is reflexive, antisymmetric and transitive, and a poset is a set carrying one (Partial order and partially ordered set).

[L5]

A chain is a subset of a poset in which any two members are comparable (Chain in a poset).

Proof

technique · contradiction

1.1

Suppose $F$ has no choice function.

assume-contra

1.2

Let $P$ be the set of partial choice functions: pairs $(G, h)$ with $G \subseteq F$ and $h$ a choice function for $G$ , ordered by $(G, h) \leq (G^{'}, h^{'})$ when $G \subseteq G^{'}$ and $h^{'}$ restricted to $G$ equals $h$ .

L2construct

2.1

$P$ is nonempty, since the empty function is a choice function for the empty subfamily, so $(\emptyset, \emptyset) \in P$ .

step 1.2L2

2.2

Every chain in $P$ has an upper bound: given a chain, take the union of the domains and the union of the functions. Any two partial choice functions in the chain are comparable by [L5], so the smaller is a restriction of the larger; their values therefore agree on overlapping domains. Thus the union is a function and is a choice function for the union of the domains.

step 1.2L2L5

2.3

The relation just defined is a partial order on $P$ : it is reflexive, since $G \subseteq G$ and $h$ restricted to $G$ is $h$ ; antisymmetric, since $(G, h) \leq (G^{'}, h^{'})$ and $(G^{'}, h^{'}) \leq (G, h)$ give $G \subseteq G^{'}$ and $G^{'} \subseteq G$ , hence $G = G^{'}$ , and then $h = h^{'}$ restricted to $G = G^{'}$ , which is $h^{'}$ itself; and transitive, since $G \subseteq G^{'} \subseteq G^{''}$ gives $G \subseteq G^{''}$ , while restricting $h^{''}$ to $G$ is the same as first restricting it to $G^{'}$ , which gives $h^{'}$ , and then restricting $h^{'}$ to $G$ , which gives $h$ . So $(P, \leq)$ is a poset.

step 1.2L4

3.1

By the assumed Zorn principle $P$ has a maximal element $(G, h)$ .

step 2.1step 2.2step 2.3A2

4.1

If $G = F$ then $h$ is a choice function for $F$ , contrary to the assumption; so there exists $S \in F$ with $S \notin G$ .

step 3.1step 1.1L2choose

5.1

The set $S$ is nonempty, so there exists an element of $S$ ; fix one and call it $a$ .

step 4.1A1choose

6.1

Then $(G \cup {S}, h \cup {(S, a)})$ lies in $P$ and is strictly above $(G, h)$ , since $S \notin G$ .

step 4.1step 5.1step 1.2L2

7.1

This contradicts maximality of $(G, h)$ , so the assumption fails and $F$ has a choice function.

step 6.1step 3.1L3discharge-contradiction∎

Remarks

Step 5.1 makes a single existential instantiation, exactly as in Every natural-number-indexed list of nonempty sets has a choice function on its family of values, and is not a use of choice. The work of choosing across all of $F$ at once has already been done by Zorn's lemma at step 3.1.
The poset of partial choice functions is the standard vehicle for this direction, and it illustrates the usual shape of a Zorn argument: order the partial solutions by extension, check that a chain of them unions to a partial solution, and observe that a maximal partial solution cannot be partial.
Together with Zorn's lemma this gives the equivalence recorded in The Axiom of Choice and Zorn's lemma are equivalent.

Depends on

Used by

The Axiom of Choice and Zorn's lemma are equivalent Corollary

Dependency tree · two levels

8 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

I. Khatchatourian, The Axiom of Choice (University of Toronto MAT327 notes) (standard reference, not scraped)
The Axiom of Choice (Stanford Encyclopedia of Philosophy) (standard reference, not scraped)
Zorn's lemma (Wikipedia) (standard reference, not scraped)
Axiom of choice (Wikipedia) (standard reference, not scraped)