$ \def \N {{ \mathbb N }} \def \Z {{ \mathbb Z }} \def \Q {{ \mathbb Q }} \def \R {{ \mathbb R }} \def \C {{ \mathbb C }} \def \H {{ \mathbb H }} \def \S {{ \mathbb S }} \def \P {{ \mathbb P }} \def \to { \longrightarrow } \def \mapsto { \longmapsto } \def \then { ~ \Longrightarrow ~ } \def \iff { ~ \Longleftrightarrow ~ } \def \and { ~ \wedge ~ } \def \or { ~ \vee ~ } \def \d {{~\rm d}} % We prepend a space to the differential symbol `d`, for good measure! \def \IFF {{\hskip4pt \sc iff \hskip2pt}} \def \Int {{ \bf Int }} \def \Clo {{ \bf Clo }} \def \Lim {{ \bf Lim }} \def \Dom {{ \bf Dom }} \def \Cod {{ \bf Cod }} \def \Ker {{ \bf Ker }} \def \Img {{ \bf Img }} \def \coKer {{ \bf coKer }} \def \coImg {{ \bf coImg }} \def \rem {{ \hskip4pt \rm rem \hskip4pt }} \def \tab {{ \hskip16pt }} $
arrow_back arrow_downward

The fundamental theorem of equivalence relations

Functions are some of the most important objects in math. So they’re studied all over the place.
In calculus, you study differentiable functions.
In topology, you study functions that preserve topological structure (continuous functions).
In group theory, you study functions that preserve group structure (group morphisms).
In ring theory, you study functions that preserve ring structure (ring morphisms).
In complex analysis, you study functions that preserve complex structure (holomorphic functions).
In the theory of topological manifolds, you study continuous functions between topological manifolds.
In the theory of differentiable manifolds, you study differential functions between differentiable manifolds.
In the theory of smooth manifolds, you study smooth functions between smooth manifolds.
And so on.

For sets, the functions that preserve set structure are simply... functions. (Sets don’t have a lot of structure.) The core idea of functions is very simple:

\(\tab\tab\) associate one object to every object.

But there’s a ton of important stuff that can be deduced from this idea without building too much technical machinery. For example, every function \(f: A \to B\) between sets gives rise to a function \(f^*: { \mathcal P } B \to { \mathcal P } A\) between their power sets, going in the opposite direction. The function \(f^*: { \mathcal P } B \to { \mathcal P } A\) can be called the preimage function of \(f\), or the contravariant subset function of \(f\), and it has very nice properties. For starters, \(f^*: { \mathcal P } B \to { \mathcal P } A\) preserves unions, intersections, complements, and inclusions. The power set of a set is always a Boolean algebra (under unions, intersections, complements, and inclusions), and the preimage function \(f^*: { \mathcal P } B \to { \mathcal P } A\) preserves its Boolean algebra structure: \(f^*: { \mathcal P } B \to { \mathcal P } A\) is a Boolean algebra morphism, or a morphism of Boolean algebras. There’s a dual function function \(f^*: { \mathcal P } B \to { \mathcal P } A\), which we denote \(f_*: { \mathcal P } A \to { \mathcal P } B\) and which we can call the image function of \(f\), or the covariant subset function of \(f\). The function \(f_*: { \mathcal P } A \to { \mathcal P } B\) goes in the same direction as \(f: A \to B\) (that is, if \(f\) goes from \(A\) to \(B\), then \(f_*\) goes from \({ \mathcal P } A\) to \({ \mathcal P } B\)). The function \(f_*: { \mathcal P } A \to { \mathcal P } B\) doesn’t behave as nicely as is dual function \(f^*: { \mathcal P } B \to { \mathcal P } A\), but it still warrants attention.

The image function and the preimage function. A first look

Let \(f: \{0, 1, 2\} \to \{5, 6\}\) be a map from the set \(\{0, 1, 2\}\) to the set \(\{5, 6\}\), and let \(f: \{0, 1, 2\} \to \{5, 6\}\) be defined by
\(\tab\tab\) \(f:0 \mapsto 5\)
\(\tab\tab\) \(f:1 \mapsto 6\)
\(\tab\tab\) \(f:2 \mapsto 5\).

