ExampleConstruction: Literature-sourcedVerification: 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.

The power set is chain-complete, with union as supremum

Example

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

$\sup D = ⋃ D \in P (X)$

(Upper bound, least upper bound, and strict upper bound). So $(P (X), \subseteq)$ is chain-complete (Chain-complete poset), and its bottom element is $⊥ = \sup \emptyset = ⋃ \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 $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 \leq u$ for every $s \in S$ , and a least upper bound when in addition $u \leq 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 $⊥ = \sup \emptyset$ is its least element (Chain-complete poset).

Verification

technique · direct

1.1

Inclusion partially orders $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 $D \subseteq P (X)$ and put $U = ⋃ D$ , so that $x \in U$ exactly when $x \in D$ for some $D \in D$ ; each such $D$ satisfies $D \subseteq X$ , hence $U \subseteq X$ and $U \in P (X)$ .

givenconstruct

2.1

$U$ is an upper bound of $D$ : if $D \in 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 P (X)$ satisfy $D \subseteq V$ for every $D \in D$ ; any $x \in U$ lies in some $D \in D$ and hence in $V$ , so $U \subseteq V$ .

step 1.2L2

3.1

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

step 1.1step 2.1step 2.2L3L4

4.1

The empty chain is the case $D = \emptyset$ , where $U = ⋃ \emptyset = \emptyset$ ; so $⊥ = \sup \emptyset = \emptyset$ , which is indeed the least element, since $\emptyset \subseteq A$ for every $A \in 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 $D$ is a chain, so every subset of $P (X)$ has a supremum and $(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 $D$ the greatest lower bound is $⋂ D$ , and the greatest lower bound of the empty family is $X$ , the top element. The class $⋂ \emptyset$ is not a set, which is why the empty case is read inside $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 $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 · one level

4 results within one dependency step 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

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