Proof of Kit for def:holomorphic-function

Facts about maps and predicative formulas carried by Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (vi) are used without comment. Throughout, formulas are written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), a formula being predicative when it is so with its abbreviations eliminated, and the given $x_{0},\dots,x_{n-1}$ are the first of distinct set variables $x_{0},x_{1},\dots$ as in Renaming and Substituting Variables in Predicative Formulas, so that $x_{0},x_{1},x_{2}$ are distinct also when $n<3$. The parameters are those of the statement, at their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i); they are variables other than $x_{0},x_{1},\dots$ and other than the bound variables below, and $\mathbb{C}$, $d_{\mathbb{C}}$, $\mathbb{R}$ and its element $0$ are sets ($d_{\mathbb{C}}$, a map $\mathbb{C}\times\mathbb{C}\to\mathbb{R}$, lies in $\mathbb{R}^{\mathbb{C}\times\mathbb{C}}$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii) and The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)). In formulas, $\oplus$ and $\odot$ denote the sum and product operations of $\mathbb{C}$, which are binary operations on $\mathbb{C}$ (The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (iii)), and for set variables $r$ and $r'$, $r\le r'$ and $r<r'$ stand for $(r,r')\in{\le}$ and $(r,r')\in{<}$. Formulas of the forms $(\cdot,\cdot)\in\cdot$ and $((\cdot,\cdot),\cdot)\in\cdot$ are those of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii) and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv): they are predicative and, when sets are assigned to the variables inside the pairs, hold exactly when the corresponding membership of ordered pairs does. The letters $\varepsilon,\delta,a,b,c,h,m,q,s,t,v,y$ denote further set variables, distinct from one another, from $x_{0},x_{1},\dots$ and from the parameters.

Openness and maps. Write $U$, $f$ and $W$ for $x_{0}$, $x_{1}$ and $x_{2}$. By Kit for def:open-subset-metric-space (i), with its number of variables equal to $3$ and its $i$, $j$, $k$ equal to $0$, $1$, $2$, there is a predicative formula $\omega$ in $x_{0},x_{1},x_{2}$, with parameters among $\mathbb{R}$, $+$, $0$ and $\le$, that holds exactly when $(x_{0},x_{1})$ is a metric space, $x_{2}\subseteq x_{0}$ and $x_{2}$ is open in $(x_{0},x_{1})$. By Renaming and Substituting Variables in Predicative Formulas (iii), with $\tau_{0}=\mathbb{C}$, $\tau_{1}=d_{\mathbb{C}}$ and $\tau_{2}=x_{0}$, respectively $\tau_{2}=x_{2}$, it yields predicative formulas $\omega_{U}$ and $\omega_{W}$ in $x_{0},x_{1},x_{2}$; as $(\mathbb{C},d_{\mathbb{C}})$ is a metric space (Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces (v)), $\omega_{U}$ holds exactly when $U\subseteq\mathbb{C}$ and $U$ is open in $(\mathbb{C},d_{\mathbb{C}})$, and $\omega_{W}$ exactly when $W\subseteq\mathbb{C}$ and $W$ is open in $(\mathbb{C},d_{\mathbb{C}})$. Let $\mu_{f}$ be the formula $\mu(F,A,B)$ of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii) with $x_{1}$, $x_{0}$ and $\mathbb{C}$ as its $F$, $A$ and $B$, its auxiliary set variables chosen pairwise distinct and distinct from the letters above and from the parameters; it is predicative and holds exactly when $f$ is a map $f:U\to\mathbb{C}$.

The formulas. Let

$$\beta(v,t,\delta)=t\in U\wedge\exists m\,\bigl(((t,v),m)\in d_{\mathbb{C}}\wedge0<m\wedge m<\delta\bigr),$$ $$\lambda(v,y,t,\varepsilon)=\exists a\,\exists b\,\exists c\,\exists h\,\exists q\,\exists s\,\bigl((t,a)\in f\wedge(v,b)\in f\wedge((c,b),a)\in{\oplus}\wedge((h,v),t)\in{\oplus}\wedge((q,h),c)\in{\odot}\wedge((q,y),s)\in d_{\mathbb{C}}\wedge s<\varepsilon\bigr),$$ $$\kappa(v,y)=\forall\varepsilon\,\Bigl((\varepsilon\in\mathbb{R}\wedge0<\varepsilon)\Rightarrow\exists\delta\,\bigl(\delta\in\mathbb{R}\wedge0<\delta\wedge\forall t\,(\beta(v,t,\delta)\Rightarrow\lambda(v,y,t,\varepsilon))\bigr)\Bigr),$$ $$\varphi=\omega_{U}\wedge\mu_{f}\wedge\forall v\,(v\in W\Rightarrow v\in U)\wedge\omega_{W}\wedge\forall v\,\bigl(v\in W\Rightarrow\exists y\,(y\in\mathbb{C}\wedge\kappa(v,y))\bigr).$$

The formulas $\omega_{U}$, $\omega_{W}$, $\mu_{f}$ and the pair and operation memberships are predicative, so they contain no quantifier over a class variable, and every other quantifier above is over a set variable; so $\varphi$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). The free variables of $\kappa(v,y)$ are among $x_{0}$, $x_{1}$, $v$, $y$ and the parameters, so those of $\varphi$ are among $x_{0}$, $x_{1}$, $x_{2}$ and the parameters.

What $\kappa$ says. Let sets $U$, $f$, $z$ and $L$ be assigned to $x_{0}$, $x_{1}$, $v$ and $y$, where $U$ is an open subset of $(\mathbb{C},d_{\mathbb{C}})$, $f$ is a map $f:U\to\mathbb{C}$, $z\in U$ and $L\in\mathbb{C}$. Let $\delta,\varepsilon\in\mathbb{R}$ and let $t$ be a set.

