avewright/proofwiki-math huggingface dataset:
Theorem: Preimage of Intersection under Mapping

Let $f: S \to T$ be a mapping.
Let $T_1$ and $T_2$ be subsets of $T$.
Then:
:$f^{-1} \sqbrk {T_1 \cap T_2} = f^{-1} \sqbrk {T_1} \cap f^{-1} \sqbrk {T_2}$
This can be expressed in the language and notation of inverse image mappings as:
:$\forall T_1, T_2 \in \powerset T: \map {f^\gets} {T_1 \cap T_2} = \map {f^\gets} {T_1} \cap \map {f^\gets} {T_2}$

Proof:
As $f$ is a mapping, it is by definition also a many-to-one relation.
It follows from Inverse of Many-to-One Relation is One-to-Many that its inverse $f^{-1}$ is a one-to-many relation.
Thus Image of Intersection under One-to-Many Relation: Family of Sets can be applied for $\RR = f^{-1}$:
:$\ds \RR \sqbrk {\bigcap_{i \mathop \in I} T_i} = \bigcap_{i \mathop \in I} \RR \sqbrk {T_i}$
where $\RR \sqbrk {T_i}$ denotes the image of $T_i$ under $\RR$.
{{Qed}}
Theorem: Preimage of Intersection under Mapping

Let $f: S \to T$ be a mapping.
Let $T_1$ and $T_2$ be subsets of $T$.
Then:
:$f^{-1} \sqbrk {T_1 \cap T_2} = f^{-1} \sqbrk {T_1} \cap f^{-1} \sqbrk {T_2}$
This can be expressed in the language and notation of inverse image mappings as:
:$\forall T_1, T_2 \in \powerset T: \map {f^\gets} {T_1 \cap T_2} = \map {f^\gets} {T_1} \cap \map {f^\gets} {T_2}$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = f^{-1} \sqbrk {\bigcap_{i \mathop \in I} T_i}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \map f x
      | o = \in
      | r = \bigcap_{i \mathop \in I} T_i
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall i \in I
      | l = \map f x
      | o = \in
      | r = T_i
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall i \in I
      | l = x
      | o = \in
      | r = f^{-1} \sqbrk {T_i}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcap_{i \mathop \in I} f^{-1} \sqbrk {T_i}
      | c = 
}}
{{end-eqn}}
{{Qed}}
Theorem: Preimage of Set Difference under Mapping

Let $f: S \to T$ be a mapping.
Let $T_1$ and $T_2$ be subsets of $T$.
Then:
:$f^{-1} \sqbrk {T_1 \setminus T_2} = f^{-1} \sqbrk {T_1} \setminus f^{-1} \sqbrk {T_2}$
where:
:$\setminus$ denotes set difference
:$f^{-1} \sqbrk {T_1}$ denotes preimage.

Proof:
From Inverse of Mapping is One-to-Many Relation, we have that $f^{-1}: T \to S$ is one-to-many.
Thus we can apply One-to-Many Image of Set Difference:
:$\RR \sqbrk {T_1 \setminus T_2} = \RR \sqbrk {T_1} \setminus \RR \sqbrk {T_2}$
where in this context $\RR = f^{-1}$.
{{qed}}
Theorem: Projection is Surjection

Let $S$ and $T$ be non-empty sets.
Let $S \times T$ be the Cartesian product of $S$ and $T$.
Let $\pr_1: S \times T \to S$ and $\pr_2: S \times T \to T$ be the first projection and second projection respectively on $S \times T$.
Then $\pr_1$ and $\pr_2$ are both surjections.

Proof:
Let $S$ and $T$ be sets such that neither is empty.
Let $\pr_1: S \times T \to S$ be the first projection on $S \times T$.
Then by definition of first projection:
:$\forall x \in S: \exists \tuple {x, t} \in S \times T: \map {\pr_1} {x, t} = x$
Similarly, let $\pr_2: S \times T \to T$ be the second projection on $S \times T$.
Then by definition of second projection:
:$\forall x \in T: \exists \tuple {s, x} \in S \times T: \map {\pr_2} {s, x} = x$
Hence the result.
{{qed}}
Theorem: Sum Rule for Derivatives

