Proof of Projection, Evaluation and Currying Maps

Each result cited is universally quantified over the data in its own statement.

Clause projections. Apply Maps and Relations Given by Formulas §binary with $X$ for its $b$ and $c$, $Y$ for its $d$, and the expression $e(v,w)=v$, a single variable, which contains no defined set symbol: $e(v,w)=v\in X$ for all $v\in X$ and $w\in Y$. It gives exactly one map $\pi_{1}:X\times Y\to X$ with $\pi_{1}((v,w))=v$ for all $v\in X$ and $w\in Y$, which is the first assertion, as $\pi_{1}(x,y)$ stands for $\pi_{1}((x,y))$ by Sets and Maps: Ordinary Notation §maps. Applied with $Y$ for its $b$ and $d$, $X$ for its $c$ and $e(v,w)=w$, it gives exactly one map $\pi_{2}:X\times Y\to Y$ with $\pi_{2}(x,y)=y$.

Let $p\in X\times Y$. By The Cartesian Product of Two Classes §product and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, there are sets $x\in X$ and $y\in Y$ with $p=(x,y)$. By The Components of an Ordered Pair §components, $p_{1}$ is the unique set $z$ with $\exists y'\,(p=(z,y'))$; $x$ is such a set, so $p_{1}=x=\pi_{1}(p)$. Likewise $p_{2}=y=\pi_{2}(p)$.

Clause evaluation. By The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §set, $Y^{I}$ is a set. Apply Maps and Relations Given by Formulas §binary with $Y$ for its $b$, $Y^{I}$ for its $c$, $I$ for its $d$, and the expression $e(f,i)=f(i)$, the value of $f$ at $i$. This value is a defined set symbol with arguments $f$ and $i$, the unique set $z$ satisfying $(i,z)\in f$, by Functions, Values of a Function, and Functions from One Class to Another §value; this formula is predicative by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §pair-membership. The hypotheses of the lemma hold: for $f\in Y^{I}$ and $i\in I$, $f$ is a map $f:I\to Y$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §members, so $f$ is a function with $\operatorname{dom}f=I$ by Functions, Values of a Function, and Functions from One Class to Another §map; hence $i\in\operatorname{dom}f$, exactly one set $z$ satisfies $(i,z)\in f$, and the symbol is used properly; and $f(i)\in Y$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §graph. So there is exactly one map $\mathrm{ev}:Y^{I}\times I\to Y$ with $\mathrm{ev}((f,i))=f(i)$, that is, $\mathrm{ev}(f,i)=f(i)$, for all $f\in Y^{I}$ and $i\in I$.

Clause currying. Let $g:X\times I\to Y$ be a map. For $x\in X$ and $i\in I$, $(x,i)\in X\times I$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, so $g(x,i)=g((x,i))$ is defined and lies in $Y$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §graph.

The maps $c(x)$. Apply Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §map-symbol with $I$ and $Y$ for its $A$ and $B$, $k=1$, $x$ for its $v_{1}$, the predicative formula $x\in X$ for its $\gamma$, and the expression $g((x,u))$ for its $t(u,v_{1})$. This expression is built from the variables $g$, $x$ and $u$ and the defined set symbols ordered pair and value, with no class abstraction written in it, and for every $x\in X$ and every $u\in I$ it is used properly and lies in $Y$, as just shown; $I$, $Y$, $X$ and $g$ are parameters. So there is a predicative formula $\theta(h,x)$ such that, for every $x\in X$, the only set $h$ satisfying $\theta(h,x)$ is the map $u\mapsto g(x,u)$ from $I$ to $Y$ of Sets and Maps: Ordinary Notation §maps; write $c(x)$ for it. By Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-set-symbols, $c(x)$ is a defined set symbol with argument $x$, given by $\theta$ and used properly where $x\in X$. For $x\in X$, $c(x)$ is a map $I\to Y$ with $c(x)(i)=g(x,i)$ for $i\in I$, so $c(x)\in Y^{I}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §members.

Existence. Apply Maps and Relations Given by Formulas §map with $X$ for its $a$, $Y^{I}$ for its $b$ and the expression $c(x)$, which is used properly and lies in $Y^{I}$ for every $x\in X$. It gives a map $h:X\to Y^{I}$ with $h(x)=c(x)$ for every $x\in X$; hence $h(x)(i)=c(x)(i)=g(x,i)$ for all $x\in X$ and $i\in I$.

Uniqueness. Let $h':X\to Y^{I}$ be a map with $h'(x)(i)=g(x,i)$ for all $x\in X$ and $i\in I$. Let $x\in X$. By Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §graph, $h(x)$ and $h'(x)$ lie in $Y^{I}$, so they are maps $I\to Y$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §members, and $h'(x)(i)=g(x,i)=h(x)(i)$ for every $i\in I$; so $h'(x)=h(x)$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §equality, with the sets $I$ and $Y$. As $x\in X$ was arbitrary, $h'=h$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §equality, with the sets $X$ and $Y^{I}$.