Proof of A Map Constant on Equivalence Classes Factors Uniquely through the Quotient

For $u\in a$, $[u]_{R}$ denotes the equivalence class of $u$, and $u\,R\,v$ means $(u,v)\in R$ as in Relations, Domain, Range, Inverse and Composition §relation. By Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection §projection, $\pi_{R}$ is a surjective map $\pi_{R}:a\to a/R$ with $\pi_{R}(u)=[u]_{R}$ for every $u\in a$. By Functions, Values of a Function, and Functions from One Class to Another §map, $\operatorname{dom}F=a$, so $F(u)$ is defined for every $u\in a$, and by Functions, Values of a Function, and Functions from One Class to Another §value it is the unique set $w$ with $(u,w)\in F$.

Construction. Let

$$G=\{p:\exists c\,\exists w\,\exists u\,(p=(c,w)\wedge u\in a\wedge c=[u]_{R}\wedge w=F(u))\},$$

formed by class abstraction with the parameters $a$, $R$ and $F$; its formula quantifies over set variables only, the ordered pair, $[u]_{R}$ and $F(u)$ being defined set symbols, so it is predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires. By Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction and The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, for all sets $c$ and $w$,

$$(c,w)\in G\quad\text{if and only if}\quad\text{there is }u\in a\text{ with }c=[u]_{R}\text{ and }w=F(u).\qquad(\ast)$$

$G$ is a function. Every element of $G$ is an ordered pair, so $G$ is a relation by Relations, Domain, Range, Inverse and Composition §relation. Let $(c,w)\in G$ and $(c,w')\in G$. By $(\ast)$ there are $u,u'\in a$ with $c=[u]_{R}=[u']_{R}$, $w=F(u)$ and $w'=F(u')$. By Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection §equal, $u\,R\,u'$, so $F(u)=F(u')$ by the hypothesis on $F$, that is, $w=w'$. Hence $G$ is a function by Functions, Values of a Function, and Functions from One Class to Another §function.

Domain. By Relations, Domain, Range, Inverse and Composition §domain and $(\ast)$, a set $c$ lies in $\operatorname{dom}G$ if and only if there are a set $w$ and some $u\in a$ with $c=[u]_{R}$ and $w=F(u)$; since $F(u)$ exists for every $u\in a$, this holds if and only if $c=[u]_{R}$ for some $u\in a$, that is, by The Quotient of a Set by an Equivalence Relation and the Canonical Projection §quotient, if and only if $c\in a/R$. By Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, $\operatorname{dom}G=a/R$.

Range. Let $w\in\operatorname{ran}G$. By Relations, Domain, Range, Inverse and Composition §range and $(\ast)$, $w=F(u)$ for some $u\in a$. Since $(u,F(u))\in F$, $w\in\operatorname{ran}F$ by Relations, Domain, Range, Inverse and Composition §range, and $\operatorname{ran}F\subseteq b$ by Functions, Values of a Function, and Functions from One Class to Another §map; so $w\in b$. Thus $\operatorname{ran}G\subseteq b$, and $G:a/R\to b$ by Functions, Values of a Function, and Functions from One Class to Another §map.

Values. For $u\in a$, $([u]_{R},F(u))\in G$ by $(\ast)$, so $G([u]_{R})=F(u)$ by Functions, Values of a Function, and Functions from One Class to Another §value.

Factorization. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, applied to $\pi_{R}:a\to a/R$ and $G:a/R\to b$, the composition is a map $G\circ\pi_{R}:a\to b$ with $(G\circ\pi_{R})(u)=G(\pi_{R}(u))=G([u]_{R})=F(u)$ for every $u\in a$. As $\operatorname{dom}(G\circ\pi_{R})=a=\operatorname{dom}F$ by Functions, Values of a Function, and Functions from One Class to Another §map, Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality gives $G\circ\pi_{R}=F$.

Uniqueness. Let $G':a/R\to b$ be a map with $G'\circ\pi_{R}=F$. Let $c\in a/R$. Since $\pi_{R}$ is surjective, there is $u\in a$ with $\pi_{R}(u)=c$, by Injective, Surjective and Bijective Functions between Classes §surjective. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, $G'(c)=G'(\pi_{R}(u))=(G'\circ\pi_{R})(u)=F(u)$, and likewise $G(c)=(G\circ\pi_{R})(u)=F(u)$; so $G'(c)=G(c)$. Since $\operatorname{dom}G'=a/R=\operatorname{dom}G$ by Functions, Values of a Function, and Functions from One Class to Another §map, Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality gives $G'=G$. Hence $G$ is the only map from $a/R$ to $b$ with $G\circ\pi_{R}=F$.