Proof of Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection

By Equivalence Relations on a Set §equivalence, $R$ is reflexive, symmetric and transitive; these are meant below by reflexivity, symmetry and transitivity. Unfolding the class abstractions once by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted: by The Equivalence Class of an Element under an Equivalence Relation §class, for $u\in a$ and every set $w$, $w\in[u]_{R}$ if and only if $w\in a$ and $u\,R\,w$; and by The Quotient of a Set by an Equivalence Relation and the Canonical Projection §quotient, a set $c$ is an element of $a/R$ if and only if $c=[u]_{R}$ for some $u\in a$.

(i) For $u\in a$, reflexivity gives $u\,R\,u$, so $u\in[u]_{R}$.

Equal. Let $u,v\in a$. Suppose $[u]_{R}=[v]_{R}$. By (i), $v\in[v]_{R}=[u]_{R}$, hence $u\,R\,v$. Conversely suppose $u\,R\,v$; by symmetry also $v\,R\,u$. If $w\in[v]_{R}$, then $w\in a$ and $v\,R\,w$, so $u\,R\,w$ by transitivity from $u\,R\,v$, and $w\in[u]_{R}$. If $w\in[u]_{R}$, then $w\in a$ and $u\,R\,w$, so $v\,R\,w$ by transitivity from $v\,R\,u$, and $w\in[v]_{R}$. By Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, $[u]_{R}=[v]_{R}$.

Disjoint. Let $u,v\in a$ with $[u]_{R}\neq[v]_{R}$, and suppose, for a contradiction, that the intersection $[u]_{R}\cap[v]_{R}$ has an element $w$. Then $w\in a$, $u\,R\,w$ and $v\,R\,w$; by symmetry $w\,R\,v$, and by transitivity $u\,R\,v$. By the Equal part above, $[u]_{R}=[v]_{R}$, a contradiction. So $[u]_{R}\cap[v]_{R}$ has no element, and the two classes are disjoint by The Boolean Operations on Classes, Disjointness, and the Universal Class §disjoint.

Quotient-set. Let $c\in a/R$. Then there is $u\in a$ with $c=[u]_{R}$, and every element of $[u]_{R}$ lies in $a$, so $c$ is a subset of $a$; hence $c\in\mathcal{P}(a)$ by The Union Set and the Power Set of a Set §power. Thus $a/R\subseteq\mathcal{P}(a)$, and since $\mathcal{P}(a)$ is a set by The Union Set and the Power Set of a Set §power, $a/R$ 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 §subclass.

Cover. For $u\in a$, $u\in[u]_{R}$ by (i). Since $a/R$ is a set by the Quotient-set part, its union set $\bigcup(a/R)$ is defined, and by The Union Set and the Power Set of a Set §union a set $w$ is an element of it if and only if $w\in c$ for some $c\in a/R$. If $w\in c$ with $c\in a/R$, then $c=[u]_{R}$ for some $u\in a$, so $w\in a$. Conversely, if $w\in a$, then $w\in[w]_{R}$ by (i) and $[w]_{R}\in a/R$, so $w\in\bigcup(a/R)$. By Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, $\bigcup(a/R)=a$. Finally, every $c\in a/R$ is $[u]_{R}$ for some $u\in a$, and $u\in c$ by (i).

Representative. Let $c\in a/R$ and $u\in c$. Then $c=[v]_{R}$ for some $v\in a$, and $u\in[v]_{R}$ gives $u\in a$ and $v\,R\,u$. By the Equal part above, $[v]_{R}=[u]_{R}$, that is, $c=[u]_{R}$.

Projection. By The Quotient of a Set by an Equivalence Relation and the Canonical Projection §projection, every element of $\pi_{R}$ is an ordered pair $(u,[u]_{R})$ with $u\in a$, so $\pi_{R}$ is a relation by Relations, Domain, Range, Inverse and Composition §relation. Moreover, for sets $u$ and $c$: if $(u,c)\in\pi_{R}$ then there is $u'\in a$ with $(u,c)=(u',[u']_{R})$, so $u=u'\in a$ and $c=[u]_{R}$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic; conversely, if $u\in a$ then $(u,[u]_{R})\in\pi_{R}$. That is,

$$(u,c)\in\pi_{R}\quad\text{if and only if}\quad u\in a\text{ and }c=[u]_{R}.\qquad(\ast)$$

Function. If $(u,c)\in\pi_{R}$ and $(u,c')\in\pi_{R}$, then $c=[u]_{R}=c'$ by $(\ast)$; so $\pi_{R}$ is a function by Functions, Values of a Function, and Functions from One Class to Another §function. Domain. By $(\ast)$ and Relations, Domain, Range, Inverse and Composition §domain, a set $u$ is in $\operatorname{dom}\pi_{R}$ if and only if $u\in a$; by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, $\operatorname{dom}\pi_{R}=a$. Values. For $u\in a$, $(u,[u]_{R})\in\pi_{R}$, so $\pi_{R}(u)=[u]_{R}$ by Functions, Values of a Function, and Functions from One Class to Another §value. Range. By $(\ast)$ and Relations, Domain, Range, Inverse and Composition §range, a set $c$ is in $\operatorname{ran}\pi_{R}$ if and only if $c=[u]_{R}$ for some $u\in a$, that is, if and only if $c\in a/R$; by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, $\operatorname{ran}\pi_{R}=a/R$. In particular $\operatorname{ran}\pi_{R}\subseteq a/R$, so $\pi_{R}:a\to a/R$ by Functions, Values of a Function, and Functions from One Class to Another §map. Surjective. Every element of $a/R$ is of the form $[u]_{R}=\pi_{R}(u)$ with $u\in a$, and $\operatorname{ran}\pi_{R}=a/R$; so $\pi_{R}$ is surjective onto $a/R$ by Injective, Surjective and Bijective Functions between Classes §surjective.