First, $\beta(v,t,\delta)$ holds if and only if $t\in U$ and $0<|t-z|<\delta$: for $t\in U$, the pair $(t,z)$ lies in $\mathbb{C}\times\mathbb{C}$, the domain of $d_{\mathbb{C}}$, so $((t,z),m)\in d_{\mathbb{C}}$ holds exactly for $m=d_{\mathbb{C}}(t,z)$ (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x)), and $d_{\mathbb{C}}(t,z)=|t-z|$ by The Distance on the Complex Numbers (i).

Second, let $t\in U$ with $0<|t-z|$; then $t-z\neq0$, as $|0|=0$. As $f$ is a map $U\to\mathbb{C}$, $(t,a)\in f$ holds exactly for $a=f(t)$ and $(z,b)\in f$ exactly for $b=f(z)$, and these are complex numbers. By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi), applied to $\oplus$ and $\odot$, the formula $((c,b),a)\in{\oplus}$ then holds exactly when $c\in\mathbb{C}$ and $c+f(z)=f(t)$, that is, for $c=f(t)-f(z)$; $((h,z),t)\in{\oplus}$ exactly for $h=t-z$; and $((q,h),c)\in{\odot}$ exactly when $q\in\mathbb{C}$ and $q(t-z)=c$, that is, as $t-z\neq0$ and $\mathbb{C}$ is a field (The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (v)), for $q=c/(t-z)$ (Negatives, Differences, Reciprocals and Quotients (ii)). For such $q$, $((q,L),s)\in d_{\mathbb{C}}$ holds exactly for $s=d_{\mathbb{C}}(q,L)=|q-L|$, as in the first step. So $\lambda(v,y,t,\varepsilon)$ holds if and only if

$$\Bigl|\frac{f(t)-f(z)}{t-z}-L\Bigr|<\varepsilon .$$

Hence $\kappa(v,y)$ holds if and only if for every real $\varepsilon>0$ there is a real $\delta>0$ such that every $t\in U$ with $0<|t-z|<\delta$ satisfies this inequality, that is, by The Complex Derivative at a Point (i), if and only if $L$ is a complex derivative of $f$ at $z$. Consequently $\exists y\,(y\in\mathbb{C}\wedge\kappa(v,y))$ holds, with $z$ assigned to $v$, if and only if $f$ has a complex derivative at $z$, that is, is complex differentiable at $z$.

What $\varphi$ says. Let sets $U$, $f$ and $W$ be assigned to $x_{0}$, $x_{1}$ and $x_{2}$. By the paragraph on openness and maps and by Subclasses and Subsets (i), the first four conjuncts of $\varphi$ hold exactly when $U\subseteq\mathbb{C}$ and $U$ is open in $(\mathbb{C},d_{\mathbb{C}})$, $f$ is a map $f:U\to\mathbb{C}$, $W\subseteq U$, and $W\subseteq\mathbb{C}$ is open in $(\mathbb{C},d_{\mathbb{C}})$; if one of them fails, $\varphi$ fails, and so does the condition of (i). If they hold, then every $z\in W$ lies in $U$, so by the previous paragraph, with $z$ assigned to $v$, the last conjunct says that $f$ is complex differentiable at every point of $W$, that is, by Holomorphic Functions and Their Derivatives (i), that $f$ is holomorphic on $W$. So $\varphi$ is a predicative formula in $x_{0},x_{1},x_{2}$, in the sense of Renaming and Substituting Variables in Predicative Formulas, expressing the condition of (i) with $U=x_{0}$, $f=x_{1}$ and $W=x_{2}$.

Renaming to arbitrary positions. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $3$ and $\sigma(0)=i$, $\sigma(1)=j$ and $\sigma(2)=k$, the formula $\varphi(x_{i},x_{j},x_{k})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds, under every assignment of sets to $x_{0},\dots,x_{n-1}$, exactly when the condition of (i) holds for $U=x_{i}$, $f=x_{j}$ and $W=x_{k}$. This proves (i).

The class of holomorphic functions. Let $U$ be an open subset of $(\mathbb{C},d_{\mathbb{C}})$ and let $W\subseteq U$ be open in $(\mathbb{C},d_{\mathbb{C}})$; $U$ and $W$ are sets, being subclasses of the set $\mathbb{C}$ (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 (i)). Apply The Class Comprehension Theorem for Predicative Formulas (i) to $\varphi$ with its abbreviations eliminated, with $x_{1}$ as its single variable and $x_{0}$ and $x_{2}$ (assigned $U$ and $W$) and the parameters of the statement as its parameters. It gives a class $H$ whose elements are exactly the sets $f$ for which $\varphi$ holds with $f$ assigned to $x_{1}$ (the one-entry tuple $\langle f\rangle$ is $f$ by The Ordered Pair of Two Sets and Nested Tuples (ii)), that is, as the hypotheses on $U$ and $W$ hold, the sets $f$ that are maps $f:U\to\mathbb{C}$ holomorphic on $W$. Every element of $H$ is a set (Classes, Membership, Sets and Proper Classes (i)), and so is every map $f:U\to\mathbb{C}$, as an element of the class $\mathbb{C}^{U}$ of functions from $U$ to $\mathbb{C}$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)), $U$ and $\mathbb{C}$ being sets. So for every class $f$, $f\in H$ if and only if $f$ is a map $f:U\to\mathbb{C}$ holomorphic on $W$. This proves (ii).