Proof of Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction

Throughout, every element of a class is a set by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §objects, and $(a,b)$ is the ordered pair, a set. Membership in a class formed by class abstraction is unfolded by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, a restricted abstraction being first rewritten by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted; class abstractions are unfolded without further mention.

Preliminaries. Let $R$, $S$, $F$ be classes and $a,b$ sets.

(P0) Let $A$ be any class, not only the class fixed in the statement. By Relations, Domain, Range, Inverse and Composition §inverse, Relations, Domain, Range, Inverse and Composition §composition, The Identity on a Class §identity and The Restriction of a Function or Relation to a Class §restriction, every element of $R^{-1}$, $S\circ R$, $\mathrm{id}_{A}$ and $F|_{A}$ is an ordered pair, so each is a relation. Moreover, applying The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic to the equation between pairs in each defining formula: $(a,b)\in R^{-1}$ if and only if $(b,a)\in R$; $(a,b)\in S\circ R$ if and only if there is a set $v$ with $(a,v)\in R$ and $(v,b)\in S$; $(a,b)\in\mathrm{id}_{A}$ if and only if $a\in A$ and $b=a$; and $(a,b)\in F|_{A}$ if and only if $(a,b)\in F$ and $a\in A$.

(P1) Let $F$ be a function. Then $(a,b)\in F$ if and only if $a\in\operatorname{dom}F$ and $b=F(a)$: if $(a,b)\in F$ then $a\in\operatorname{dom}F$ by Relations, Domain, Range, Inverse and Composition §domain and $b=F(a)$ by Functions, Values of a Function, and Functions from One Class to Another §value; the converse is Functions, Values of a Function, and Functions from One Class to Another §value. In particular, for $a\in\operatorname{dom}F$ we have $(a,F(a))\in F$ and so $F(a)\in\operatorname{ran}F$ by Relations, Domain, Range, Inverse and Composition §range; for a map $F:A\to B$ and $a\in A$ this gives $F(a)\in B$, by Functions, Values of a Function, and Functions from One Class to Another §map and Subclasses and Subsets §subclass.

(P2) If $R$ and $S$ are relations and, for all sets $a,b$, $(a,b)\in R$ if and only if $(a,b)\in S$, then $R=S$: every element of $R$ is a pair $(a,b)$ by Relations, Domain, Range, Inverse and Composition §relation, hence lies in $S$, and symmetrically, so $R=S$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality.

Equality. $F$ and $G$ are relations by Functions, Values of a Function, and Functions from One Class to Another §function. For sets $a,b$, by (P1) and the hypotheses, $(a,b)\in F$ iff $a\in\operatorname{dom}F$ and $b=F(a)$, iff $a\in\operatorname{dom}G$ and $b=G(a)$, iff $(a,b)\in G$. Hence $F=G$ by (P2).