First, take the element \(1 \in \{0, 1, 2\}\) of \(\{0, 1, 2\}\).
Consider the (unique!) image of \(1\) under \(f\).
The image of \(1 \in \{0, 1, 2\}\) under \(f\) is denoted \(f[1]\), or \(f(1)\), and it’s the sole element of \(\{5, 6\}\) that \(1\) is \(f\)-associated to.
By the definition of \(f\), the image \(f[1]\) of \(1\) under \(f\) is the element \(6 \in \{5, 6\}\).
Notice that \(1\) is an element of \(\{0, 1, 2\}\), and \(f[1]\) is an element of \(\{5, 6\}\).

Second, take the subset \(\{0, 2\} \subseteq \{0, 1, 2\}\) of \(\{0, 1, 2\}\).
Consider the (unique!) image of each element of \(\{0, 2\}\) under \(f\).
The image of \(0 \in \{0, 2\}\) under \(f\) is denoted \(f[0]\), or \(f(0)\), and it’s the sole element of \(\{5, 6\}\) that \(0\) is \(f\)-associated to.
The image of \(2 \in \{0, 2\}\) under \(f\) is denoted \(f[2]\), or \(f(2)\), and it’s the sole element of \(\{5, 6\}\) that \(2\) is \(f\)-associated to.
By the definition of \(f\), the image \(f[0]\) of \(0\) under \(f\) is the element \(5 \in \{5, 6\}\).
By the definition of \(f\), the image \(f[2]\) of \(2\) under \(f\) is the element \(5 \in \{5, 6\}\).
Now, the image of \(\{0, 2\}\) under \(f\) is defined as the set \(\{f[0], f[2]\}\), which can also be written as the set \(\{5, 5\}\) (using the definition of \(f\)), which is also the set \(\{5\}\) (sets don’t allow repetitions).
The image of \(\{0, 2\}\) under \(f\) is denoted \(f_*[\{0, 2\}]\), or simply \(f(\{0, 2\})\), and it’s the sole subset of \(\{5, 6\}\) that \(\{0, 2\}\) if \(f\)-associated to.
Notice that \(\{0, 2\}\) is a subset of \(\{0, 1, 2\}\), and \(f_*[\{0, 2\}]\) is a subset of \(\{5, 6\}\).

Third, take the subset \(\{5\} \subseteq \{5, 6\}\) of \(\{5, 6\}\).
Consider the elements of \(\{0, 1, 2\}\) that have some element of \(\{5, 6\}\) as their image under \(f\).
The preimage of \(\{5\}\) under \(f\) is defined as the set of all such elements, and it’s denoted \(f^*[\{5\}]\), or \(f^{-1}[\{5\}]\) (not to be confused with the inverse function of \(f\), which doesn’t always exist!).

In general, the image of a subset \(A' \subseteq A\) under \(f\) is denoted \(f_*[A']\), or simply \(f(A')\), and in symbols you can write it down as
\(\tab\tab\) \(f_*[A'] \hskip8pt := \hskip8pt \{f[a] \in B \hskip6pt | \hskip6pt a \in A'\}\),
and you can read this as “the set of all \(f[a]\) in \(B\) as \(a\) ranges over \(A'\).

In general, the preimage of a subset \(B' \subseteq B\) under \(f\) is denoted \(f^*[B']\), or also \(f^{-1}(B')\), and in symbols you can write it down as
\(\tab\tab\) \(f^*[B'] \hskip8pt := \hskip8pt \{a \in A \hskip6pt | \hskip6pt f[a] \in B'\}\),
and you can read this as “the set of all \(a\) in \(A\) whose image \(f[a]\) is in \(B'\).

Notice that
\(\tab\tab1)\) if \(f: A \to B\) is a function from \(A\) to \(B\) and \(a \in A\) is an element of \(A\), then \(f[a]\) is an element of \(B\)
\(\tab\tab2)\) if \(f: A \to B\) is a function from \(A\) to \(B\) and \(A' \subseteq A\) is a subset of \(A\), then \(f_*[A']\) is a subset of \(B\)
\(\tab\tab3)\) if \(f: A \to B\) is a function from \(A\) to \(B\) and \(B' \subseteq B\) is a subset of \(B\), then \(f^*[B']\) is a subset of \(A\).

