Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- Defines a well-order on a set as a total order on it in which every subset with at least one element has a least element.
- Defines the image R[A] of a class A under a class R, and the preimage F^{-1}[B] of a class B under a class F as the image of B under the inverse relation of F.
Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders
lemmalem:partial-order-nbg-2026aSet TheoryFor a partial order on a set: a subclass has at most one least and one greatest element; the strict relation is characterized by u <= v and u != v, is irreflexive and transitive, and u <= v iff u < v or u = v; for a total order, trichotomy holds and the negation of u <= v is v <…Partial and Total Orders on a Set and the Associated Strict Relation
definitiondef:partial-order-nbg-2026aSet TheoryDefines partial orders (reflexive, antisymmetric, transitive relations on a set), total orders, and the strict relation associated with a partial order.Functions, Values of a Function, and Functions from One Class to Another
definitiondef:function-nbg-2026aSet TheoryDefines a function as a single-valued relation, its value F(u) at a point u of its domain, and functions (maps) F:A→B from a class A to a class B.- Defines a relation as a class of ordered pairs, and the domain, range, inverse and composition of classes regarded as relations, together with relations on a class.
Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection
lemmalem:equivalence-classes-nbg-2026aSet TheoryFor an equivalence relation R on a set a: classes are equal iff their elements are related, distinct classes are disjoint, the nonempty classes cover a and each is the class of any of its elements, the quotient a/R is a set, and the canonical projection is a surjection from a ont…- Defines the Cartesian product X×Y of two classes as the class of all ordered pairs (u,v) with u in X and v in Y.
- Defines an equivalence relation on a set as a reflexive, symmetric and transitive relation on it.
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.