Proof of Compatible Operations, Maps and Relations Pass to the Quotient

Throughout, $[u]$ is the equivalence class of $u\in a$, and $u\,R\,v$ means $(u,v)\in R$ as in Relations, Domain, Range, Inverse and Composition §relation. We use three facts repeatedly. First, by The Quotient of a Set by an Equivalence Relation and the Canonical Projection §quotient and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, a set $c$ lies in $a/R$ if and only if $c=[u]$ for some $u\in a$. Second, by Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection §equal, for all $u,v\in a$ we have $[u]=[v]$ if and only if $u\,R\,v$. Third, by The Cartesian Product of Two Classes §product and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, a set $x$ lies in $(a/R)\times(a/R)$ if and only if $x=(c,d)$ for some $c,d\in a/R$, that is, by the first fact, if and only if $x=([u],[v])$ for some $u,v\in a$. By Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection §quotient-set, $a/R$ is a set.

Proof of the clause operation above. Construction. For $u,v\in a$ the value $u\ast v$ exists and lies in $a$ by Binary Operations on a Set §notation, so $[u\ast v]$ is defined. Let

$$\circledast=\{p:\exists x\,\exists w\,\exists u\,\exists v\,(p=(x,w)\wedge u\in a\wedge v\in a\wedge x=([u],[v])\wedge w=[u\ast v])\},$$

formed by class abstraction with the parameters $a$, $R$ and $\ast$; its formula quantifies over set variables only, the ordered pair, $[u]$, $[v]$, $u\ast v$ and $[u\ast v]$ being defined set symbols used under the hypotheses $u\in a$ and $v\in a$, 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 $x$ and $w$,

$$(x,w)\in\circledast\quad\text{if and only if}\quad\text{there are }u,v\in a\text{ with }x=([u],[v])\text{ and }w=[u\ast v].\qquad(1)$$

