Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $A$, $B$ and $C$ be classes. For a map $F$, $F(u)$ is its value at $u$ and $\operatorname{dom}F$ its domain. $(u,v)$ is the ordered pair, restrictions $H|_{S}$ are as in The Restriction of a Function or Relation to a Class (i), $A\times B$ is the Cartesian product, $\{c\}$ the singleton, $F^{-1}[D]$ the preimage of a class $D$, and $\cap$ the intersection.

(i) Values. Let $F:A\to B$ be a map. For every $u\in A$: $u\in\operatorname{dom}F$, $F(u)$ is a set, $F(u)\in B$ and $(u,F(u))\in F$ (for sets $A$ and $B$, the last two assertions are Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii)).

(ii) Pairs as values. Let $F:A\to B$ be a map. For every $u\in A$ and every set $v$: $(u,v)\in F$ if and only if $v=F(u)$. For all sets $u$ and $v$: $(u,v)\in F$ if and only if $u\in A$ and $v=F(u)$.

(iii) Extensionality. If $F:A\to B$ and $G:A\to C$ are maps with $G(u)=F(u)$ for every $u\in A$, then $G=F$ (this restates Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i) for maps, and Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv) for classes and two codomains).

(iv) Restriction of a restriction. For all classes $H$, $S$ and $T$ with $T\subseteq S$: $(H|_{S})|_{T}=H|_{T}$.

(v) Restriction to the domain. Let $F:A\to B$ be a map. Then $F|_{A}=F$ (for sets $A$ and $B$, this is Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iii)).

(vi) Restriction to a subclass. Let $F:A\to B$ be a map. For every class $S\subseteq A$, $F|_{S}:S\to B$ is a map. For every class $S$ and every $u\in S$ with $u\in A$: $(F|_{S})(u)=F(u)$ (this restates Domains and Restrictions of Maps (ii) and, for an arbitrary class $S$, Domains and Restrictions of Maps (iii)).

(vii) Constant maps. For every set $c$, $A\times\{c\}$ is a map $A\to\{c\}$, with $(A\times\{c\})(u)=c$ for every $u\in A$; hence, if $c\in B$, then $A\times\{c\}:A\to B$ is a map.

(viii) Pairs in a product. For all sets $u$ and $v$: $(u,v)\in A\times B$ if and only if $u\in A$ and $v\in B$ (this is Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i)).

(ix) Preimages. Let $F:A\to B$ be a map. For all classes $D$ and $u$: $u\in F^{-1}[D]$ if and only if $u\in A$ and $F(u)\in D$ (this is Membership in Inverse Relations, Preimages and Images of Classes, and Enlarging the Codomain of a Map (iii), stated for every class $u$).

(x) Preimages of intersections. Let $F:A\to B$ be a map. For all classes $D$ and $E$: $F^{-1}[D]\cap F^{-1}[E]=F^{-1}[D\cap E]$.