Proof of Membership in Inverse Relations, Preimages and Images of Classes, and Enlarging the Codomain of a Map

Throughout, every element of a class is a set (Class Theory NBG: the Axioms, Standing Conventions and Basic Notation (i)), and for a set $u$, membership of $u$ in a class $\{x:\varphi(x)\}$ formed by class abstraction means $\varphi(u)$; the inverse, the domain, the range and the image are all formed in this way. Likewise, a map $F:A\to B$ is a function with $\operatorname{dom}F=A$ and $\operatorname{ran}F\subseteq B$ (Functions, Values of a Function, and Functions from One Class to Another (iii)); a set $x$ lies in the domain $\operatorname{dom}F$ exactly when $(x,v)\in F$ for some set $v$; and for $x\in\operatorname{dom}F$ the value $F(x)$ is the unique set $v$ with $(x,v)\in F$ (Functions, Values of a Function, and Functions from One Class to Another (ii)).

Inverse. Let $x$ and $y$ be sets. By the definition of the inverse in Relations, Domain, Range, Inverse and Composition (iv), $(x,y)\in R^{-1}$ means that there are sets $u$ and $v$ with $(u,v)\in R$ and $(x,y)=(v,u)$. If $(y,x)\in R$, the sets $u=y$ and $v=x$ witness this. Conversely, if $u$ and $v$ are such sets, then $x=v$ and $y=u$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets (i), so $(y,x)=(u,v)\in R$. This proves (i).

Preimage. By The Image and the Preimage of a Class under a Class (ii), $R^{-1}[C]$ is the image of $C$ under $R^{-1}$, so by The Image and the Preimage of a Class under a Class (i) a set $x$ lies in $R^{-1}[C]$ if and only if there is a set $w$ with $w\in C$ and $(w,x)\in R^{-1}$. By (i), $(w,x)\in R^{-1}$ holds if and only if $(x,w)\in R$, which gives (ii).

Preimage under a map. Let $F:A\to B$ be a map and let $x$ be a set. Suppose first that $x\in F^{-1}[C]$. By (ii), applied with $F$ in place of $R$, there is a set $w\in C$ with $(x,w)\in F$. Then $x\in\operatorname{dom}F=A$, and $F(x)=w\in C$ since $F(x)$ is the unique set paired with $x$ in $F$. Conversely, suppose $x\in A$ and $F(x)\in C$. Then $x\in\operatorname{dom}F$, so $(x,F(x))\in F$, and $w=F(x)$ is a set in $C$ with $(x,w)\in F$; hence $x\in F^{-1}[C]$ by (ii). This proves (iii).

Image. Let $F:A\to B$ be a map. Its range is $\operatorname{ran}F=F[A]$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (v), and $\operatorname{ran}F\subseteq B$ by Functions, Values of a Function, and Functions from One Class to Another (iii). Hence $F[A]\subseteq B$, which proves (iv).

Codomain. Let $F:A\to B$ be a map with $F(u)\in D$ for every $u\in A$. Since $F$ is a function with $\operatorname{dom}F=A$, it remains to show $\operatorname{ran}F\subseteq D$. Let $v\in\operatorname{ran}F$. By Relations, Domain, Range, Inverse and Composition (iii) there is a set $u$ with $(u,v)\in F$. Then $u\in\operatorname{dom}F=A$, and $v=F(u)$ because $F(u)$ is the unique set paired with $u$ in $F$. Hence $v\in D$ by hypothesis. Thus $F$ is a function with $\operatorname{dom}F=A$ and $\operatorname{ran}F\subseteq D$, that is, $F:A\to D$ is a map, which proves (v).