Proof of Sethood and Subclasses: Bookkeeping

Throughout, every element of a class is a set by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i), so membership in a class term is read off from Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i).

Intervals. Let $m,n\in\mathbb{N}_{0}$. By Intervals of Natural Numbers (i),

$$\{m,\dots,n\}=\{k\in\mathbb{N}_{0}:m\le k\le n\},$$

which is the class $\{k:k\in\mathbb{N}_{0}\wedge m\le k\le n\}$ of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (ii). Every element $k$ of it therefore satisfies $k\in\mathbb{N}_{0}$, so $\{m,\dots,n\}\subseteq\mathbb{N}_{0}$ by Subclasses and Subsets (i). Since $\mathbb{N}_{0}$ is a set (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii)), $\{m,\dots,n\}$ is a set by 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 (i). This proves (i).

Subclasses of a class containing $A\cup\{b\}$. Let $A$ and $C$ be classes, $b$ a set, and suppose $A\cup\{b\}\subseteq C$. If $u\in A$, then $u\in A\cup\{b\}$ by The Boolean Operations on Classes, Disjointness, and the Universal Class (i), hence $u\in C$ by Subclasses and Subsets (i); thus $A\subseteq C$. Since $b$ is a set, $b\in\{b\}$ by The Empty Set, the Unordered Pair and the Singleton (iii), so $b\in A\cup\{b\}$ by The Boolean Operations on Classes, Disjointness, and the Universal Class (i), and therefore $b\in C$. This proves (ii).