Proof of Maps and Relations Given by Formulas

Like The Class Comprehension Theorem for Predicative Formulas, the lemma is a scheme, with one instance for each expression $t$ or formula $\varphi$. By Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols, an expression stands for the formula obtained by eliminating its abbreviations, and each elimination step replaces an atomic part by a predicative formula; for a defined set symbol it replaces an atomic part $\alpha(t)$ by $\exists z\,(\theta\wedge\alpha(z))$ with $\theta$ predicative and $z$ a set variable. So an expression that quantifies over set variables only stands for a predicative formula. The parameters of $t$ and $\varphi$, sets or classes, remain free in them and are parameters of the class abstractions below.

The clause map above. Let

$$f=\{p:\exists u\,(u\in a\wedge p=(u,t(u)))\},$$

formed by class abstraction with the parameter $a$ and the parameters of $t$. Its formula quantifies over set variables only; the ordered pair and $t(u)$ are defined set symbols, and $t(u)$ is used properly, since it occurs only under the conjunct $u\in a$, for which it is defined by hypothesis. So the formula 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, for sets $u$ and $y$, $(u,y)\in f$ holds if and only if there is $u'\in a$ with $(u,y)=(u',t(u'))$, that is, by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, with $u=u'$ and $y=t(u')$. Hence, for all sets $u$ and $y$,

$$(u,y)\in f\quad\text{if and only if}\quad u\in a\text{ and }y=t(u).\qquad(\ast)$$

Every element of $f$ is a pair $(u,t(u))$ with $u\in a$, so $f$ is a relation by Relations, Domain, Range, Inverse and Composition §relation. If $(u,y)\in f$ and $(u,y')\in f$, then $y=t(u)=y'$ by $(\ast)$. Hence $f$ is a function by Functions, Values of a Function, and Functions from One Class to Another §function.

By Relations, Domain, Range, Inverse and Composition §domain and $(\ast)$, a set $u$ lies in $\operatorname{dom}f$ if and only if $u\in a$ and some set $y$ equals $t(u)$; since $t(u)$ is a set for every $u\in a$, this holds if and only if $u\in a$. By Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, $\operatorname{dom}f=a$. If $y\in\operatorname{ran}f$, then by Relations, Domain, Range, Inverse and Composition §range and $(\ast)$ there is $u\in a$ with $y=t(u)$, so $y\in b$ by hypothesis. Thus $\operatorname{ran}f\subseteq b$ by Subclasses and Subsets §subclass, and $f:a\to b$ by Functions, Values of a Function, and Functions from One Class to Another §map. For $u\in a$, $(u,t(u))\in f$ by $(\ast)$, so $f(u)=t(u)$ by Functions, Values of a Function, and Functions from One Class to Another §value.

The class $f$ is moreover a set, as the lower-case letter requires under Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §notation: each element $(u,t(u))$ of $f$ has $u\in a$ and $t(u)\in b$, so it lies in the Cartesian product $a\times b$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership; thus $f\subseteq a\times b$, where $a\times b$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set, and $f$ 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.

Uniqueness: let $g:a\to b$ be a map with $g(u)=t(u)$ for every $u\in a$. Then $\operatorname{dom}g=a=\operatorname{dom}f$ by Functions, Values of a Function, and Functions from One Class to Another §map, and $g(u)=t(u)=f(u)$ for every $u\in a$, so $g=f$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality.

The clause binary above. We argue as in the clause map above, forming the map directly so that the abstraction uses $t(v,w)$ only for $v\in c$ and $w\in d$. Let

$$f=\{p:\exists v\,\exists w\,(v\in c\wedge w\in d\wedge p=((v,w),t(v,w)))\},$$

formed by class abstraction with the parameters $c$, $d$ and those of $t$. As before its formula is predicative: it quantifies over set variables only, and $t(v,w)$ occurs only under the conjuncts $v\in c$ and $w\in d$, for which it is defined by hypothesis. 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 $q$ and $y$,

$$(q,y)\in f\quad\text{if and only if}\quad\text{there are }v\in c\text{ and }w\in d\text{ with }q=(v,w)\text{ and }y=t(v,w).\qquad(\ast\ast)$$

Every element of $f$ is an ordered pair, so $f$ is a relation by Relations, Domain, Range, Inverse and Composition §relation. If $(q,y)\in f$ and $(q,y')\in f$, then by $(\ast\ast)$ there are $v,v'\in c$ and $w,w'\in d$ with $q=(v,w)=(v',w')$, $y=t(v,w)$ and $y'=t(v',w')$; by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, $v=v'$ and $w=w'$, so $y=y'$. Hence $f$ is a function by Functions, Values of a Function, and Functions from One Class to Another §function.

By Relations, Domain, Range, Inverse and Composition §domain and $(\ast\ast)$, since $t(v,w)$ is a set for all $v\in c$ and $w\in d$, a set $q$ lies in $\operatorname{dom}f$ if and only if $q=(v,w)$ for some $v\in c$ and $w\in d$, that is, by The Cartesian Product of Two Classes §product and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, if and only if $q\in c\times d$. By Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, $\operatorname{dom}f=c\times d$. If $y\in\operatorname{ran}f$, then by Relations, Domain, Range, Inverse and Composition §range and $(\ast\ast)$, $y=t(v,w)$ for some $v\in c$ and $w\in d$, so $y\in b$. Thus $\operatorname{ran}f\subseteq b$, and $f:c\times d\to b$ by Functions, Values of a Function, and Functions from One Class to Another §map. For $v\in c$ and $w\in d$, $((v,w),t(v,w))\in f$ by $(\ast\ast)$, so $f((v,w))=t(v,w)$ by Functions, Values of a Function, and Functions from One Class to Another §value.

The class $f$ is a set: for $v\in c$ and $w\in d$, $(v,w)\in c\times d$ and then $((v,w),t(v,w))\in(c\times d)\times b$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, so $f\subseteq(c\times d)\times b$; by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set, applied twice, $(c\times d)\times b$ is a set, and $f$ 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.

Uniqueness: let $g:c\times d\to b$ be a map with $g((v,w))=t(v,w)$ for all $v\in c$ and $w\in d$. Then $\operatorname{dom}g=c\times d=\operatorname{dom}f$ by Functions, Values of a Function, and Functions from One Class to Another §map. Each $q\in c\times d$ is, by The Cartesian Product of Two Classes §product and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, of the form $q=(v,w)$ with $v\in c$ and $w\in d$, so $g(q)=t(v,w)=f(q)$. Hence $g=f$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality.

The clause relation above. Let

$$R=\{p:\exists u\,\exists v\,(u\in a\wedge v\in a\wedge p=(u,v)\wedge\varphi(u,v))\},$$

formed by class abstraction with the parameter $a$ and the parameters of $\varphi$. Its formula is predicative: it quantifies over set variables only, since $\varphi$ does, and the defined set symbols of $\varphi$ are used properly, since $\varphi(u,v)$ occurs only under the conjuncts $u\in a$ and $v\in a$. 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 $u$ and $v$,

$$(u,v)\in R\quad\text{if and only if}\quad u\in a,\ v\in a\text{ and }\varphi(u,v).\qquad(\ast\ast\ast)$$

Every element of $R$ is a pair $(u,v)$ with $u,v\in a$, so $R$ is a relation by Relations, Domain, Range, Inverse and Composition §relation, and each of its elements lies in $a\times a$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership. Thus $R\subseteq a\times a$ by Subclasses and Subsets §subclass, and $R$ is a relation on $a$ by Relations, Domain, Range, Inverse and Composition §on. By $(\ast\ast\ast)$, for all $u,v\in a$, $(u,v)\in R$ if and only if $\varphi(u,v)$.

Uniqueness: let $R'$ be a relation on $a$ such that, for all $u,v\in a$, $(u,v)\in R'$ if and only if $\varphi(u,v)$. Every element $p$ of $R$ or of $R'$ lies in $a\times a$ by Relations, Domain, Range, Inverse and Composition §on and Subclasses and Subsets §subclass, so by The Cartesian Product of Two Classes §product and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction it is of the form $p=(u,v)$ with $u,v\in a$; then $p\in R$ if and only if $\varphi(u,v)$, if and only if $p\in R'$. Hence $R=R'$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality.