Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicableverified 2026-08-06 (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 ⋃x of a set, and the binary union a∪b:=⋃{a,b}

Definition

Let x be a set. The Axiom of Union: ∀x ∃y ∀z (z∈y↔∃s (s∈x∧z∈s)) gives a set whose elements are exactly the sets z belonging to some member of x, and The Axiom of Extensionality: ∀x ∀y (∀z (z∈x↔z∈y)→x=y) shows there is only one such set; it is written ⋃x. Thus ⋃x is the set whose elements are exactly the elements of the elements of x, and a∪b:=⋃{a,b} is the binary union of a and b, formed from the unordered pair of The unordered pair {x,y} and the singleton {x}={x,x}:

z∈⋃x↔∃s (s∈x∧z∈s).

The membership criterion for the binary union, that z∈a∪b holds exactly when z∈a or z∈b, is proved at ⋃∅=∅, ⋃{a}=a, ⋃{a,b}=a∪b, ⋂{a}=a, and ⋂{a,b}=a∩b rather than assumed here.

Remarks

  • One layer only. ⋃x collects the elements of the elements of x, not the elements of x. For a set of sets of sets the operation therefore has to be applied twice, and that iteration is what makes ⋃⋃R the right ambient set for the domain and range of a relation.

  • Notation. ⋃ with a single set argument is the primitive operation supplied by the axiom; ∪ between two sets is the derived binary one. The indexed form ⋃i∈IAi is a further abbreviation, defined once indexed families are available.

Depends on

Used by

Dependency tree · two levels

5 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