Proof of Images of Unions, Intersections, Differences and Subclasses under a Function, and under an Injective Function

Throughout, membership in a class term is read off by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction: for a set $v$, $v\in R[C]$ means $\exists u\,(u\in C\wedge(u,v)\in R)$ by The Image and the Preimage of a Class under a Class §image, and $u\in C\cup D$, $u\in C\cap D$, $u\in C\setminus D$ mean $u\in C\vee u\in D$, $u\in C\wedge u\in D$, $u\in C\wedge u\notin D$ by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations. Every element of a class is a set by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique §elements, so all quantifiers below range over sets. Each equality of classes is proved by Axiom of Extensionality for Classes, adopted in Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, by showing that each side is a subclass of the other, which by Subclasses and Subsets §subclass means that every element of the one is an element of the other.

Preliminary. Let $H:P\to Q$ be a map and $C\subseteq P$. We show: for every set $v$, $v\in H[C]$ if and only if $v=H(u)$ for some $u\in C$; and in that case $v\in Q$. By Functions, Values of a Function, and Functions from One Class to Another §map, $H$ is a function with domain $\operatorname{dom}H=P$ and range $\operatorname{ran}H\subseteq Q$. If $v\in H[C]$, there is $u\in C$ with $(u,v)\in H$; then $u\in P=\operatorname{dom}H$ since $C\subseteq P$, so the value $H(u)$ is the unique set $z$ with $(u,z)\in H$, whence $v=H(u)$. Conversely, if $u\in C$, then $u\in\operatorname{dom}H$, and $H(u)$ is a set with $(u,H(u))\in H$ by Functions, Values of a Function, and Functions from One Class to Another §value, so $H(u)\in H[C]$. Finally $(u,H(u))\in H$ gives $H(u)\in\operatorname{ran}H$ by Relations, Domain, Range, Inverse and Composition §range, hence $H(u)\in Q$. We call this fact (P). Note also that $A\cup B$, $A\cap B$ and $A\setminus B$ are subclasses of $X$, since each of their elements lies in $A$ or in $B$, both subclasses of $X$; so (P) applies to them with $H=F$.

Union. Let $v\in F[A\cup B]$. By (P), $v=F(u)$ for some $u\in A\cup B$; if $u\in A$ then $v\in F[A]$ by (P), and if $u\in B$ then $v\in F[B]$; either way $v\in F[A]\cup F[B]$. Conversely let $v\in F[A]\cup F[B]$, say $v\in F[A]$ (the case $v\in F[B]$ is symmetric). By (P), $v=F(u)$ with $u\in A$, so $u\in A\cup B$ and $v\in F[A\cup B]$ by (P). By extensionality $F[A\cup B]=F[A]\cup F[B]$.

Monotone. Let $A\subseteq B$ and $v\in F[A]$. By (P), $v=F(u)$ with $u\in A$, so $u\in B$ and $v\in F[B]$ by (P); thus $F[A]\subseteq F[B]$.

Composition. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, the composite $G\circ F:X\to Z$ of Relations, Domain, Range, Inverse and Composition §composition is a map with $(G\circ F)(u)=G(F(u))$ for every $u\in X$. First, $F[A]\subseteq Y$: every element of $F[A]$ is a value $F(u)$ with $u\in A$, and that value lies in $Y$, both by (P) for $F$; so (P) applies to $G$ and the subclass $F[A]$ of $Y$. Let $w\in(G\circ F)[A]$. By (P) for $G\circ F$, $w=(G\circ F)(u)=G(F(u))$ for some $u\in A$. By (P) for $F$, $F(u)\in F[A]$, and (P) for $G$ and $F[A]$ gives $w=G(F(u))\in G[F[A]]$. Conversely let $w\in G[F[A]]$. By (P) for $G$, $w=G(v)$ for some $v\in F[A]$, and by (P) for $F$, $v=F(u)$ for some $u\in A$. Then $w=G(F(u))=(G\circ F)(u)$, so $w\in(G\circ F)[A]$ by (P) for $G\circ F$. By extensionality $(G\circ F)[A]=G[F[A]]$.

From now on $F$ is injective.

Membership. Let $x\in X$. If $x\in A$, then $F(x)\in F[A]$ by (P). Conversely, if $F(x)\in F[A]$, then by (P) $F(x)=F(u)$ for some $u\in A$; as $u\in X$ and $F$ is injective, Injective, Surjective and Bijective Functions between Classes §injective gives $x=u$, so $x\in A$.

Intersection. Let $v\in F[A\cap B]$. By (P), $v=F(u)$ with $u\in A\cap B$, so $u\in A$ and $u\in B$, and (P) gives $v\in F[A]$ and $v\in F[B]$, i.e. $v\in F[A]\cap F[B]$. Conversely let $v\in F[A]\cap F[B]$. By (P), $v=F(u)$ with $u\in A$, so $u\in X$; since $F(u)=v\in F[B]$, the membership clause, applied to $B$, gives $u\in B$. Hence $u\in A\cap B$ and $v\in F[A\cap B]$ by (P). By extensionality $F[A\cap B]=F[A]\cap F[B]$.

Difference. Let $v\in F[A\setminus B]$. By (P), $v=F(u)$ with $u\in A$ and $u\notin B$, so $u\in X$ and $v\in F[A]$ by (P); and $v\notin F[B]$, since otherwise the membership clause, applied to $B$, would give $u\in B$. Thus $v\in F[A]\setminus F[B]$. Conversely let $v\in F[A]\setminus F[B]$. By (P), $v=F(u)$ with $u\in A$; if $u\in B$, then $v\in F[B]$ by (P), which is excluded, so $u\notin B$. Hence $u\in A\setminus B$ and $v\in F[A\setminus B]$ by (P). By extensionality $F[A\setminus B]=F[A]\setminus F[B]$.

Inclusion. If $A\subseteq B$, then $F[A]\subseteq F[B]$ by the monotone clause. Conversely let $F[A]\subseteq F[B]$ and $x\in A$. Then $x\in X$ and $F(x)\in F[A]$ by (P), so $F(x)\in F[B]$, and the membership clause gives $x\in B$; thus $A\subseteq B$. If $A=B$, then $F[A]=F[B]$ by substitution of equals. Conversely, if $F[A]=F[B]$, then $F[A]\subseteq F[B]$ and $F[B]\subseteq F[A]$, so $A\subseteq B$ and $B\subseteq A$ by what was just shown, and $A=B$ by extensionality.