LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)

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 union of a nonempty chain of filters is a filter

Statement

Let $X$ be a set and let $D$ be a nonempty chain (Chain in a poset) in the set of filters on $X$ ordered by inclusion (Filter on a set, Partial order and partially ordered set): every member of $D$ is a filter on $X$ , and any two members of $D$ are comparable under $\subseteq$ . Then $⋃ D$ is a filter on $X$ , and it is an upper bound of $D$ for inclusion.

The hypothesis $D \neq \emptyset$ cannot be dropped: $⋃ \emptyset = \emptyset$ contains no set at all, in particular not $X$ , so it is not a filter.

Facts & Assumptions

Given: A set $X$ and a nonempty family $D$ of filters on $X$ , any two members of which are comparable under inclusion.

[A1]

$D \neq \emptyset$ ; every $F \in D$ is a filter on $X$ ; and for all $F_{1}, F_{2} \in D$ either $F_{1} \subseteq F_{2}$ or $F_{2} \subseteq F_{1}$ (Chain in a poset).

[L1]

A filter on $X$ is a family of subsets of $X$ containing $X$ , omitting $\emptyset$ , closed under pairwise intersection, and closed upward in $X$ (Filter on a set).

[L2]

Inclusion is a partial order on any set of sets (Partial order and partially ordered set), and $u$ is an upper bound of $S$ when $s \subseteq u$ for every $s \in S$ (Upper bound, least upper bound, and strict upper bound).

Proof

technique · direct

1.1

Fix a member $F_{*} \in D$ , which exists because $D$ is nonempty.

A1choose

1.2

$⋃ D \subseteq P (X)$ : a member of the union belongs to some filter on $X$ , hence is a subset of $X$ .

A1L1

1.3

$\emptyset \notin ⋃ D$ : a member of the union belongs to some $F \in D$ , and $\emptyset \notin F$ .

A1L1

1.4

$⋃ D$ is closed upward in $X$ : if $A \in F \in D$ and $A \subseteq B \subseteq X$ then $B \in F \subseteq ⋃ D$ .

A1L1

1.5

$⋃ D$ is closed under pairwise intersection: let $A \in F_{1}$ and $B \in F_{2}$ with $F_{1}, F_{2} \in D$ ; comparability puts one of the two inside the other, so $A$ and $B$ both belong to the larger one, which contains $A \cap B$ , and $A \cap B \in ⋃ D$ .

A1L1

1.6

Every $F \in D$ satisfies $F \subseteq ⋃ D$ , so $⋃ D$ is an upper bound of $D$ for inclusion.

A1L2

1.7

If instead $D = \emptyset$ then $⋃ D = \emptyset$ , which fails the requirement $X \in ⋃ D$ , so nonemptiness of $D$ is genuinely used and cannot be removed.

2.1

$X \in ⋃ D$ , because $X \in F_{*}$ and $F_{*} \subseteq ⋃ D$ .

step 1.1A1L1

3.1

So $⋃ D$ satisfies all four filter axioms and is an upper bound of $D$ : it is a filter on $X$ above every member of $D$ .

step 2.1step 1.2step 1.3step 1.4step 1.5step 1.6L1∎

Remarks

Nonemptiness is used exactly once, at step 1.1, and only for the axiom $X \in ⋃ D$ . The other three axioms hold vacuously for the empty chain, which is precisely why the failure is easy to overlook: three of the four checks go through and the one that does not is the one nobody writes out.
This is the chain-bound half of the hypothesis of Zorn's lemma (Zorn's lemma), and the empty chain is the other half. In The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter the empty chain is bounded not by this lemma but by the given filter $F_{0}$ , which is why that proof must treat the two cases separately.
Unions of chains are used rather than unions of arbitrary families because an arbitrary union of filters is almost never a filter: for $x \neq y$ the union of the principal filters at $x$ and at $y$ contains ${x}$ and ${y}$ but not $\emptyset = {x} \cap {y}$ , so it is not closed under intersection. Comparability at step 1.5 is what repairs this.

Depends on

Used by

Dependency tree · two levels

7 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

Filter (set theory) (Wikipedia) (standard reference, not scraped)
Zorn's lemma (Wikipedia) (standard reference, not scraped)
B. Kaya, Ultrafilters and How to Use Them (standard reference, not scraped)