ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

The chains of a poset, ordered by inclusion, form a chain-complete poset

Example

Let $(P, \le)$ be any poset and let

$\mathcal{C} = \{\, C \subseteq P : C \text{ is a chain of } P \,\}$

be the set of its chains (Chain in a poset), ordered by inclusion. Then $\mathcal{C}$ is chain-complete (Chain-complete poset): an inclusion chain $\mathcal{D} \subseteq \mathcal{C}$ has least upper bound $\bigcup \mathcal{D}$ , which is again a chain of $P$ because any two of its elements lie in a common member of $\mathcal{D}$ . Its bottom element is $\bot = \sup \emptyset = \emptyset$ .

This is the poset that Zorn's lemma builds at its step 1.2 and declares chain-complete at its step 2.1, so what follows is that step worked out in full: the engine of Zorn's lemma, running on its own.

Facts & Assumptions

Given: A poset $(P, \le)$ and the set $\mathcal{C}$ of chains of $P$ , ordered by inclusion; note $\mathcal{C} \subseteq \mathcal{P}(P)$ .

[L1]

A subset $C \subseteq P$ is a chain when any two of its elements are comparable, and the empty set is a chain (Chain in a poset).

[L2]

Inclusion partially orders $\mathcal P(P)$ . For any $\mathcal D\subseteq\mathcal P(P)$ , every $C\in\mathcal D$ satisfies $C\subseteq\bigcup\mathcal D$ , while any $V$ containing every $C\in\mathcal D$ also contains every element of $\bigcup\mathcal D$ ; hence $\bigcup\mathcal D$ is the least upper bound of $\mathcal D$ (Partial order and partially ordered set, Upper bound, least upper bound, and strict upper bound).

[L3]

$u$ is an upper bound of $S$ when $s \le u$ for every $s \in S$ , and a least upper bound when in addition $u \le v$ for every upper bound $v$ of $S$ (Upper bound, least upper bound, and strict upper bound).

[L4]

A poset is chain-complete when every chain has a least upper bound, and then $\bot = \sup \emptyset$ is its least element (Chain-complete poset).

[L5]

A partial order on a set $X$ is a relation on $X$ that is reflexive, antisymmetric and transitive, each of the three being a condition required of all elements of $X$ (Partial order and partially ordered set).

Verification

technique · direct

1.1

$\mathcal{C}$ is a subset of $\mathcal{P}(P)$ , and inclusion partially orders $\mathcal{P}(P)$ ; reflexivity, antisymmetry and transitivity are required of all elements of $\mathcal{P}(P)$ , so they hold in particular for all elements of $\mathcal{C}$ , and the restriction of inclusion to $\mathcal{C}$ partially orders $\mathcal{C}$ .

givenL2L5

1.2

Let $\mathcal{D} \subseteq \mathcal{C}$ be a chain for inclusion and put $U = \bigcup \mathcal{D}$ .

givenconstruct

2.1

$U$ is a chain of $P$ : let $x, y \in U$ , say $x \in C_1$ and $y \in C_2$ with $C_1, C_2 \in \mathcal{D}$ ; as $\mathcal{D}$ is a chain for inclusion, $C_1 \subseteq C_2$ or $C_2 \subseteq C_1$ , so $x$ and $y$ both lie in whichever of the two is the larger, and that set is a chain of $P$ , hence $x$ and $y$ are comparable in $P$ . So $U \in \mathcal{C}$ , the case $\mathcal{D} = \emptyset$ reading $U = \emptyset \in \mathcal{C}$ with the condition on $x, y$ vacuous.

step 1.2L1

2.2

$U$ is an upper bound of $\mathcal{D}$ for inclusion: $C \subseteq \bigcup \mathcal{D} = U$ for every $C \in \mathcal{D}$ .

step 1.2L3

3.1

$U$ is least among the upper bounds of $\mathcal{D}$ lying in $\mathcal{C}$ : such a $V$ is in particular an upper bound of $\mathcal{D}$ in $\mathcal{P}(P)$ , where $\bigcup \mathcal{D}$ is least, so $U \subseteq V$ .

step 2.2L2L3

4.1

So every inclusion chain $\mathcal{D} \subseteq \mathcal{C}$ has least upper bound $\bigcup \mathcal{D}$ in $\mathcal{C}$ , that is $\mathcal{C}$ is chain-complete, with $\bot = \sup \emptyset = \emptyset$ .

step 2.1step 3.1L4∎

Remarks

This is the whole of Zorn's engine. Given a nonempty $P$ in which every chain has an upper bound and assuming no maximal element exists, every chain $C$ admits a strict upper bound; choosing one for each chain at once turns $C \mapsto C \cup \{\text{chosen strict upper bound}\}$ into a progressive map on $\mathcal{C}$ , and Bourbaki-Witt applied to the chain-completeness proved here returns a chain equal to its own extension, which is absurd. That is Zorn's lemma, and the Axiom of Choice is used at exactly one point of it, the simultaneous choice of strict upper bounds, and nowhere in this example.
$\mathcal{C}$ is chain-complete but usually not a complete lattice. An arbitrary union of chains need not be a chain: if $x, y \in P$ are incomparable then $\{x\}$ and $\{y\}$ are chains and $\{x, y\}$ is not, so the family $\{\{x\}, \{y\}\}$ has no supremum given by union. This is exactly the gap between this example and The power set is chain-complete, with union as supremum, and it is why chain-completeness rather than completeness is the right hypothesis for Bourbaki–Witt fixed point theorem.
An immediate consequence, at the price of the Axiom of Choice. $\mathcal{C}$ is nonempty, since $\emptyset \in \mathcal{C}$ , and every chain of $\mathcal{C}$ has an upper bound by the verification above. Assume in addition the Axiom of Choice (The Axiom of Choice), which Zorn's lemma assumes outright: Zorn's lemma then applies to $\mathcal{C}$ and yields a maximal element, so every poset has a maximal chain. This is the Hausdorff maximal principle, and it costs exactly one application of Zorn, hence the Axiom of Choice. The chain-completeness verified above costs nothing.
The verification never used any property of $P$ beyond its being a poset. In particular $P$ may be empty, in which case $\mathcal{C} = \{\emptyset\}$ is the one-element poset.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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

Bourbaki-Witt Principle (Menemui Matematik 39(1), 2017) (standard reference, not scraped)
Bourbaki–Witt theorem (Wikipedia) (standard reference, not scraped)
Zorn's lemma (Wikipedia) (standard reference, not scraped)
Complete partial order (Wikipedia) (standard reference, not scraped)