Proof of Gluing Maps on Disjoint Domains, and Shrinking the Codomain

Throughout, a map $F:A\to X$ is a function with domain $A$ and range contained in $X$ (Functions, Values of a Function, and Functions from One Class to Another (iii)); for $u$ in its domain, $F(u)=v$ if and only if $(u,v)\in F$ (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x)); and the union of two relations is a relation, whose domain and range are the unions of their domains and of their ranges.

Gluing. Let $(u,v)$ and $(u,v')$ be elements of $f\cup g$. If both lie in $f$, or both in $g$, then $v=v'$, as $f$ and $g$ are functions. A pair in $f$ and a pair in $g$ cannot have the same first component $u$, since $u$ would lie in $A$ and in $C$ by Domains and Restrictions of Maps (i), while $A\cap C=\emptyset$. So $f\cup g$ is a function with domain $A\cup C$ and range $\operatorname{ran}f\cup\operatorname{ran}g\subseteq X$, that is, a map $f\cup g:A\cup C\to X$. For $x\in A$ we have $(x,f(x))\in f\subseteq f\cup g$, so $(f\cup g)(x)=f(x)$; likewise $(f\cup g)(x)=g(x)$ for $x\in C$. This proves (i).

Gluing bijections. Write $h=f\cup g$. Since $f$ and $g$ take values in $B\cup D$, they are maps $f:A\to B\cup D$ and $g:C\to B\cup D$ by Membership in Inverse Relations, Preimages and Images of Classes, and Enlarging the Codomain of a Map (v), so $h:A\cup C\to B\cup D$ is a map by (i), with $h=f$ on $A$ and $h=g$ on $C$.

$h$ is injective: let $u,u'\in A\cup C$ with $h(u)=h(u')$. If $u,u'\in A$, then $f(u)=f(u')$, so $u=u'$ as $f$ is injective; likewise if $u,u'\in C$. If $u\in A$ and $u'\in C$, then $h(u)=f(u)\in B$ and $h(u')=g(u')\in D$, which is impossible as $B\cap D=\emptyset$; the case $u\in C$, $u'\in A$ is the same.

$h$ is surjective: an element of $B$ is $f(a)=h(a)$ for some $a\in A$, and an element of $D$ is $g(x)=h(x)$ for some $x\in C$, as $f$ and $g$ are surjective.

Hence $h$ is a bijection, which proves (ii).

Shrinking the codomain. For $u\in A$ we have $(u,f(u))\in f$, so $f(u)\in f(A)\subseteq Y$ by The Image and the Preimage of a Class under a Class (i); hence $f:A\to Y$ is a map by Membership in Inverse Relations, Preimages and Images of Classes, and Enlarging the Codomain of a Map (v). Taking $Y=f(A)$, the map $f:A\to f(A)$ is surjective: by The Image and the Preimage of a Class under a Class (i), every $v\in f(A)$ satisfies $(u,v)\in f$ for some $u\in A$, that is, $v=f(u)$. Injectivity does not involve the codomain (Injective, Surjective and Bijective Functions between Classes (i)), so if $f$ is injective, then $f:A\to f(A)$ is a bijection. This proves (iii).