Let $\map f x, \map j x, \map k x$ be real functions defined on the open interval $I$.
Let $\xi \in I$ be a point in $I$ at which both $j$ and $k$ are differentiable.
Let $\map f x = \map j x + \map k x$.
Then $f$ is differentiable at $\xi$ and:
:$\map {f'} \xi = \map {j'} \xi + \map {k'} \xi$
It follows from the definition of derivative that if $j$ and $k$ are both differentiable on the interval $I$, then:
:$\forall x \in I: \map {f'} x = \map {j'} x + \map {k'} x$

Proof:
{{begin-eqn}}
{{eqn | l = \map {f'} \xi
      | r = \lim_{h \mathop \to 0} \frac {\map f {\xi + h} - \map f \xi} h
      | c = {{Defof|Derivative}}
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\paren {\map j {\xi + h} + \map k {\xi + h} } - \paren {\map j \xi + \map k \xi } } h
      | c = 
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map j {\xi + h} + \map k {\xi + h} - \map j \xi - \map k \xi} h
      | c = 
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\paren {\map j {\xi + h} - \map j \xi} + \paren {\map k {\xi + h} - \map k \xi} } h
      | c = 
}}
{{eqn | r = \lim_{h \mathop \to 0} \paren {\frac {\map j {\xi + h} - \map j \xi} h + \frac {\map k {\xi + h} - \map k \xi} h}
      | c = 
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map j {\xi + h} - \map j \xi} h + \lim_{h \mathop \to 0} \frac {\map k {\xi + h} - \map k \xi} h
      | c = 
}}
{{eqn | r = \map {j'} \xi + \map {k'} \xi
      | c = {{Defof|Derivative}}
}}
{{end-eqn}}
{{qed}}
Theorem: Sum Rule for Derivatives