Composition. $G\circ F$ is a relation by (P0). If $(a,c)\in G\circ F$ and $(a,c')\in G\circ F$, (P0) gives sets $b,b'$ with $(a,b),(a,b')\in F$ and $(b,c),(b',c')\in G$; then $b=b'$ and $c=c'$ by Functions, Values of a Function, and Functions from One Class to Another §function for $F$ and for $G$. So $G\circ F$ is a function. If $a\in A=\operatorname{dom}F$, then $(a,F(a))\in F$ and $F(a)\in B=\operatorname{dom}G$ by (P1), so $(F(a),G(F(a)))\in G$ and $(a,G(F(a)))\in G\circ F$ by (P0); thus $a\in\operatorname{dom}(G\circ F)$ and, by (P1), $(G\circ F)(a)=G(F(a))$. Conversely if $(a,c)\in G\circ F$ then $(a,b)\in F$ for some $b$ by (P0), so $a\in\operatorname{dom}F=A$; hence $\operatorname{dom}(G\circ F)=A$ by Relations, Domain, Range, Inverse and Composition §domain and Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality. If $c\in\operatorname{ran}(G\circ F)$ then $(a,c)\in G\circ F$ for some $a$ (Relations, Domain, Range, Inverse and Composition §range), so $(b,c)\in G$ for some $b$ by (P0), and $c\in\operatorname{ran}G\subseteq C$. Hence $G\circ F:A\to C$ by Functions, Values of a Function, and Functions from One Class to Another §map.

Identity. $\mathrm{id}_{A}$ is a relation by (P0); if $(a,b),(a,b')\in\mathrm{id}_{A}$ then $b=a=b'$ by (P0), so it is a function. For a set $a$: if $a\in A$ then $(a,a)\in\mathrm{id}_{A}$, and if $(a,b)\in\mathrm{id}_{A}$ then $a\in A$ and $b=a\in A$, by (P0). Thus $\operatorname{dom}\mathrm{id}_{A}=A$ and $\operatorname{ran}\mathrm{id}_{A}\subseteq A$ (Relations, Domain, Range, Inverse and Composition §domain, Relations, Domain, Range, Inverse and Composition §range, Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality), so $\mathrm{id}_{A}:A\to A$, and $\mathrm{id}_{A}(a)=a$ for $a\in A$ by (P1). It is injective, since $\mathrm{id}_{A}(a)=\mathrm{id}_{A}(a')$ means $a=a'$ (Injective, Surjective and Bijective Functions between Classes §injective), and surjective, since each $v\in A$ equals $\mathrm{id}_{A}(v)$ (Injective, Surjective and Bijective Functions between Classes §surjective); so it is bijective by Injective, Surjective and Bijective Functions between Classes §bijective.

Identity-neutral. Let $F:A\to B$. By the clause composition above, $F\circ\mathrm{id}_{A}:A\to B$ and $\mathrm{id}_{B}\circ F:A\to B$, and by the clauses composition and identity above (the latter for $A$ and for $B$), $(F\circ\mathrm{id}_{A})(a)=F(\mathrm{id}_{A}(a))=F(a)$ and $(\mathrm{id}_{B}\circ F)(a)=\mathrm{id}_{B}(F(a))=F(a)$ for $a\in A$, using $F(a)\in B$ from (P1). Both have domain $A=\operatorname{dom}F$, so both equal $F$ by the clause equality above.

Injective-inverse. Let $F:A\to B$ be a map. For a set $b$: $b\in\operatorname{ran}F$ if and only if $(a,b)\in F$ for some set $a$, by Relations, Domain, Range, Inverse and Composition §range; since $(a,b)\in F$ gives $a\in\operatorname{dom}F=A$ by Relations, Domain, Range, Inverse and Composition §domain, this holds if and only if $(a,b)\in F$ for some set $a\in A$, that is, by The Image and the Preimage of a Class under a Class §image, if and only if $b\in F[A]$. Hence $\operatorname{ran}F=F[A]$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality; injectivity was not used.

Now suppose moreover that $F$ is injective. $F^{-1}$ is a relation by (P0). If $(b,a),(b,a')\in F^{-1}$ then $(a,b),(a',b)\in F$ by (P0), so $a,a'\in A$ and $F(a)=b=F(a')$ by (P1), whence $a=a'$ by Injective, Surjective and Bijective Functions between Classes §injective; so $F^{-1}$ is a function. For a set $b$: $b\in\operatorname{dom}F^{-1}$ if and only if $(b,a)\in F^{-1}$ for some set $a$, if and only if $(a,b)\in F$ for some set $a$ by (P0), if and only if $b\in\operatorname{ran}F$, by Relations, Domain, Range, Inverse and Composition §domain and Relations, Domain, Range, Inverse and Composition §range; so $\operatorname{dom}F^{-1}=\operatorname{ran}F$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality. If $a\in\operatorname{ran}F^{-1}$, then $(b,a)\in F^{-1}$ for some set $b$, so $(a,b)\in F$ by (P0) and $a\in\operatorname{dom}F=A$; thus $\operatorname{ran}F^{-1}\subseteq A$ by Subclasses and Subsets §subclass, and $F^{-1}:\operatorname{ran}F\to A$ by Functions, Values of a Function, and Functions from One Class to Another §map.

For $a\in A$, $(a,F(a))\in F$ by (P1), so $(F(a),a)\in F^{-1}$ by (P0); hence $F(a)\in\operatorname{ran}F$ and $F^{-1}(F(a))=a$ by (P1). For $b\in\operatorname{ran}F=\operatorname{dom}F^{-1}$, $(b,F^{-1}(b))\in F^{-1}$ by (P1), so $(F^{-1}(b),b)\in F$ by (P0), and by (P1) we obtain

($*$) $F(F^{-1}(b))=b$ for every set $b\in\operatorname{ran}F$.

Now $F^{-1}$ is injective, since $F^{-1}(b)=F^{-1}(b')$ for $b,b'\in\operatorname{ran}F$ gives $b=F(F^{-1}(b))=F(F^{-1}(b'))=b'$ by ($*$), and surjective onto $A$, since every $a\in A$ equals $F^{-1}(F(a))$ with $F(a)\in\operatorname{ran}F$ (Injective, Surjective and Bijective Functions between Classes §injective, Injective, Surjective and Bijective Functions between Classes §surjective); so it is bijective by Injective, Surjective and Bijective Functions between Classes §bijective.

Inverse. Let $F:A\to B$ be bijective; it is injective and surjective by Injective, Surjective and Bijective Functions between Classes §bijective. First, $\operatorname{ran}F=B$: $\operatorname{ran}F\subseteq B$ by Functions, Values of a Function, and Functions from One Class to Another §map, and every $b\in B$ equals $F(a)$ for some $a\in A$ by Injective, Surjective and Bijective Functions between Classes §surjective, so $b\in\operatorname{ran}F$ by (P1); apply Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality. By the clause injective-inverse above, with $\operatorname{ran}F=B$, $F^{-1}:B\to A$ is a bijective map with $F^{-1}(F(a))=a$ for $a\in A$, and $F(F^{-1}(b))=b$ for $b\in B$ by ($*$). By the clause composition above, $F^{-1}\circ F:A\to A$ with value $F^{-1}(F(a))=a=\mathrm{id}_{A}(a)$, and $F\circ F^{-1}:B\to B$ with value $F(F^{-1}(b))=b=\mathrm{id}_{B}(b)$, using the clause identity above for $A$ and for $B$; as $\mathrm{id}_{A}:A\to A$ and $\mathrm{id}_{B}:B\to B$, the clause equality above gives $F^{-1}\circ F=\mathrm{id}_{A}$ and $F\circ F^{-1}=\mathrm{id}_{B}$.

Inverse-criterion. Let $F:A\to B$ and $G:B\to A$ with $G\circ F=\mathrm{id}_{A}$ and $F\circ G=\mathrm{id}_{B}$. By the clauses composition and identity above, $G(F(a))=\mathrm{id}_{A}(a)=a$ for $a\in A$ and $F(G(b))=\mathrm{id}_{B}(b)=b$ for $b\in B$. If $F(a)=F(a')$ for $a,a'\in A$, then $a=G(F(a))=G(F(a'))=a'$, so $F$ is injective by Injective, Surjective and Bijective Functions between Classes §injective; for $b\in B$, $G(b)\in A$ by (P1) and $F(G(b))=b$, so $F$ is surjective by Injective, Surjective and Bijective Functions between Classes §surjective. Thus $F$ is bijective by Injective, Surjective and Bijective Functions between Classes §bijective, and $F^{-1}:B\to A$ with $F^{-1}(F(a))=a$ for $a\in A$ by the clause inverse above and the clause injective-inverse above. For $b\in B$, $F^{-1}(b)=F^{-1}(F(G(b)))=G(b)$ since $G(b)\in A$. As $\operatorname{dom}F^{-1}=B=\operatorname{dom}G$, the clause equality above gives $G=F^{-1}$.

Preservation. Let $F:A\to B$ and $G:B\to C$; then $G\circ F:A\to C$ and $(G\circ F)(a)=G(F(a))$ by the clause composition above. If $F$ and $G$ are injective and $G(F(a))=G(F(a'))$ for $a,a'\in A$, then $F(a)=F(a')$ because $F(a),F(a')\in B$ by (P1), and so $a=a'$. If $F$ and $G$ are surjective and $c\in C$, there is $b\in B$ with $G(b)=c$ and then $a\in A$ with $F(a)=b$, so $(G\circ F)(a)=c$. The bijective case is the conjunction of the two, by Injective, Surjective and Bijective Functions between Classes §bijective.

Restriction. Let $F$ be a function. $F|_{A}$ is a relation by (P0). If $(a,b),(a,b')\in F|_{A}$ then $(a,b),(a,b')\in F$ by (P0), so $b=b'$; thus $F|_{A}$ is a function. For a set $a$: $a\in\operatorname{dom}(F|_{A})$ iff there is $b$ with $(a,b)\in F|_{A}$, iff $a\in A$ and there is $b$ with $(a,b)\in F$ (by (P0)), iff $a\in A$ and $a\in\operatorname{dom}F$, iff $a\in A\cap\operatorname{dom}F$, using Relations, Domain, Range, Inverse and Composition §domain and The Boolean Operations on Classes, Disjointness, and the Universal Class §operations; hence $\operatorname{dom}(F|_{A})=A\cap\operatorname{dom}F$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality. For $a\in A\cap\operatorname{dom}F$, $(a,F(a))\in F$ by (P1) and $a\in A$, so $(a,F(a))\in F|_{A}$ by (P0), and $(F|_{A})(a)=F(a)$ by (P1).