Function. Every element of $\circledast$ is an ordered pair, so $\circledast$ is a relation by Relations, Domain, Range, Inverse and Composition §relation. Let $(x,w)\in\circledast$ and $(x,w')\in\circledast$. By (1) there are $u,v,u',v'\in a$ with $x=([u],[v])=([u'],[v'])$, $w=[u\ast v]$ and $w'=[u'\ast v']$. By The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, $[u]=[u']$ and $[v]=[v']$, so $u\,R\,u'$ and $v\,R\,v'$ by Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection §equal. By the hypothesis on $\ast$, $(u\ast v)\,R\,(u'\ast v')$; as $u\ast v$ and $u'\ast v'$ lie in $a$, Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection §equal gives $[u\ast v]=[u'\ast v']$, that is, $w=w'$. Hence $\circledast$ 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 (1), a set $x$ lies in $\operatorname{dom}\circledast$ if and only if there are a set $w$ and $u,v\in a$ with $x=([u],[v])$ and $w=[u\ast v]$; since $[u\ast v]$ exists for all $u,v\in a$, this holds if and only if $x=([u],[v])$ for some $u,v\in a$, that is, by the third fact above, if and only if $x\in(a/R)\times(a/R)$. By Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, $\operatorname{dom}\circledast=(a/R)\times(a/R)$.

Range. Let $w\in\operatorname{ran}\circledast$. By Relations, Domain, Range, Inverse and Composition §range and (1), $w=[u\ast v]$ for some $u,v\in a$; since $u\ast v\in a$, $w\in a/R$ by the first fact above. Thus $\operatorname{ran}\circledast\subseteq a/R$, so $\circledast:(a/R)\times(a/R)\to a/R$ by Functions, Values of a Function, and Functions from One Class to Another §map, and $\circledast$ is a binary operation on the set $a/R$ by Binary Operations on a Set §operation.

Values. Let $u,v\in a$. Then $[u],[v]\in a/R$, and $(([u],[v]),[u\ast v])\in\circledast$ by (1), so by Binary Operations on a Set §notation and Functions, Values of a Function, and Functions from One Class to Another §value, $[u]\circledast[v]=\circledast(([u],[v]))=[u\ast v]$.

Uniqueness. Let $\circledast'$ be a binary operation on $a/R$ with $[u]\circledast'[v]=[u\ast v]$ for all $u,v\in a$. By Binary Operations on a Set §operation and Functions, Values of a Function, and Functions from One Class to Another §map, $\operatorname{dom}\circledast'=(a/R)\times(a/R)=\operatorname{dom}\circledast$. Let $x\in\operatorname{dom}\circledast$; by the third fact above, $x=([u],[v])$ for some $u,v\in a$, and then, by Binary Operations on a Set §notation, $\circledast'(x)=[u]\circledast'[v]=[u\ast v]=[u]\circledast[v]=\circledast(x)$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality, $\circledast'=\circledast$.

Proof of the clause map above. Construction. By Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection §projection, the canonical projection is a map $\pi_{R}:a\to a/R$ with $\pi_{R}(u)=[u]$ for every $u\in a$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, applied to $F:a\to a$ and $\pi_{R}:a\to a/R$, the composition is a map $P=\pi_{R}\circ F:a\to a/R$ with $P(u)=\pi_{R}(F(u))=[F(u)]$ for every $u\in a$, using $F(u)\in a$ by Functions, Values of a Function, and Functions from One Class to Another §map. Let $u,u'\in a$ with $u\,R\,u'$. By the hypothesis on $F$, $F(u)\,R\,F(u')$, and since $F(u),F(u')\in a$, Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection §equal gives $[F(u)]=[F(u')]$, that is, $P(u)=P(u')$. As $a/R$ is a set, A Map Constant on Equivalence Classes Factors Uniquely through the Quotient §factorization, applied with $b=a/R$ and the map $P$, gives exactly one map $\bar F:a/R\to a/R$ with $\bar F\circ\pi_{R}=P$.

Function, domain and range. $\bar F$ is a map from $a/R$ to $a/R$, so by Functions, Values of a Function, and Functions from One Class to Another §map it is a function with $\operatorname{dom}\bar F=a/R$ and $\operatorname{ran}\bar F\subseteq a/R$.

Values. Let $u\in a$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, applied to $\pi_{R}:a\to a/R$ and $\bar F:a/R\to a/R$, $\bar F([u])=\bar F(\pi_{R}(u))=(\bar F\circ\pi_{R})(u)=P(u)=[F(u)]$.

Uniqueness. Let $H:a/R\to a/R$ be a map with $H([u])=[F(u)]$ for every $u\in a$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, $H\circ\pi_{R}:a\to a/R$ is a map with $(H\circ\pi_{R})(u)=H([u])=[F(u)]=P(u)$ for every $u\in a$. Both $H\circ\pi_{R}$ and $P$ have domain $a$ by Functions, Values of a Function, and Functions from One Class to Another §map, so $H\circ\pi_{R}=P$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. By the uniqueness in A Map Constant on Equivalence Classes Factors Uniquely through the Quotient §factorization, $H=\bar F$.

Proof of the clause relation above. Construction. Let

$$\bar T=\{p:\exists c\,\exists d\,\exists u\,\exists v\,(p=(c,d)\wedge u\in a\wedge v\in a\wedge c=[u]\wedge d=[v]\wedge(u,v)\in T)\},$$

formed by class abstraction with the parameters $a$, $R$ and $T$; its formula quantifies over set variables only, the ordered pair, $[u]$ and $[v]$ being defined set symbols used under the hypotheses $u\in a$ and $v\in a$, 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 $d$,

$$(c,d)\in\bar T\quad\text{if and only if}\quad\text{there are }u,v\in a\text{ with }c=[u],\ d=[v]\text{ and }(u,v)\in T.\qquad(2)$$

Relation on $a/R$. Every element of $\bar T$ is an ordered pair, so $\bar T$ is a relation by Relations, Domain, Range, Inverse and Composition §relation. Let $p\in\bar T$; then $p=(c,d)$ with $c=[u]$ and $d=[v]$ for some $u,v\in a$, so $c,d\in a/R$ by the first fact above, and $p\in(a/R)\times(a/R)$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership. Thus $\bar T$ is a subclass of $(a/R)\times(a/R)$ by Subclasses and Subsets §subclass, and $\bar T$ is a relation on $a/R$ by Relations, Domain, Range, Inverse and Composition §on.

Characterization. Let $u,v\in a$. If $(u,v)\in T$, then $([u],[v])\in\bar T$ by (2). Conversely, let $([u],[v])\in\bar T$. By (2) there are $u',v'\in a$ with $[u]=[u']$, $[v]=[v']$ and $(u',v')\in T$. 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'$ and $v\,R\,v'$, so the hypothesis on $T$ gives $(u,v)\in T$ if and only if $(u',v')\in T$; hence $(u,v)\in T$.

Uniqueness. Let $S$ and $S'$ be relations on $a/R$ such that, for all $u,v\in a$, $([u],[v])\in S$ if and only if $(u,v)\in T$, and likewise for $S'$. Let $p\in S$. Since $S\subseteq(a/R)\times(a/R)$ by Relations, Domain, Range, Inverse and Composition §on, the third fact above gives $p=([u],[v])$ for some $u,v\in a$; then $(u,v)\in T$, so $p\in S'$. By symmetry every element of $S'$ lies in $S$, so $S=S'$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality. Applied with $S'=\bar T$, this shows that $\bar T$ is the only relation on $a/R$ with the stated property.