Every function \(f: A \to B\) from a set \(A\) to a set \(B\) gives rise to a pair \((f_*: { \mathcal P } A \to { \mathcal P } B, f^*: { \mathcal P } B \to { \mathcal P } A)\) of functions:
\(\tab\tab1)\) a function \(f_*: { \mathcal P } A \to { \mathcal P } B\) from the power set \({ \mathcal P } A\) of \(A\) to the power set \({ \mathcal P } B\) of \(B\)
\(\tab\tab2)\) a function \(f^*: { \mathcal P } B \to { \mathcal P } A\) from the power set \({ \mathcal P } B\) of \(B\) to the power set \({ \mathcal P } A\) of \(A\).

In other words, the function \(f_*: { \mathcal P } A \to { \mathcal P } B\) maps subsets of \(A\) to subsets of \(B\), and the function \(f^*: { \mathcal P } B \to { \mathcal P } A\) maps subsets of \(B\) to subsets of \(A\). The functions \(f_*: { \mathcal P } A \to { \mathcal P } B\) and \(f^*: { \mathcal P } B \to { \mathcal P } A\) are closely related to the function \(f: A \to B\), and they depend on \(f: A \to B\), which is why they have the symbol \(f\) in their name.

In this page, we intend to prove that, for any subsets \(A',A1,A2 \subseteq A\) and for any \(B',B1,B2 \subseteq B\), the following hold:
\(\tab\tab1)\) \(A' \subseteq f^*[f_*[A']]\)
\(\tab\tab2)\) \(f_*[f^*[B']] \subseteq B'\)
\(\tab\tab3)\) \(f^*: B1 \cup B2 \hskip6pt\mapsto\hskip6pt f^*[B1] \cup f^*[B1]\)
\(\tab\tab4)\) \(f^*: B1 \cap B2 \hskip6pt\mapsto\hskip6pt f^*[B1] \cap f^*[B2]\)
\(\tab\tab5)\) \(f^*: B \setminus B1 \hskip6pt\mapsto\hskip6pt A \setminus f^*[B1]\)
\(\tab\tab6)\) \(B1 \subseteq B2 \hskip6pt\then\hskip6pt f^*[B1] \subseteq f^*[B2]\)
\(\tab\tab7)\) \(f^*: \{\} \hskip6pt\mapsto\hskip6pt \{\}\)
\(\tab\tab8)\) \(f^*: B \hskip6pt\mapsto\hskip6pt A\)

In particular, this means that the preimage function \(f^*: { \mathcal P } B \to { \mathcal P } A\) is a morphism of the Boolean algebras \({ \mathcal P } B\) and \({ \mathcal P } A\). (More on this later!)

The image function and the preimage function. Example

