Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Union and Product of a Family of Sets Indexed by a Set, and the Intersection of a Family with an Inhabited Index Class, Are Sets
lemmalem:indexed-family-nbg-2026aSet TheoryFor a family of sets indexed by a class I: if I is a set, the union equals the union set of the image A[I] and the product is a set; if I has an element, the intersection is a set.Indexed Families of Sets and Their Union, Intersection and Product
definitiondef:indexed-family-nbg-2026aSet TheoryDefines a family of sets indexed by a class as a function on that class, together with the union and intersection of a family and the product of a family indexed by a set.- The standing framework for the foundations: classes and sets, the ten axioms of NBG without global choice, class comprehension, and the basic notation for the empty set, pairs, ordered pairs, class abstraction, Boolean operations, unions and power sets.
The Logical Framework of the Foundations: Classical First-Order Logic, the Informal Metatheory, and the Class Theory NBG
remarkrem:nbg-logic-2026aLogicSet TheoryRecords the three layers under the foundations: an informal metatheory, classical first-order logic with equality, and von Neumann-Bernays-Gödel class theory as a first-order theory with dependent choice to be added; explains where formulas enter and why statements about all subs…- The union of a set x is the set of all elements of elements of x, and its power set is the set of all subsets of x.
Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper
lemmalem:sets-closure-nbg-2026aSet TheoryEvery subclass of a set is a set, so the intersection and difference of a set with a class are sets; each set has a unique union set and a unique power set; the union of two sets is a set; and the class of all sets is a proper class, by Russell's argument.The Boolean Operations on Classes, Disjointness, and the Universal Class
definitiondef:class-operations-nbg-2026aSet TheoryInclusion of classes, the intersection, union and difference of two classes, and the universal class of all sets.Class Abstraction: the Class of All Sets Satisfying a Predicative Formula
definitiondef:class-abstraction-nbg-2026aSet TheoryFor a predicative formula, {x : φ} is the unique class whose elements are exactly the sets satisfying φ, and {x ∈ A : φ} is the class of elements of A satisfying φ.The Class Comprehension Theorem for Predicative Formulas
theoremthm:class-comprehension-nbg-2026aLogicSet TheoryFor every predicative formula there is a class whose elements, among the tuples of sets, are exactly the tuples satisfying the formula; for a single variable this class is unique. This is a theorem scheme, one theorem for each formula.- Every class with at least one element has an element that shares no element with it.
- There is a set containing the empty set and containing, along with each of its elements u, the set whose elements are those of u together with u itself.
- If a class assigns to each set at most one set through its ordered pairs, then the sets assigned to the elements of any given set form a set.
- For every set there is a set whose elements are exactly the sets all of whose elements belong to it.
- For every set there is a set whose elements are exactly the elements of its elements.
- The elements of a set that belong to a given class form a set.
- Seven class-existence axioms: the membership relation, intersections, complements and domains of classes, products with the universe, and two permutations of the entries of triples define classes.
The Characteristic Property of Ordered Pairs and Nested Tuples of Sets
lemmalem:ordered-pair-nbg-2026aSet TheoryTwo ordered pairs of sets are equal exactly when their first components and their second components are equal, and likewise two nested tuples of the same length are equal exactly when their entries agree.- The Kuratowski ordered pair of two sets x and y is the set {{x},{x,y}}; nested tuples of n sets are built by pairing the tuple of the first n-1 entries with the last.
The Empty Set, the Unordered Pair and the Singleton
definitiondef:empty-set-pair-singleton-nbg-2026aSet TheoryThe empty set is the unique set with no elements; the unordered pair of two sets is the unique set whose elements are exactly those two; the singleton of a set is the pair of the set with itself.Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique
lemmalem:empty-set-pair-unique-nbg-2026aSet TheoryEvery element of a class is a set; there is exactly one set with no elements, and every class with no elements equals it; and for any two sets there is exactly one set whose elements are exactly those two.