Proof of Maps Defined by Cases

We work in the setting of Sets and Maps: Ordinary Notation. Fix $A$, $B$, $P$, $t_{1}$ and $t_{2}$ as in the statement.

The two pieces. Let $A_{1}=\{x\in A:P(x)\}$; since $P$ is expressed by a predicative formula, $A_{1}$ is a set by Sets and Maps: Ordinary Notation §set-builder, and by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction a set $x$ lies in $A_{1}$ if and only if $x\in A$ and $P(x)$. Let $A_{2}=A\setminus A_{1}$, a set by Sets and Maps: Ordinary Notation §sets; by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations a set $x$ lies in $A_{2}$ if and only if $x\in A$ and $x\notin A_{1}$, that is, if and only if $x\in A$ and $P(x)$ fails. Hence $A_{1}\subseteq A$, $A_{2}\subseteq A$, no set lies in both $A_{1}$ and $A_{2}$, and every $x\in A$ lies in $A_{1}$ (if $P(x)$) or in $A_{2}$ (if not).

The two partial maps. Every $x\in A_{1}$ is an element of $A$ with $P(x)$, and every $x\in A_{2}$ is an element of $A$ without $P(x)$. Hence, by the hypotheses of the statement, for every $x\in A_{1}$ the symbols in $t_{1}(x)$ are used properly and $t_{1}(x)\in B$, and for every $x\in A_{2}$ the symbols in $t_{2}(x)$ are used properly and $t_{2}(x)\in B$. By Maps and Relations Given by Formulas §map, applied with the sets $A_{1}$ and $B$ and the expression $t_{1}$, and again with $A_{2}$, $B$ and $t_{2}$, there are maps $f_{1}:A_{1}\to B$ and $f_{2}:A_{2}\to B$ with $f_{1}(x)=t_{1}(x)$ for $x\in A_{1}$ and $f_{2}(x)=t_{2}(x)$ for $x\in A_{2}$. By Functions, Values of a Function, and Functions from One Class to Another §map, each $f_{i}$ is a function with $\operatorname{dom}f_{i}=A_{i}$ and $\operatorname{ran}f_{i}\subseteq B$; each $f_{i}$ is a set by Sets and Maps: Ordinary Notation §maps.

The glued map. Let $f=f_{1}\cup f_{2}$, 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 §binary-union; by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations its elements are the sets lying in $f_{1}$ or in $f_{2}$. We check the requirements of Functions, Values of a Function, and Functions from One Class to Another §map for $f:A\to B$.

$f$ is a relation. Every element of $f$ lies in $f_{1}$ or in $f_{2}$, both of which are relations by Functions, Values of a Function, and Functions from One Class to Another §function, so it is an ordered pair; thus $f$ is a relation by Relations, Domain, Range, Inverse and Composition §relation.

A pair in $f_{i}$ has its first component in $A_{i}$. If $(u,v)\in f_{i}$, then $u\in\operatorname{dom}f_{i}=A_{i}$ by Relations, Domain, Range, Inverse and Composition §domain and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction.

$f$ is a function. Let $(u,v)\in f$ and $(u,v')\in f$. If one of these pairs lay in $f_{1}$ and the other in $f_{2}$, then by the previous paragraph $u$ would lie in both $A_{1}$ and $A_{2}$, which is impossible. So both pairs lie in the same $f_{i}$, and $v=v'$ because $f_{i}$ is a function (Functions, Values of a Function, and Functions from One Class to Another §function). Hence $f$ is a function.

$\operatorname{dom}f=A$. If $u\in\operatorname{dom}f$, then by Relations, Domain, Range, Inverse and Composition §domain there is $v$ with $(u,v)\in f$, so $(u,v)\in f_{i}$ for some $i$, whence $u\in A_{i}\subseteq A$. Conversely, let $u\in A$. Then $u\in A_{i}$ for some $i$, so $u\in\operatorname{dom}f_{i}$ and there is $v$ with $(u,v)\in f_{i}\subseteq f$; hence $u\in\operatorname{dom}f$. The two classes have the same elements, so they are equal by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, in force by Sets and Maps: Ordinary Notation §base.

$\operatorname{ran}f\subseteq B$. If $v\in\operatorname{ran}f$, then by Relations, Domain, Range, Inverse and Composition §range there is $u$ with $(u,v)\in f$, so $(u,v)\in f_{i}$ for some $i$, whence $v\in\operatorname{ran}f_{i}\subseteq B$ (Subclasses and Subsets §subclass).

Thus $f:A\to B$ is a map by Functions, Values of a Function, and Functions from One Class to Another §map.

Values. Let $x\in A$ with $P(x)$, so $x\in A_{1}$. By Functions, Values of a Function, and Functions from One Class to Another §value, $(x,f_{1}(x))\in f_{1}\subseteq f$, and since $f(x)$ is the unique set $z$ with $(x,z)\in f$ (Functions, Values of a Function, and Functions from One Class to Another §value), $f(x)=f_{1}(x)=t_{1}(x)$. Likewise, for $x\in A$ without $P(x)$ we have $x\in A_{2}$ and $(x,f_{2}(x))\in f_{2}\subseteq f$, so $f(x)=f_{2}(x)=t_{2}(x)$. This proves existence.

Uniqueness. Let $g:A\to B$ be any map with $g(x)=t_{1}(x)$ for $x\in A$ with $P(x)$ and $g(x)=t_{2}(x)$ for $x\in A$ without $P(x)$. Then $f$ and $g$ are functions with $\operatorname{dom}f=A=\operatorname{dom}g$ (Functions, Values of a Function, and Functions from One Class to Another §map), and for every $x\in A$ either $P(x)$ holds and $g(x)=t_{1}(x)=f(x)$, or it fails and $g(x)=t_{2}(x)=f(x)$. Hence $g=f$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. $\blacksquare$