\(\tab\) Example. Let \(A\) be the set \(\{0, 1, 2\}\), let \(B\) be the set \(\{5, 6\}\), let \(f: A \to B\) be the function given by
\(\tab\tab\) \(f:0 \mapsto 5\)
\(\tab\tab\) \(f:1 \mapsto 6\)
\(\tab\tab\) \(f:2 \mapsto 5\).
Equivalently, the data for the function \(f: A \to B\) could be given using the graph of \(f: A \to B\), which is a subset of the Cartesian product \(A \times B\). We can denote the graph of the function \(f: A \to B\) using the letter \(f\), and then specify the graph \(f\) of the function \(f: A \to B\) as
\(\tab\tab\) \(f \hskip8pt := \hskip8pt \{(0, 5), (1, 6), (2, 5)\}\).
Notice \(f: A \to B\) is indeed a function: it maps each element of \(A\) to exactly one element of \(B\).
Now, what do the functions \(f_*: { \mathcal P } A \to { \mathcal P } B\) and \(f^*: { \mathcal P } A \to { \mathcal P } B\) look like? First, let’s construct the powersets \({ \mathcal P } A\) and \({ \mathcal P } B\).
Since \(A\) is the set \(\{0, 1, 2\}\), then \({ \mathcal P } A\) is the set \(\{\{\}, \{0\}, \{1\}, \{2\}, \{0, 1\}, \{0, 2\}, \{1, 2\}, \{0, 1, 2\}\}\).
Since \(B\) is the set \(\{5, 6\}\), then \({ \mathcal P } B\) is the set \(\{\{\}, \{5\}, \{6\}, \{5, 6\}\}\).
Now, from the data for the function \(f: A \to B\), we can derive the data for the image function \(f_*: { \mathcal P } A \to { \mathcal P } B\). More explicitly, from the data for the function
\(\tab\tab\) \(f: \{0, 1, 2\} \to \{5, 6\}\),
we can derive the data for the image function
\(\tab\tab\) \(f_*: \{\{\}, \{0\}, \{1\}, \{2\}, \{0, 1\}, \{0, 2\}, \{1, 2\}, \{0, 1, 2\}\} \to \{\{\}, \{5\}, \{6\}, \{5, 6\}\}\).
This yields
\(\tab\tab\) \(f_*:\{\} \mapsto \{\}\)
\(\tab\tab\) \(f_*:\{0\} \mapsto \{5\}\)
\(\tab\tab\) \(f_*:\{1\} \mapsto \{6\}\)
\(\tab\tab\) \(f_*:\{2\} \mapsto \{5\}\)
\(\tab\tab\) \(f_*:\{0, 1\} \mapsto \{5, 6\}\)
\(\tab\tab\) \(f_*:\{0, 2\} \mapsto \{5\}\)
\(\tab\tab\) \(f_*:\{1, 2\} \mapsto \{5, 6\}\)
\(\tab\tab\) \(f_*:\{0, 1, 2\} \mapsto \{5, 6\}\).
And, from the data for the function \(f: A \to B\), we can derive the data for the preimage function \(f^*: { \mathcal P } B \to { \mathcal P } A\). More explicitly, from the data for the function
\(\tab\tab\) \(f: \{0, 1, 2\} \to \{5, 6\}\),
we can derive the data for the preimage function
\(\tab\tab\) \(f^*: \{\{\}, \{5\}, \{6\}, \{5, 6\}\} \to \{\{\}, \{0\}, \{1\}, \{2\}, \{0, 1\}, \{0, 2\}, \{1, 2\}, \{0, 1, 2\}\}\).
This yields
\(\tab\tab\) \(f^*:\{\} \mapsto \{\}\)
\(\tab\tab\) \(f^*:\{5\} \mapsto \{0, 2\}\)
\(\tab\tab\) \(f^*:\{6\} \mapsto \{1\}\)
\(\tab\tab\) \(f^*:\{5, 6\} \mapsto \{0, 1, 2\}\).
And we’re done.
\(\tab\) \(\square\)

Having seen an example, we can look at the definitions.

The image function of a function. Definition

Every function from a set \(A\) to a set \(B\) gives rise to a function from the power set of \(A\) to the power set of \(B\).
That is, every function \(f: A \to B\) gives rise to a function \(f_*: { \mathcal P } A \to { \mathcal P } B\).
That is, if \(f: A \to B\) maps elements of \(A\) to elements of \(B\), then \(f_*: { \mathcal P } A \to { \mathcal P } B\) maps subsets of \(A\) to subsets of \(B\).
The function \(f_*: { \mathcal P } A \to { \mathcal P } B\) is not too special, and it doesn’t have too many properties. We call \(f_*\) the image function of \(f\), or the covariant subset function of \(f\).