Let $\map f x, \map j x, \map k x$ be real functions defined on the open interval $I$.
Let $\xi \in I$ be a point in $I$ at which both $j$ and $k$ are differentiable.
Let $\map f x = \map j x + \map k x$.
Then $f$ is differentiable at $\xi$ and:
:$\map {f'} \xi = \map {j'} \xi + \map {k'} \xi$
It follows from the definition of derivative that if $j$ and $k$ are both differentiable on the interval $I$, then:
:$\forall x \in I: \map {f'} x = \map {j'} x + \map {k'} x$

Proof:
It can be observed that this is an example of a Linear Combination of Derivatives with $\lambda = \mu = 1$.
{{qed}}
Theorem: Quotient Mapping is Surjection

Let $S$ be a set.
Let $\RR$ be an equivalence relation on $S$.
Then the quotient mapping $q_\RR: S \to S / \RR$ is a surjection.

Proof:
Suppose $S$ is  empty. 
<!-- The following sentence is annoying, normally we talk about the equclass of an *element* (under some relation).
Intuitively, it's really should be "the set of equclass is empty" and more or less directly go to "$S / \RR$ is empty", but it feel as if a step would be missed. -->
Then, vacuously, $S$ has no equivalence classes
Hence, the set $S / \RR$ of $\RR$-classes of $\RR$ is the empty set.
Therefore, as the codomain of $q_\RR$ is empty, $q_\RR$ is vacuously surjective.
{{qed|lemma}}
Suppose $S$ is non-empty.
From Equivalence Class is not Empty, we have that:
:$\forall \eqclass x \RR \in S / \RR: \exists x \in S: x \in \eqclass x \RR$
and the result follows.
{{qed}}
Theorem: Trivial Quotient is a Bijection

Let $\Delta_S$ be the diagonal relation on a set $S$.
Let $q_{\Delta_S}: S \to S / \Delta_S$ be the trivial quotient of $S$.
Then $q_{\Delta_S}: S \to S / \Delta_S$ is a bijection.

Proof:
The diagonal relation is defined as:
:$\Delta_S = \set {\tuple {x, x}: x \in S} \subseteq S \times S$
From the fact that $q_{\Delta_S}$ is a quotient mapping, we know that it is a surjection.
It relates each $x \in S$ to the singleton $\set x$.
Thus:
:$\set x = \eqclass x {\Delta_S} \subseteq S$
So $\map {q_{\Delta_S} } x = \set x$, and it follows that:
:$\eqclass x {\Delta_S} = \eqclass y {\Delta_S} \implies x = y$
Thus $q_{\Delta_S}$ is injective, and therefore by definition a bijection.
{{Qed}}
Theorem: Composite of Quotient Mappings

Let $S$ be a set.
Let $\RR_1$ be an equivalence on $S$, and $\RR_2$ be an equivalence on the quotient set $S / \RR_1$.
We can find an equivalence $\RR_3$ on $S$ such that $\paren {S / \RR_1} / \RR_2$ is in one-to-one correspondence with $S / \RR_3$ under the mapping:
:$\phi: \paren {S / \RR_1} / \RR_2 \to S / \RR_3: \eqclass {\eqclass x {\RR_1} } {\RR_2} \mapsto \eqclass x {\RR_3}$.

Proof:
Define $\RR_3$ to be the equivalence induced by:
:$x \mapsto \eqclass {\eqclass x {\RR_1} } {\RR_2}$
By definition of $\RR_3$:
:$\eqclass {\eqclass x {\RR_1} } {\RR_2} = \eqclass {\eqclass y {\RR_1} } {\RR_2} \implies \eqclass x {\RR_3} = \eqclass y {\RR_3}$
Therefore, $\phi$ is well-defined.
Again by definition of $\RR_3$: 
:$\eqclass x {\RR_3} = \eqclass y {\RR_3} \implies \eqclass {\eqclass x {\RR_1} } {\RR_2} = \eqclass {\eqclass y {\RR_1} } {\RR_2}$
which means $\phi$ is an injection.
Lastly, note that every element of $S / \RR_3$ is of the form $\eqclass x {\RR_3}$ for some $x \in S$.
It is now immediate from the definition of $\phi$ that it is surjective.
Hence $\phi$ is a bijection, as desired.
{{qed}}
Theorem: Renaming Mapping is Well-Defined

Let $f: S \to T$ be a mapping.
Let $r: S / \RR_f \to \Img f$ be the renaming mapping,  defined as:
:$r: S / \RR_f \to \Img f: \map r {\eqclass x {\RR_f} } = \map f x$
where:
:$\RR_f$ is the equivalence induced by the mapping $f$
:$S / \RR_f$ is the quotient set of $S$ determined by $\RR_f$
:$\eqclass x {\RR_f}$ is the equivalence class of $x$ under $\RR_f$.
The renaming mapping is always well-defined.

Proof:
By Relation Induced by Mapping is Equivalence Relation, we have that $\RR_f$ is an equivalence relation.
To determine whether $r$ is well-defined, we have to determine whether $r: S / \RR_f \to \Img f$ actually defines a mapping at all.
Consider a typical element $\eqclass x {\RR_f}$ of $S / \RR_f$.
Suppose we were to choose another name for the class $\eqclass x {\RR_f}$.
Assume that $\eqclass x {\RR_f}$ is not a singleton.
For example, let us choose $y \in \eqclass x {\RR_f}, y \ne x$ such that: 
:$\eqclass x {\RR_f} = \eqclass y {\RR_f}$
then:
:$\map r {\eqclass x {\RR_f} } = \map r {\eqclass y {\RR_f} }$
Hence from the definition, we have:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = \eqclass x {\RR_f}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map f y
      | r = \map f x
      | c = 
}}
{{eqn | r = \map r {\eqclass x {\RR_f} }
      | c = 
}}
{{eqn | r = \map r {\eqclass y {\RR_f} }
      | c = 
}}
{{end-eqn}}
Thus $r$ is well-defined.
{{qed}}
Theorem: Renaming Mapping is Well-Defined

Let $f: S \to T$ be a mapping.
Let $r: S / \RR_f \to \Img f$ be the renaming mapping,  defined as:
:$r: S / \RR_f \to \Img f: \map r {\eqclass x {\RR_f} } = \map f x$
where:
:$\RR_f$ is the equivalence induced by the mapping $f$
:$S / \RR_f$ is the quotient set of $S$ determined by $\RR_f$
:$\eqclass x {\RR_f}$ is the equivalence class of $x$ under $\RR_f$.
The renaming mapping is always well-defined.

Proof:
From Condition for Mapping from Quotient Set to be Well-Defined:
:there exists a mapping $\phi: S / \RR \to T$ such that $\phi \circ q_\RR = f$
{{iff}}:
:$\forall x, y \in S: \tuple {x, y} \in \RR \implies \map f x = \map f y$
But by definition of the equivalence induced by the mapping $f$:
:$\forall x, y \in S: \tuple {x, y} \in \RR_f \implies \map f x = \map f y$
The result follows directly.
{{qed}}
Theorem: Renaming Mapping is Bijection

