ExampleConstruction: Literature-sourcedVerification: 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 power set is chain-complete, with union as supremum

Example

For any set $X$ , the power set $\mathcal{P}(X)$ ordered by inclusion is a poset (Partial order and partially ordered set) in which every $\subseteq$ -chain $\mathcal{D}$ (Chain in a poset) has least upper bound

$\sup \mathcal{D} = \bigcup \mathcal{D} \in \mathcal{P}(X)$

(Upper bound, least upper bound, and strict upper bound). So $(\mathcal{P}(X), \subseteq)$ is chain-complete (Chain-complete poset), and its bottom element is $\bot = \sup \emptyset = \bigcup \emptyset = \emptyset$ .

Both halves of "least upper bound" are checked below. Chain-completeness asks for the least one, not merely for some upper bound, and it is leastness that the Bourbaki–Witt argument consumes.

Facts & Assumptions

Given: A set $X$ and its power set $\mathcal{P}(X) = \{A : A \subseteq X\}$ , ordered by inclusion.

[F1]

Axiom of Extensionality: sets with exactly the same elements are equal.

[L1]

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

[L2]

$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).

[L3]

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

[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).

Verification

technique · direct

1.1

Inclusion partially orders $\mathcal{P}(X)$ : $A \subseteq A$ ; if $A \subseteq B$ and $B \subseteq A$ then $A$ and $B$ have the same elements, so $A = B$ by extensionality; and $A \subseteq B \subseteq C$ gives $A \subseteq C$ .

givenF1L1

1.2

Let $\mathcal{D} \subseteq \mathcal{P}(X)$ and put $U = \bigcup \mathcal{D}$ , so that $x \in U$ exactly when $x \in D$ for some $D \in \mathcal{D}$ ; each such $D$ satisfies $D \subseteq X$ , hence $U \subseteq X$ and $U \in \mathcal{P}(X)$ .

givenconstruct

2.1

$U$ is an upper bound of $\mathcal{D}$ : if $D \in \mathcal{D}$ and $x \in D$ then $x \in U$ , so $D \subseteq U$ .

step 1.2L2

2.2

$U$ is least among the upper bounds: let $V \in \mathcal{P}(X)$ satisfy $D \subseteq V$ for every $D \in \mathcal{D}$ ; any $x \in U$ lies in some $D \in \mathcal{D}$ and hence in $V$ , so $U \subseteq V$ .

step 1.2L2

3.1

So every subset $\mathcal{D}$ of $\mathcal{P}(X)$ has least upper bound $\bigcup \mathcal{D}$ , and a chain is in particular a subset, so every chain has one and $(\mathcal{P}(X), \subseteq)$ is chain-complete.

step 1.1step 2.1step 2.2L3L4

4.1

The empty chain is the case $\mathcal{D} = \emptyset$ , where $U = \bigcup \emptyset = \emptyset$ ; so $\bot = \sup \emptyset = \emptyset$ , which is indeed the least element, since $\emptyset \subseteq A$ for every $A \in \mathcal{P}(X)$ .

step 3.1step 1.2L4∎

Remarks

The argument proves more than chain-completeness. Neither the construction of $U$ nor either of the two bound checks used that $\mathcal{D}$ is a chain, so every subset of $\mathcal{P}(X)$ has a supremum and $(\mathcal{P}(X), \subseteq)$ is a complete lattice. Chain-completeness is strictly weaker, and the posets to which Zorn's lemma is applied usually have only the weaker property (The chains of a poset, ordered by inclusion, form a chain-complete poset is the standard instance).
Infima are present too: for nonempty $\mathcal{D}$ the greatest lower bound is $\bigcap \mathcal{D}$ , and the greatest lower bound of the empty family is $X$ , the top element. The class $\bigcap \emptyset$ is not a set, which is why the empty case is read inside $\mathcal{P}(X)$ rather than absolutely.
The empty chain is not a technicality. It is what forces a chain-complete poset to have a least element at all, and here it produces $\emptyset$ . A convention that excludes the empty chain has to reintroduce the same content as a separate nonemptiness hypothesis (Chain-complete poset records the reduction between the two conventions).
Chain-completeness is not the same as having a top. Deleting the top element from $\mathcal{P}(\{1,2\})$ leaves the three-element poset of Two maximal elements and no greatest element, which is still chain-complete, since $\{1\}$ and $\{2\}$ are incomparable and so never lie in a common chain, yet it now has two maximal elements and no greatest one.

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: 4 results over 3 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

Complete partial order (Wikipedia) (standard reference, not scraped)
Complete lattice (Wikipedia) (standard reference, not scraped)