\(\tab\) Definition. Let \(f: A \to B\) be a function between sets, let \(A' \subseteq A\) be a subset of \(A\).
The image of \(A'\) under \(f\), denoted \(f_*[A']\), is the set of all elements of the form \(f[a]\) as \(a\) ranges over \(A'\).
Equivalently, \(f_*[A']\) is the set of all elements of \(B\) that are the image of at least one element of \(A'\).
In symbols, the image \(f_*[A']\) of \(A'\) under \(f\) can be defined in any of the following equivalent ways:
\(\tab\tab1)\) \(f_*[A'] \hskip8pt := \hskip8pt \{f[a] \in B \hskip6pt | \hskip6pt a \in A'\}\)
\(\tab\tab2)\) \(f_*[A'] \hskip8pt := \hskip8pt \{b \in B \hskip6pt | \hskip6pt \exists a \in A' \hskip4pt \langle f[a] = b \rangle\}\)

Even though these two definitions yield the same set, they have different “flavors”. You can think about them in terms of how an “algorithm” would “compute” the image \(f_*[A']\) of \(A'\) under \(f\) using each definition.

An algorithm to compute the image \(f_*[A']\) of \(A'\) under \(f\) using definition \(1)\) would do the following. Loop through each element \(a\) of \(A'\), apply \(f\) to each element \(a\) of \(A'\), and gather all the results inside a set; this set is your desired image \(f[A']\).

An algorithm to compute the image \(f_*[A']\) of \(A'\) under \(f\) using definition \(2)\) would do the following. Loop through each element \(b\) of \(B\) and, for each element \(b\) of \(B\), it would loop through all elements \(a\) of \(A'\) and apply \(f\) to \(a\) until the image \(f[a]\) of \(a\) lands in \(b\) (in which case it stores this \(b\) somewhere safe) or until it has traversed through all of \(A'\) and \(f[a]\) never lands in \(b\) (in which case it discards this \(b\)). The set of all \(b\)’s that the algorithm didn’t discard in the desired image \(f[A']\).

Using the definition of the image \(f_*[A']\)

Notice that \(f: A \to B\) and \(f_*: { \mathcal P } A \to { \mathcal P } B\) can’t be the same function because they don’t have the same domain or the same codomain. In the literature people drop the notational distinction between \(f: A \to B\) and \(f_*: { \mathcal P } A \to { \mathcal P } B\), calling them both \(f\).

The preimage function of a function. Definition

Every function from a set \(A\) to a set \(B\) gives rise to a function from the power set of \(B\) to the power set of \(A\).
That is, every function \(f: A \to B\) gives rise to a function \(f^*: { \mathcal P } B \to { \mathcal P } A\).
That is, if \(f: A \to B\) maps elements of \(A\) to elements of \(B\), then \(f^*: { \mathcal P } B \to { \mathcal P } A\) maps subsets of \(B\) to subsets of \(A\).
The function \(f^*: { \mathcal P } B \to { \mathcal P } A\) is very special, and it has very nice properties. We call \(f^*\) the contravariant subset function of \(f\), or the preimage function of \(f\).

\(\tab\) Definition. Let \(f: A \to B\) be a function between sets, let \(B' \subseteq B\) be a subset of \(B\).
The preimage of \(B'\) under \(f\), denoted \(f^*[B']\), is the set of all \(a\) in \(A\) whose image \(f[a]\) is in \(B'\).
Equivalently, \(f_*[B']\) is the set of all elements of \(A\) whose image is at least one element of \(B'\).
In symbols, the preimage \(f^*[B']\) of \(B'\) under \(f\) can be defined in any of the following equivalent ways:
\(\tab\tab1)\) \(f^*[B'] \hskip8pt := \hskip8pt \{a \in A \hskip6pt | \hskip6pt f[a] \in B'\}\)
\(\tab\tab2)\) \(f^*[B'] \hskip8pt := \hskip8pt \{a \in A \hskip6pt | \hskip6pt \exists b \in B' \hskip4pt \langle f[a] = b \rangle\}\)

Even though these two definitions yield the same set, they have different “flavors”.

The domain is a subset of the preimage of the image

\(\tab\) Theorem. Let \(f: A \to B\) be a function from set \(A\) to set \(B\), let \(A' \subseteq A\) be a subset of \(A\). Now
\(\tab\tab1)\) \(A'\) is a subset of the preimage of the image of \(A'\)
\(\tab\tab2)\) \(A'\) is a subset of the preimage (under \(f\)) of the image (under \(f\)) of \(A'\)
\(\tab\tab3)\) \(A'\) is a subset of \(f^* \circ f_*[A']\)
\(\tab\tab4)\) \(A' \subseteq f^* \circ f_*[A']\)
\(\tab\tab5)\) \(A' \subseteq f^*[f_*[A']]\)
\(\tab\tab6)\) for every \(a\) in \(A'\), \(a\) is in \(f^*[f_*[A']]\)
\(\tab\tab7)\) \(\forall a \in A' \hskip4pt \langle\hskip4pt a \in f^*[f_*[A']] \hskip4pt\rangle\)
\(\tab\tab8)\) for every \(a\), if \(a\) is in \(A'\), then \(a\) is in \(f^*[f_*[A']]\)
\(\tab\tab9)\) \(\forall a \hskip4pt \langle\hskip4pt a \in A' \then a \in f^*[f_*[A']] \hskip4pt\rangle\)