Let $f: S \to T$ be a mapping.
Let $r: S / \RR_f \to \Img f$ be the renaming mapping, defined as:
:$r: S / \RR_f \to \Img f: \map r {\eqclass x {\RR_f} } = \map f x$
where:
:$\RR_f$ is the equivalence induced by the mapping $f$
:$S / \RR_f$ is the quotient set of $S$ determined by $\RR_f$
:$\eqclass x {\RR_f}$ is the equivalence class of $x$ under $\RR_f$.
The renaming mapping is a bijection.

Proof:
=== Proof of Injectivity ===
To show that $r: S / \RR_f \to \Img f$ is an injection:
{{begin-eqn}}
{{eqn | l = \map r {\eqclass x {\RR_f} }
      | r = \map r {\eqclass y {\RR_f} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map f x
      | r = \map f y
      | c = {{Defof|Renaming Mapping}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \RR_f
      | r = y
      | c = {{Defof|Equivalence Relation Induced by Mapping}}
}}
{{eqn | ll= \leadsto
      | l = \eqclass x {\RR_f}
      | r = \eqclass y {\RR_f}
      | c = {{Defof|Equivalence Class}}
}}
{{end-eqn}}
Thus $r: S / \RR_f \to \Img f$ is an injection.
{{qed|lemma}}
=== Proof of Surjectivity ===
To show that $r: S / \RR_f \to \Img f$ is a surjection:
Note that for all mappings $f: S \to T$, $f: S \to \Img f$ is always a surjection from Surjection by Restriction of Codomain.
Thus by definition:
:$\forall y \in \Img f: \exists x \in S: \map f x = y$
So:
{{begin-eqn}}
{{eqn | q = \forall x \in S: \exists \eqclass x {\RR_f}
      | l = x
      | o = \in
      | r = \eqclass x {\RR_f}
      | c = Equivalence Class is not Empty
}}
{{eqn | ll= \leadsto
      | q = \forall y \in \Img f: \exists \eqclass x {\RR_f} \in S / \RR_f
      | l = \map f x
      | r = y
      | c = {{Defof|Equivalence Relation Induced by Mapping}}
}}
{{eqn | ll= \leadsto
      | q = \forall y \in \Img f: \exists \eqclass x {\RR_f} \in S / \RR_f
      | l = \map r {\eqclass x {\RR_f} }
      | r = y
      | c = {{Defof|Renaming Mapping}}
}}
{{end-eqn}}
Thus $r: S / \RR_f \to \Img f$ is a surjection.
{{qed|lemma}}
As $r: S / \RR_f \to \Img f$ is both an injection and a surjection, it is by definition a bijection.
{{qed}}
Theorem: Renaming Mapping is Bijection

Let $f: S \to T$ be a mapping.
Let $r: S / \RR_f \to \Img f$ be the renaming mapping, defined as:
:$r: S / \RR_f \to \Img f: \map r {\eqclass x {\RR_f} } = \map f x$
where:
:$\RR_f$ is the equivalence induced by the mapping $f$
:$S / \RR_f$ is the quotient set of $S$ determined by $\RR_f$
:$\eqclass x {\RR_f}$ is the equivalence class of $x$ under $\RR_f$.
The renaming mapping is a bijection.

Proof:
From Renaming Mapping is Well-Defined, $r: S / \RR_f \to \Img f$ is a well-defined mapping.
By definition, $\RR_f$ is the equivalence relation induced by the mapping $f$.
Hence by definition:
:$\tuple {s_1, s_2} \in \RR_f \iff \map f {s_1} = \map f {s_2}$
From Condition for Mapping from Quotient Set to be Injection, this is precisely the condition required for $r$ to be an injection.
Next it is noted that the codomain of $r$ is $\Img f$.
Then from Restriction of Mapping to Image is Surjection, we have that $f_{\restriction \Img f}$ is a surjection.
Hence from Condition for Mapping from Quotient Set to be Surjection it follows that $r$ is also a surjection.
Thus $r$ is shown to be both an injection and a surjection, and so by definition is a bijection.
{{qed}}
Theorem: Composite of Mapping with Inverse

Let $f: S \to T$ be a mapping.
Then:
:$\forall x \in S: \map {f^{-1} \circ f} x = \eqclass x {\RR_f}$
where:
:$\RR_f$ is the equivalence induced by $f$
:$\eqclass x {\RR_f}$ is the $\RR_f$-equivalence class of $x$.

Proof:
Let $y = \map f x$.
Then by the definition of induced equivalence:
:$x \in \eqclass x {\RR_f}$
By the definition of the inverse of a mapping:
:$f^{-1} = \set {\tuple {y, x}: \tuple {x, y} \in f}$
Thus:
:$\eqclass x {\RR_f} = \set {s \in \Dom f: \map f s = \map f x}$
By definition:
:$\map {f^{-1} } y = \eqclass x {\RR_f}$
Hence the result.
{{qed}}
Theorem: Factoring Mapping into Surjection and Inclusion

Every mapping $f:S \to T$ can be uniquely '''factored into''' a surjection $g$ followed by the inclusion mapping $i_T$.
That is, $f = i_T \circ g$ where:
:$g: S \to \Img f: \map g x = \map f x$
:$i_T: \Img f \to T: \map {i_T} x = x$
This can be illustrated using a commutative diagram as follows:
$\quad\quad \begin{xy}\xymatrix@L+2mu@+1em {
S \ar@{-->}[r]^*{g}
\ar[rd]_*{f = i_T \circ g}
&
\Img f \ar@{-->}[d]^*{i_T}
\\
&
T
}\end{xy}$

Proof:
From Surjection by Restriction of Codomain, $f: S \to \Img f$ is a surjection.
The mapping $g: S \to \Img f$ where $\map g x = \map f x$ is therefore also clearly a surjection.
The mapping $g: S \to \Img f: \map g x = \map f x$ is clearly unique, by Equality of Mappings.
From Inclusion Mapping is Injection, $i_T: \Img f \to T$ is an injection.
Likewise, the mapping $i_T: \Img f \to T : \map {i_T} x = x$ is also unique, by its own definition.
{{qed}}
Theorem: Quotient Theorem for Surjections

Let $f: S \to T$ be a surjection.
Then there is one and only one bijection $r: S / \RR_f \to T$ such that:
:$r \circ q_{\RR_f} = f$
where:
:$\RR_f$ is the equivalence induced by $f$
:$r: S / \RR_f \to T$ is the renaming mapping
:$q_{\RR_f}: S \to S / \RR_f$ is the quotient mapping induced by $\RR_f$.
This can be illustrated using a commutative diagram as follows:
$\quad\quad \begin {xy} \xymatrix@L + 2mu@ + 1em {
S \ar@{-->}[rr]^*{f = r \circ q_{\RR_f} }
\ar[dd]_*{q_{\RR_f} }
&& T \\
\\
S / \RR_f \ar[urur]_*{r} 
} \end {xy}$

Proof:
From the definition of Induced Equivalence, the mapping $f: S \to T$ induces an equivalence $\RR_f$ on its domain.
As $f: S \to T$ is a surjection, $T = \Img f$ by definition.
From Renaming Mapping is Bijection, the renaming mapping $r: S / \RR_f \to T$ is a bijection, where $S / \RR_f$ is the quotient set of $S$ by $\RR_f$.
Hence:
:$r \circ q_{\RR_f} = f$
:$r$ is the only mapping $r: S / \RR_f \to T$ that satisfies this equality.
{{qed}}
Theorem: Quotient Theorem for Sets

A mapping $f: S \to T$ can be uniquely '''factored into''' a surjection, followed by a bijection, followed by an injection.
Thus:
:$f = i \circ r \circ q_{\RR_f}$
where:
{{begin-eqn}}
{{eqn | ll= q_{\RR_f}:
      | lo= S \to S / \RR_f:
      | l = \map {q_{\RR_f} } s
      | r = \eqclass s {\RR_f}
      | c = Quotient Mapping
}}
{{eqn | ll= r:
      | lo= S / \RR_f \to \Img f:
      | l = \map r {\eqclass s {\RR_f} }
      | r = \map f s
      | c = Renaming Mapping
}}
{{eqn | ll= i:
      | lo= \Img f \to T:
      | l = \map i t
      | r = t
      | c = Inclusion Mapping
}}
{{end-eqn}}
where:
:$\RR_f$ is the equivalence induced by $f$
:$S / \RR_f$ is the quotient set of $S$ induced by $\RR_f$
This can be illustrated using a commutative diagram as follows:
$\quad\quad \begin {xy} \xymatrix@L + 2mu@ + 1em {
S \ar@{-->}[rrr]^*{f = i_T \circ r \circ q_{\RR_f} }
\ar[d]_*{q_{\RR_f} }
& & & T \\
S / \RR_f \ar[rrr]_*{r} & & & \Img f \ar[u]_*{i_T} } \end {xy}$

Proof:
From Factoring Mapping into Surjection and Inclusion, $f$ can be factored uniquely into:
:A surjection $g: S \to \Img f$, followed by:
:The inclusion mapping $i: \Img f \to T$ (an injection).
$\quad\quad \begin{xy}\xymatrix@L+2mu@+1em {
S \ar[drdr]_*{g}
\ar@{-->}[rr]^*{f = i_T \circ g}
& & T
\\ \\
& & \Img f \ar[uu]_*{i_T}
}\end{xy}$
From the Quotient Theorem for Surjections, the surjection $g$ can be factored uniquely into:
:The quotient mapping $q_{\RR_f}: S \to S / \RR_f$ (a surjection), followed by:
:The renaming mapping $r: S / \RR_f \to \Img f$ (a bijection).
Thus:
:$f = i_T \circ \paren {r \circ q_{\RR_f} }$
As Composition of Mappings is Associative it can be seen that $f = i_T \circ r \circ q_{\RR_f}$.
The commutative diagram is as follows:
$\quad\quad \begin {xy} \xymatrix@L + 2mu@ + 1em {
S \ar@{-->}[rrr]^*{f = i_T \circ r \circ q_{\RR_f} }
\ar[ddd]_*{q_{\RR_f} }
\ar@{..>}[drdrdr]_*{g = r \circ q_{\RR_f} }
& & & T \\ \\ \\
S / \RR_f \ar[rrr]_*{r} & & & \Img f \ar[uuu]_*{i_T} } \end {xy}$
{{qed}}
Theorem: Empty Set is Element of Power Set

The empty set is an element of all power sets:
:$\forall S: \O \in \powerset S$

Proof:
{{begin-eqn}}
{{eqn | q = \forall S
      | l = \O
      | o = \subseteq
      | r = S
      | c = Empty Set is Subset of All Sets
}}
{{eqn | ll= \leadsto
      | q = \forall S
      | l = \O
      | o = \in
      | r = \powerset S
      | c = {{Defof|Power Set}}
}}
{{end-eqn}}
{{qed}}
Theorem: Direct Image Mapping of Relation is Mapping

Let $S$ and $T$ be sets.
Let $\RR \subseteq S \times T$ be a relation on $S \times T$.
Let $\RR^\to: \powerset S \to \powerset T$ be the direct image mapping of $\RR$:
:$\forall X \in \powerset S: \map {\RR^\to} X = \set {t \in T: \exists s \in X: \tuple {s, t} \in \RR}$
Then $\RR^\to$ is indeed a mapping.

Proof:
Take the general relation $\RR \subseteq S \times T$.
Let $X \subseteq S$, that is $X \in \powerset S$.
Suppose $X = \O$.
Then from Image of Empty Set is Empty Set:
:$\map {\RR^\to} X = \O \subseteq T$
Suppose $X = S$.
Then from Image is Subset of Codomain: Corollary 1:
:$\map {\RR^\to} X = \Img \RR \subseteq T$
Finally, suppose $\O \subset X \subset S$.
From Image is Subset of Codomain, again:
:$\map {\RR^\to} X \subseteq T$
Now, from the definition of the power set, we have that:
:$Y \subseteq T \iff Y \in \powerset T$
We defined $\RR^\to \subseteq \powerset S \times \powerset T$ such that:
:$\RR^\to: \powerset S \to \powerset T: \map {\RR^\to} X = \set {t \in T: \exists s \in X: \tuple {s, t} \in \RR}$
By definition, there is only one $\map {\RR^\to} X$ for any given $X$, and so $\RR^\to$ is many-to-one.
We have shown that:
:$\forall X \subseteq S: \map {\RR^\to} X \in \powerset T$
So:
:$\forall X \in \powerset S: \exists_1 Y \in \powerset T: \map {\RR^\to} X = Y$
So:
:$\RR^\to$ is defined for all $X \in \powerset S$
and therefore $\RR^\to$ is a mapping.
{{qed}}
Theorem: Inverse Image Mapping of Relation is Mapping

Let $S$ and $T$ be sets.
Let $\RR \subseteq S \times T$ be a relation on $S \times T$.
Let $\RR^\gets$ be the inverse image mapping of $\RR$:
:$\RR^\gets: \powerset T \to \powerset S: \map {\RR^\gets} Y = \RR^{-1} \sqbrk Y$
Then $\RR^\gets$ is indeed a mapping.

Proof:
$\RR^{-1}$, being a relation, obeys the same laws as $\RR$.
So Direct Image Mapping of Relation is Mapping applies directly.
{{qed}}
Theorem: Direct Image Mapping of Surjection is Surjection

Let $f: S \to T$ be a surjection.
Then the direct image mapping of $f$:
:$f^\to: \powerset S \to \powerset T$
is a surjection.

Proof:
Let $f: S \to T$ be a surjection.
Then:
:$\forall y \in T: \exists x \in S: f \paren x = y$
From the Quotient Theorem for Surjections, there is one and only one bijection $r: S / \RR_f \to T$ such that $r \circ q_{\RR_f} = f$.
Each element of $S / \RR_f$ is a subset of $S$ and therefore an element of $\powerset S$.
Thus as $r: S / \RR_f \to T$ is a bijection, and hence a fortiori also an injection:
:$\forall X_1, X_2 \in \powerset S: \map r {X_1} = \map r {X_2} \implies X_1 = X_2$
Because $f$ is a surjection, every $y \in T$ is mapped to by exactly one element of the partition of $S$ defined by $\RR_f$.
Let $T = \set {y_1, y_2, \ldots}$.
Let the partition defined by $\RR_f$ be $\bigcup \paren {X_1, X_2, \ldots}$ where $\map r {X_n} = y_n$.
Let $Y_r \in \powerset T$, such that $Y_r = \set {y_{r_1}, y_{r_2}, \ldots}$.
Then:
:$\map {f^\to} {X_r} = Y_r$
where $\ds X_r = \bigcup \paren {X_{r_1}, X_{r_2}, \ldots}$.
As $\set {X_1, X_2, \ldots}$ is a partition of $S$, $\forall Y_r \in \powerset T: X_r$ is unique.
Thus $f^\to: \powerset S \to \powerset T$ is a surjection.
{{Qed}}
Theorem: Direct Image Mapping of Surjection is Surjection

Let $f: S \to T$ be a surjection.
Then the direct image mapping of $f$:
:$f^\to: \powerset S \to \powerset T$
is a surjection.

Proof:
Let $f: S \to T$ be a surjection.
By definition, $f^\to$ is defined by sending subsets of $S$ to their image under $f$.
That is:
:$\forall X \subseteq S: \map {f^\to} X = \set{\map f x: x \in X} \subseteq T$
To prove that $f^\to$ is a surjection, we need to show that every subset of $T$ is the image under $f^\to$ of some subset of $S$.
Let $Y \subseteq T$.
Since $f$ is a surjection, by definition we have that:
:$\forall t \in T: \exists s \in S: \map f s = t$
Hence (possibly requiring the {{Axiom-link|Choice}}), we can select for each $y \in Y$ some $s_y \in S$ such that $\map f {s_y} = y$.
Define $X_Y$ to be:
:$X_Y := \set {s_y: y \in Y}$
Then:
{{begin-eqn}}
{{eqn | l = \map {f^\to} {X_Y}
      | r = \set {\map f {s_y}: s_y \in X_Y}
      | c = 
}}
{{eqn | r = \set {\map f {s_y}: y \in Y}
      | c = 
}}
{{eqn | r = \set {y : y \in Y}
      | c = 
}}
{{eqn | r = Y
      | c = 
}}
{{end-eqn}}
Thus $f^\to: \powerset S \to \powerset T$ is a surjection.
{{qed}}
{{AoC||4}}
Theorem: Direct Image Mapping of Surjection is Surjection

Let $f: S \to T$ be a surjection.
Then the direct image mapping of $f$:
:$f^\to: \powerset S \to \powerset T$
is a surjection.

Proof:
Let $f^\gets$ be the inverse image mapping of $f$.
Let $Y \in \powerset T$.
Let $X = \map {f^\gets} Y$.
By Subset equals Image of Preimage iff Mapping is Surjection:
:$\map {f^\to} X = Y$
As such an $X$ exists for each $Y \in \powerset S$, $f^\to$ is surjective.
{{qed}}