\(\tab\) Proof. TODO

The image of the preimage is a subset of the codomain

\(\tab\) Theorem. Let \(f: A \to B\) be a function from set \(A\) to set \(B\), let \(B' \subseteq B\) be a subset of \(B\). Now
\(\tab\tab1)\) the image of the preimage of \(B'\) is a subset of \(B'\)
\(\tab\tab2)\) the image (under \(f\)) of the preimage (under \(f\)) of \(B'\) is a subset of \(B'\)
\(\tab\tab3)\) \(f_* \circ f^*[B']\) is a subset of \(B'\)
\(\tab\tab4)\) \(f_* \circ f^*[B'] \subseteq B'\)
\(\tab\tab5)\) \(f_*[f^*[B']] \subseteq B'\)
\(\tab\tab6)\) for every \(b\) in \(f_*[f^*[B']]\), \(b\) is in \(B'\)
\(\tab\tab7)\) \(\forall b \in f_*[f^*[B']] \hskip4pt \langle\hskip4pt b \in B' \hskip4pt\rangle\)
\(\tab\tab8)\) for every \(b\), if \(b\) is in \(f_*[f^*[B']]\), then \(b\) is in \(B'\)
\(\tab\tab9)\) \(\forall b \hskip4pt \langle\hskip4pt b \in f_*[f^*[B']] \then b \in B' \hskip4pt\rangle\)

\(\tab\) Proof. Statements \(1)\) through \(9)\) are all the same statement written in different (but equivalent) ways. We want to prove that

\[f_*[f^*[B']] \subseteq B'.\]

To do this, take an arbitrary element \(b \in f_*[f^*[B']]\). We don’t know much about the element \(b\), except that it belongs to \(f_*[f^*[B']]\).
From the definition of \(f_*: { \mathcal P } A \to { \mathcal P } B\), we can immediately deduce that there exists an element \(a \in f^*[B']\) that goes to \(b\) (under \(f\)), meaning \(f: a \mapsto b\).
That is, the very definition of \(f_*: { \mathcal P } A \to { \mathcal P } B\) guarantees the existence of a particular element \(a \in f^*[B']\) whose image \(f[a]\) under \(f\) is \(b\) (remember that \(b \in f_*[f^*[B']]\) is the original element we started with).

This element \(a \in f^*[B']\) will be the key to everything.
One thing to notice about \(a \in f^*[B']\) is that it’s not arbitrary. I mean, the element \(b \in f_*[f^*[B']]\) is arbitrary, but, after we “lock in” our choice of \(b \in f_*[f^*[B']]\), we find that our realm of possibilities for \(a\) is not arbitrary. That is, this element \(a \in f^*[B']\), whose existence is guaranteed by the very definition of \(f_*: { \mathcal P } A \to { \mathcal P } B\), depends the specific \(b \in f_*[f^*[B']]\) that we take.
Another thing to notice about \(a \in f^*[B']\) is that it need not be unique! The hypothesis that \(f\) is a function is perfectly fine with this fact: indeed, there can exist multiple elements of \(f^*[B']\) whose image (under \(f\)) is \(b\). The important thing is that we’re guaranteed the existence of at least one.

So, to recap.
Assume \(b\) is in \(f_*[f^*[B']]\).
It follows that there exists at least one element \(a\) of \(f^*[B']\) whose image \(f[a]\) is \(b\), meaning \(f: a \mapsto b\).

Now let’s look at the definition of \(f^*[B']\). What does it mean to be an element of \(f^*[B']\)? What does it mean that \(a\) is an element of \(f^*[B']\)? What membership criteria must \(a\) fulfill in order to be an element of \(f^*[B']\)? Given the knowledge that \(a\) is in \(f^*[B']\), what can we deduce about \(a\)? What can we deduce about \(f[a]\)?
One crucial thing the membership of \(a\) to \(f^*[B']\) allows us to deduce is the existence of some element of \(B'\) that \(a\) goes to (under \(f\)). This element is important, so let’s give it a name: call it \(b'\). So, \(b'\) is an element of \(B'\).
Let’s state this again. Given the fact that \(a\) is in \(f^*[B']\), we’re guaranteed the existence of an element \(b'\) in \(B'\) that \(a\) goes to (under \(f\)), meaning \(f: a \mapsto b'\).

Now we stop, and look back.
We started with the hypothesis that \(b\) is in \(f_*[f^*[B']]\).
Then, we deduced the existence of an element \(a \in A\) with the property that \(f: a \mapsto b\).
And now we’ve deduced the existence of an element \(b' \in B'\) with the property that \(f: a \mapsto b'\).
So we simultaneously have that \(f: a \mapsto b\) and that \(f: a \mapsto b'\).
What does this mean? Can we deduce anything from this? The really important question is: are \(b\) and \(b'\) distinct elements, or are they secretly the same element written in two different (but equivalent) ways?

The hypothesis that \(f: A \to B\) is a function contradicts the possibility that \(b\) and \(b'\) are distinct. We can’t have that \(f: A \to B\) is a function and also that \(b\) and \(b'\) are distinct. If we assume that \(b\) and \(b'\) are distinct, then \(f: A \to B\) is not a function. But, if we do insist that \(f: A \to B\) is a function (and we do; this is one of our hypotheses), then we must necessarily arrive at the conclusion that \(b\) is equal to \(b'\), meaning \(b = b'\). And recall that \(b'\) is in \(B'\). Since \(b'\) was actually \(b\) all along, it follows that \(b\) is in \(B'\).

So, we started with the hypothesis that \(b\) is in \(f_*[f^*[B']]\), and we’ve arrived at the conclusion that \(b\) is in \(B'\). This argument proves that, if \(b\) is in \(f_*[f^*[B']]\), then \(b\) is in \(B'\), which, by definition, means that \(f_*[f^*[B']]\) is a subset of \(B'\), meaning \(f_*[f^*[B']] \subseteq B'\), which is our goal.

But there’s one subtlety left. What if \(f_*[f^*[B']]\) is the empty set \(\{\}\)? That is, what if \(f_*[f^*[B']]\) has no elements? Then we couldn’t possibly have that \(b\) is in \(f_*[f^*[B']]\) to start with. In this case, the statement that \(b\) is in \(f_*[f^*[B']]\) is a false statement, and so the implication “if \(b\) is in \(f_*[f^*[B']]\), then \(b\) is in \(B'\)” is (vacuously) true, by the definition of implication.
\(\tab\) \(\square\)

A proof of \(f_*[f^*[B']] \subseteq B'\) that outlines the steps, but doesn’t explain any of the reasoning, goes as follows.

\(\tab\) Proof. Let \(b \in f_*[f^*[B']]\). Then there exists \(a \in f^*[B']\) such that \(f[a] = b\). Since \(a \in f^*[B']\), then \(f[a] \in B'\). It follows that \(b \in B'\).
\(\tab\) \(\square\)

The preimage function is a morphism of Boolean algebras

\(\tab\) Theorem. Let \(f: A \to B\) be a map from set \(A\) to set \(B\).
Now the preimage function \(f^*: { \mathcal P } B \to { \mathcal P } A\) induced by map \(f\) is a morphism of Boolean algebras.
In symbols, the preimage function \(f^*: { \mathcal P } B \to { \mathcal P } A\) satisfies the following, for all subsets \(B1,B2 \subseteq B\):
\(\tab\tab1)\) \(f^*: B1 \cup B2 \hskip6pt\mapsto\hskip6pt f^*[B1] \cup f^*[B1]\)
\(\tab\tab2)\) \(f^*: B1 \cap B2 \hskip6pt\mapsto\hskip6pt f^*[B1] \cap f^*[B2]\)
\(\tab\tab3)\) \(f^*: B \setminus B1 \hskip6pt\mapsto\hskip6pt A \setminus f^*[B1]\)
\(\tab\tab4)\) \(B1 \subseteq B2 \hskip6pt\then\hskip6pt f^*[B1] \subseteq f^*[B2]\)
\(\tab\tab5)\) \(f^*: \{\} \hskip6pt\mapsto\hskip6pt \{\}\)
\(\tab\tab6)\) \(f^*: B \hskip6pt\mapsto\hskip6pt A\)

\(\tab\) Proof. To prove that \(f^*: { \mathcal P } B \to { \mathcal P } A\) is a morphism of Boolean algebras, we must prove that, in passing from the Boolean algebra \({ \mathcal P } B\) to the Boolean algebra \({ \mathcal P } A\), the map \(f^*\) preserves the Boolean algebra structure. The Boolean algebra structure has four components: unions, intersections, complements, inclusions, the least element, and the greatest element. So, we must prove that
\(\tab\tab1)\) \(f^*: { \mathcal P } B \to { \mathcal P } A\) preserves unions
\(\tab\tab2)\) \(f^*: { \mathcal P } B \to { \mathcal P } A\) preserves intersections
\(\tab\tab3)\) \(f^*: { \mathcal P } B \to { \mathcal P } A\) preserves complements
\(\tab\tab4)\) \(f^*: { \mathcal P } B \to { \mathcal P } A\) preserves inclusions
\(\tab\tab5)\) \(f^*: { \mathcal P } B \to { \mathcal P } A\) preserves the least element
\(\tab\tab6)\) \(f^*: { \mathcal P } B \to { \mathcal P } A\) preserves the greatest element.

To prove \(1)\), let \(B1\) and \(B2\) be subsets of \(B\).

To prove \(2)\), let \(B1\) and \(B2\) be subsets of \(B\).

To prove \(5)\), recall that the Boolean-least element of \({ \mathcal P } B\) is the empty set \(\{\}\) and the Boolean-least element of \({ \mathcal P } A\) is the empty set \(\{\}\). Now, what is the image of \(\{\}\) under \(f^*\)? That is, what is the preimage \(f^*[\{\}]\) of the empty set under the map \(f\)? Well, recall the definition of preimage. If \(B1\) is a subset of \(B\), then \(f^*[B1]\) is defined as the set of all elements of \(A\) that are mapped to an element of \(B1\). This means

\[f^*[B1] \hskip8pt := \hskip8pt \{a \in A \hskip6pt | \hskip6pt f[a] \in B1\}.\]

Now, the empty set \(\{\}\) is a subset of \(B\), so \(f^*[\{\}]\) is defined as the set of all elements of \(A\) that are mapped to an element of the empty set \(\{\}\). This means

\[f^*[\{\}] \hskip8pt := \hskip8pt \{a \in A \hskip6pt | \hskip6pt f[a] \in \{\}\}.\]

But there’s something very wrong with the expression: \(f[a] \in \{\}\). Namely, \(f[a]\) can’t be an element of \(\{\}\) because \(\{\}\) has no elements. So, there can’t be any element of \(A\) that gets mapped (by \(f\)) an element of \(\{\}\). This means that the set of all such elements is also empty. This shows that the preimage (under \(f\)) of the empty set is also empty, meaning that the image (under \(f^*\)) of the empty set is the empty set, meaning that \(f^*[\{\}]\) is \(\{\}\). And this is the desired result: the preimage function \(f^*\) maps to Boolean-least element of \({ \mathcal P } B\) to the Boolean-least element of \({ \mathcal P } A\).

To prove \(6)\), let \(B1\) and \(B2\) be subsets of \(B\).