avewright/proofwiki-math huggingface dataset:
Theorem: Relation Partitions Set iff Equivalence

Let $\RR$ be a relation on a set $S$.
Then $S$ can be partitioned into subsets by $\RR$ {{iff}} $\RR$ is an equivalence relation on $S$.
The partition of $S$ defined by $\RR$ is the quotient set $S / \RR$.

Proof:
Let $\RR$ be an equivalence relation on $S$.
From the Fundamental Theorem on Equivalence Relations, we have that the equivalence classes of $\RR$ form a partition.
{{qed|lemma}}
Let $S$ be partitioned into subsets by a relation $\RR$.
From Relation Induced by Partition is Equivalence, $\RR$ is an equivalence relation.
{{qed}}
Theorem: Intersection of Equivalences

The intersection of two equivalence relations is itself an equivalence relation.

Proof:
Let $\RR_1$ and $\RR_2$ be equivalence relations on $S$.
Let $\RR_3 = \RR_1 \cap \RR_2$.
Checking in turn each of the criteria for equivalence:
Theorem: Union of Equivalences

The union of two equivalence relations is '''not''' necessarily an equivalence relation itself.

Proof:
This can be shown by giving an example.
Let $S = \set {a, b, c}$, and let $\RR_1$ and $\RR_2$ be equivalences on $S$ such that:
: $\eqclass a {\RR_1} = \eqclass b {\RR_1} = \set {a, b}$
: $\eqclass c {\RR_1} = \set c$
: $\eqclass a {\RR_2} = \set a$
: $\eqclass b {\RR_2} = \eqclass c {\RR_2} = \set {b, c}$
Let $\RR_3 = \RR_1 \cup \RR_2$.
Then:
{{begin-eqn}}
{{eqn | l = \tuple {a, b}
      | o = \in
      | r = \RR_1
      | c =
}}
{{eqn | l = \tuple {b, c}
      | o = \in
      | r = \RR_2
      | c =
}}
{{eqn | ll= \leadsto
      | l = \tuple {a, b}
      | o = \in
      | r = \RR_1 \cup \RR_2
      | c =
}}
{{eqn | lo= \land
      | l = \tuple {b, c}
      | o = \in
      | r = \RR_1 \cup \RR_2
      | c =
}}
{{eqn | ll= \leadsto
      | l = \tuple {a, b}
      | o = \in
      | r = \RR_3
      | c =
}}
{{eqn | lo= \land
      | l = \tuple {b, c}
      | o = \in
      | r = \RR_3
      | c =
}}
{{end-eqn}}
However:
{{begin-eqn}}
{{eqn | l = \tuple {a, c}
      | o = \notin
      | r = \RR_1
      | c = 
}}
{{eqn | lo= \land
      | l = \tuple {a, c}
      | o = \notin
      | r = \RR_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {a, c}
      | o = \notin
      | r = \RR_1 \cup \RR_2
      | c =
}}
{{eqn | ll= \leadsto
      | l = \tuple {a, c}
      | o = \notin
      | r = \RR_3
      | c = 
}}
{{end-eqn}}
So $\RR_3$ is not transitive, and therefore $\RR_3 = \RR_1 \cup \RR_2$ is not an equivalence relation.
{{qed}}
Theorem: Union of Equivalences

The union of two equivalence relations is '''not''' necessarily an equivalence relation itself.

Proof:
We have that the Union of Reflexive Relations is Reflexive.
We also have that the Union of Symmetric Relations is Symmetric.
However, we also have that the Union of Transitive Relations Not Always Transitive.
Hence the union of two equivalence relations is not always an equivalence relation.
{{qed}}
Theorem: Equivalence of Definitions of Equivalence Relation

Let $\RR$ be a relation on a set $S$.
{{TFAE|def = Equivalence Relation}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $\RR$ be an equivalence relation by definition 1.
By definition, $\RR$ is reflexive, symmetric and transitive.
From Relation Contains Diagonal Relation iff Reflexive:
:$\Delta_S \subseteq \RR$
From Relation equals Inverse iff Symmetric:
:$\RR^{-1} = \RR$
and so by definition of set equality:
:$\RR^{-1} \subseteq \RR$
From Relation contains Composite with Self iff Transitive:
:$\RR \circ \RR \subseteq \RR$
From Union is Smallest Superset:
:$\Delta_S \cup \RR^{-1} \cup \RR \circ \RR \subseteq \RR$
Thus $\RR$ is an equivalence relation by definition 2.
{{qed|lemma}}
Theorem: Equivalence iff Diagonal and Inverse Composite

Let $\RR$ be a relation on $S$.
Then $\RR$ is an equivalence relation on $S$ {{iff}}:
:$\Delta_S \subseteq \RR$
and:
:$\RR = \RR \circ \RR^{-1}$

Proof:
=== Necessary Condition ===
Let $\RR$ be an equivalence relation.
Then by definition, it is reflexive, symmetric and transitive.
As $\RR$ is reflexive, we have $\Delta_S \subseteq \RR$ from Relation Contains Diagonal Relation iff Reflexive.
As $\RR$ is transitive:
:$\RR \circ \RR \subseteq \RR$
from Relation contains Composite with Self iff Transitive.
But as $\RR$ is symmetric:
:$\RR = \RR^{-1}$
from Relation equals Inverse iff Symmetric.
Thus:
:$\RR \circ \RR^{-1} \subseteq \RR$
Now we need to show that $\RR \subseteq \RR \circ \RR^{-1}$:
Let $\tuple {x, y} \in \RR$.
Then as $\RR$ is reflexive:
:$\tuple {x, y} \in \RR \land \tuple {y, y} \in \RR$
and so:
:$\tuple {x, y} \in \RR \circ \RR$
As $\RR = \RR^{-1}$, it follows that:
:$\RR \subseteq \RR \circ \RR^{-1}$
So it has been shown:
:$\Delta_S \subseteq \RR$ and $\RR = \RR \circ \RR^{-1}$
{{qed|lemma}}
Theorem: Equality of Elements in Range of Mapping

Let $f: S \to T$ be a mapping.
Then:
:$\exists y \in \Rng f: \tuple {x_1, y} \in f \land \tuple {x_2, y} \in f \iff \map f {x_1} = \map f {x_2}$

Proof:
=== Necessary Condition ===
Let:
:$\exists y \in \Rng f: \tuple {x_1, y} \in f \land \tuple {x_2, y} \in f$
Then:
{{begin-eqn}}
{{eqn | o =
      | r = \tuple {x_1, y} \in f \land \tuple {x_2, y} \in f
      | c =
}}
{{eqn | o = \leadsto
      | r = \map f {x_1} = y \land \map f {x_2} = y
      | c = {{Defof|Mapping}}
}}
{{eqn | o = \leadsto
      | r = \map f {x_1} = \map f {x_2}
      | c = Equality is Equivalence Relation
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Inverse of Mapping is One-to-Many Relation

Let $f$ be a mapping.
Then its inverse $f^{-1}$ is a one-to-many relation.
Hence $f^{-1}$ is not necessarily a mapping itself.

Proof:
We have that $f$ is a mapping.
Hence $f$ is {{afortiori}} a many-to-one relation.
Then from Inverse of Many-to-One Relation is One-to-Many, $f^{-1}$ is one-to-many.
{{Qed}}
Theorem: Equality of Mappings

Two mappings $f_1: S_1 \to T_1, f_2: S_2 \to T_2$ are equal {{iff}}:
:$(1): \quad S_1 = S_2$
:$(2): \quad T_1 = T_2$
:$(3): \quad \forall x \in S_1: \map {f_1} x = \map {f_2} x$

Proof:
This follows directly from Equality of Relations.
{{qed}}
Theorem: Mapping is Constant iff Image is Singleton

A mapping is a constant mapping {{iff}} its image is a singleton.

Proof:
=== Necessary Condition ===
Let $f_c: S \to T$ be a constant mapping.
Then from the definition of the image of an element:
:$\forall x \in S: \map {f_c} x = c \implies \Img S = \set c$
Thus the image of $f_c: S \to T$ is a singleton.
{{qed|lemma}}
Theorem: Diagonal Relation is Right Identity

Let $\RR \subseteq S \times T$ be a relation on $S \times T$.
Then:
:$\RR \circ \Delta_S = \RR$
where $\Delta_S$ is the diagonal relation on $S$, and $\circ$ signifies composition of relations.

Proof:
{{Rewrite|In light of the more relaxed definition of composite of relation}}
We use the definition of relation equality, as follows:
Theorem: Identity Mapping is Left Identity

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Then:
:$I_T \circ f = f$
where $I_T$ is the identity mapping on $T$, and $\circ$ signifies composition of mappings.

Proof:
=== Equality of Domains ===
The domains of $f$ and $I_T \circ f$ are equal from Domain of Composite Relation:
:$\Dom {I_T \circ f} = \Dom f$
{{qed|lemma}}
=== Equality of Codomains ===
The codomains of $f$ and $f \circ I_S$ are also easily shown to be equal.
From Codomain of Composite Relation, the codomains of $I_T \circ f$ and $I_T$ are both equal to $T$.
But from the definition of the identity mapping, the codomain of $I_T$ is $\Dom {I_T} = T$
{{qed|lemma}}
=== Equality of Relations ===
The composite of $f$ and $I_T$ is defined as:
:$I_T \circ f = \set {\tuple {x, z} \in S \times T: \exists y \in T: \tuple {x, y} \in f \land \tuple {y, z} \in I_T}$
But by definition of the identity mapping on $T$, we have that:
:$\tuple {y, z} \in I_T \implies y = z$
Hence:
:$I_T \circ f = \set {\tuple {x, y} \in S \times T: \exists y \in T: \tuple {x, y} \in f \land \tuple {y, y} \in I_T}$
But as $\forall y \in T: \tuple {y, y} \in I_T$, this means:
:$I_T \circ f = \set {\tuple {x, y} \in S \times T: \tuple {x, y} \in f}$
That is:
:$I_T \circ f = f$
{{qed|lemma}}
Hence the result, by Equality of Mappings.
{{qed}}
Theorem: Identity Mapping is Left Identity

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Then:
:$I_T \circ f = f$
where $I_T$ is the identity mapping on $T$, and $\circ$ signifies composition of mappings.

Proof:
By definition, a mapping is also a relation.
Also by definition, the identity mapping is the same as the diagonal relation.
Thus Diagonal Relation is Left Identity can be applied directly.
{{qed}}
Theorem: Image of Element under Inverse Mapping

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping such that its inverse $f^{-1}: T \to S$ is also a mapping.
Then:
:$\forall x \in S, y \in T: \map f x = y \iff \map {f^{-1} } y = x$

Proof:
=== Sufficient Condition ===
Let $f: S \to T$ be a mapping.
From the definition of inverse mapping:
:$f^{-1} = \set {\tuple {y, x}: \tuple {x, y} \in f}$
Let $y = \map f x$.
From the definition of the preimage of an element:
:$\map {f^{-1} } y = \set {s \in S: \tuple {y, x} \in f}$
Thus:
:$x \in \map {f^{-1} } y$
However, $f^{-1}$ is a mapping.
Therefore, by definition:
:$\forall y \in T: \tuple {y, x_1} \in f^{-1} \land \tuple {y, x_2} \in f^{-1} \implies x_1 = x_2$
Thus:
:$\forall s \in \map {f^{-1} } y: s = x$
Thus:
:$\map {f^{-1} } y = \set x$
That is:
:$x = \map {f^{-1} } y$
{{qed|lemma}}
Theorem: Injection iff Left Cancellable

A mapping $f$ is an injection {{iff}} $f$ is left cancellable.

Proof:
From the definition: a mapping $f: Y \to Z$ is left cancellable {{iff}}:
:$\forall X: \forall g_1: X \to Y, g_2: X \to Y: f \circ g_1 = f \circ g_2 \implies g_1 = g_2$
Theorem: Identity Mapping is Injection

On any set $S$, the identity mapping $I_S: S \to S$ is an injection.

Proof:
From the definition of the identity mapping:
:$\forall x \in S: \map {I_S} x = x$
So:
:$\map {I_S} x = \map {I_S} y \implies x = y$
So by definition $I_S$ is an injection.
{{Qed}}
Theorem: Composite of Injections is Injection

A composite of injections is an injection.
That is:
:If $f$ and $g$ are injections, then so is $f \circ g$.

Proof:
Let $f$ and $g$ be injections.
Then:
{{begin-eqn}}
{{eqn | l = \map {f \circ g} x
      | r = \map {f \circ g} y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map f {\map g x}
      | r = \map f {\map g y}
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | ll= \leadsto
      | l = \map g x
      | r = \map g y
      | c = as $f$ is injective
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = as $g$ is injective
}}
{{end-eqn}}
{{qed}}
Theorem: Injection if Composite is Injection

Let $f$ and $g$ be mappings such that their composite $g \circ f$ is an injection.
Then $f$ is an injection.

Proof:
Let $g \circ f$ be injective.
We need to show that $\map f a = \map f b \implies a = b$.
So suppose $\map f a = \map f b$.
Then:
{{begin-eqn}}
{{eqn | l = \map {g \circ f} a
      | r = \map g {\map f a}
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map g {\map f b}
      | c = by hypothesis
}}
{{eqn | r = \map {g \circ f} b
      | c = {{Defof|Composition of Mappings}}
}}
{{end-eqn}}
and so $a = b$ as $g \circ f$ is an injection.
So we have shown that:
:$\map f a = \map f b \implies a = b$
Hence the result from the definition of injection.
{{qed}}
Theorem: Injection iff Left Inverse

A mapping $f: S \to T, S \ne \O$ is an injection {{iff}}:
:$\exists g: T \to S: g \circ f = I_S$
where $g$ is a mapping.
That is, {{iff}} $f$ has a left inverse.

Proof:
Let:
:$\exists g: T \to S: g \circ f = I_S$
From Identity Mapping is Injection, $I_S$ is injective, so $g \circ f$ is injective.
So from Injection if Composite is Injection, $f$ is an injection.
Note that the existence of such a $g$ ''requires'' that $S \ne \O$.
{{qed|lemma}}
Now, assume $f$ is an injection.
We now define a mapping $g: T \to S$ as follows.
As $S \ne \O$, we choose $x_0 \in S$.
By definition of injection:
:$f^{-1} {\restriction_{\Img f} } \to S$ is a mapping
so it is possible to define:
:<nowiki>$\map g y = \begin{cases}
x_0: & y \in T \setminus \Img f \\
\map {f^{-1} } y: & y \in \Img f \end{cases}$</nowiki>
:750px
It does not matter what the elements of $T \setminus \Img f$ are.
Using the construction given, the equation $g \circ f = I_S$ holds whatever value (or values) we choose for $g \sqbrk {T \setminus \Img f}$.
The remaining elements of $T$ can be mapped arbitrarily, and will not affect the image of any $x \in S$ under the mapping $g \circ f$.
So, for all $x \in S$:
:$\map {g \circ f} x = \map g {\map f x}$
is the unique element of $S$ which $f$ maps to $\map f x$.
This unique element is $x$.
Thus $g \circ f = I_S$.
{{Qed}}
Theorem: Injection iff Left Inverse

A mapping $f: S \to T, S \ne \O$ is an injection {{iff}}:
:$\exists g: T \to S: g \circ f = I_S$
where $g$ is a mapping.
That is, {{iff}} $f$ has a left inverse.

Proof:
Take the result Condition for Composite Mapping on Left:
Let $A, B, C$ be sets.
Let $f: A \to B$ and $g: A \to C$ be mappings.
Then:
:$\forall x, y \in A: \map f x = \map f y \implies \map g x = \map g y$
{{iff}}:
:$\exists h: B \to C$ such that $h$ is a mapping and $h \circ f = g$.
Let $C = A = S$, let $B = T$ and let $g = I_S$.
Then the above translates into:
:$\exists h: T \to S$ such that $h$ is a mapping and $h \circ f = g$
{{iff}}:
:$\forall x, y \in S: \map f x = \map f y \implies \map {I_S} x = \map {I_S} y$
But as $\map {I_S} x = x$ and $\map {I_S} y = y$ by definition of identity mapping, it follows that:
:$\exists h: T \to S$ such that $h$ is a mapping and $h \circ f = g$
{{iff}}:
:$\forall x, y \in S: \map f x = \map f y \implies x = y$
which is our result.
{{qed}}
Theorem: Injection iff Left Inverse

A mapping $f: S \to T, S \ne \O$ is an injection {{iff}}:
:$\exists g: T \to S: g \circ f = I_S$
where $g$ is a mapping.
That is, {{iff}} $f$ has a left inverse.

Proof:
Let $f: S \to T$ be an injection.
Then $f$ is a one-to-many relation.
By Inverse of Many-to-One Relation is One-to-Many, $f^{-1}: T \to S$ is many-to-one.
By Many-to-One Relation Extends to Mapping, there is a mapping $g: T \to S$ such that:
:$f^{-1} \subseteq g$
Let $\tuple {x, y} \in g \circ f$.
Then:
:$\exists z \in T: \tuple {x, z} \in f, \tuple {z, y} \in g$
Since $\tuple {x, z} \in f$:
:$\tuple {z, x} \in f^{-1} \subseteq g$
Since $\tuple {z, y} \in g$, $\tuple {z, x} \in g$ and $g$ is a mapping:
:$x = y$
so:
:$\tuple {x, y} \in I_S$
So we see that:
:$g \circ f \subseteq I_S$
Let $x \in S$.
Then:
:$\tuple {x, \map f x} \in f$
and:
:$\tuple {\map f x, x} \in f^{-1} \subseteq g$
So:
:$\tuple {x, x} \in g \circ f$
Thus:
:$I_S \subseteq g \circ f$
By definition of set equality:
:$I_S = g \circ f$
{{qed}}
Theorem: Inclusion Mapping is Injection

Let $S, T$ be sets such that $S$ is a subset of $T$.
Then the inclusion mapping $i_S: S \to T$ defined as:
:$\forall x \in S: \map {i_S} x = x$
is an injection.
For this reason the inclusion mapping can be known as the '''canonical injection of $S$ to $T$'''.

Proof:
Suppose $\map {i_S} {s_1} = \map {i_S} {s_2}$.
{{begin-eqn}}
{{eqn | l = \map {i_S} {s_1}
      | r = s_1
      | c = {{Defof|Inclusion Mapping}}
}}
{{eqn | l = \map {i_S} {s_2}
      | r = s_2
      | c = {{Defof|Inclusion Mapping}}
}}
{{eqn | l = \map {i_S} {s_1}
      | r = \map {i_S} {s_2}
      | c = by definition
}}
{{eqn | ll= \leadsto
      | l = s_1
      | r = s_2
      | c = from above
}}
{{end-eqn}}
Thus $i_S$ is an injection by definition.
{{qed}}
Theorem: Surjection iff Right Cancellable

Let $f$ be a mapping.
Then $f$ is a surjection {{iff}} $f$ is right cancellable.

Proof:
Let $f: X \to Y$ be surjective.
Let $h_1: Y \to Z, h_2: Y \to Z: h_1 \circ f = h_2 \circ f$.
As $f$ is a surjection:
:$\Img f = Y$
by definition.
But in order for $h_1 \circ f$ to be defined, it is necessary that $Y = \Dom {h_1}$.
Similarly, for $h_2 \circ f$ to be defined, it is necessary that $Y = \Dom {h_2}$.
So it follows that the domains of $h_1$ and $h_2$ are the same.
Also:
:The codomain of $h_1$ equals the codomain of $h_1 \circ f$
:The codomain of $h_2$ equals the codomain of $h_2 \circ f$
again by definition of composition of mappings.
Now, we have shown that the domains and codomains of $h_1$ and $h_2$ are the same.
All we need to do now to prove that $h_1 = h_2$, and therefore that $f$ is right cancellable, is to show that:
:$\forall y \in Y: h_1 \paren y = h_2 \paren y$.
So, let $y \in Y$.
As $f$ is surjective:
: $\exists x \in X: y = f \paren x$
Thus:
{{begin-eqn}}
{{eqn | l = h_1 \paren y
      | r = h_1 \paren {f \paren x}
      | c = Definition of $y$
}}
{{eqn | r = h_1 \circ f \paren x
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = h_2 \circ f \paren x
      | c = By Hypothesis
}}
{{eqn | r = h_2 \paren {f \paren x}
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = h_2 \paren y
      | c = Definition of $y$
}}
{{end-eqn}}
Thus $h_1 \paren y = h_2 \paren y$ and thus $f$ is right cancellable.
Theorem: Surjection iff Right Cancellable

Let $f$ be a mapping.
Then $f$ is a surjection {{iff}} $f$ is right cancellable.

Proof:
Let $f: X \to Y$ be surjective.
Then from Surjection iff Right Inverse:
:$\exists g: Y \to X: f \circ g = I_Y$
Suppose $h \circ f = k \circ f$ for two mappings $h: Y \to Z$ and $k: Y \to Z$.
Then:
{{begin-eqn}}
{{eqn | l = h
      | r = h \circ I_Y
      | c = 
}}
{{eqn | r = h \circ \paren {f \circ g}
      | c = 
}}
{{eqn | r = \paren {h \circ f} \circ g
      | c = Composition of Mappings is Associative
}}
{{eqn | r = \paren {k \circ f} \circ g
      | c = by hypothesis
}}
{{eqn | r = k \circ \paren {f \circ g}
      | c = Composition of Mappings is Associative
}}
{{eqn | r = k \circ I_Y
      | c = 
}}
{{eqn | r = k
      | c = 
}}
{{end-eqn}}
Thus $f$ is right cancellable.
So surjectivity implies right cancellability.
Theorem: Surjection iff Right Cancellable

Let $f$ be a mapping.
Then $f$ is a surjection {{iff}} $f$ is right cancellable.

Proof:
Suppose $f$ is a mapping which is not surjective.
Then:
:$\exists y_1 \in Y: \neg \exists x \in X: \map f x = y_1$
Let $Z = \set {a, b}$.
Let $h_1$ and $h_2$ be defined as follows. 
:$\map {h_1} y = a: y \in Y$
:<nowiki>$\map {h_2} y = \begin {cases}
a & : y \ne y_1 \\
b & : y = y_1
\end {cases}$</nowiki>
Thus we have $h_1 \ne h_2$ such that $h_1 \circ f = h_2 \circ f$.
Therefore $f$ is not right cancellable.
It follows from the Rule of Transposition that if $f$ is right cancellable, then $f$ must be surjective.
Theorem: Surjection iff Right Cancellable

Let $f$ be a mapping.
Then $f$ is a surjection {{iff}} $f$ is right cancellable.

Proof:
Let $f: X \to Y$ be a right cancellable mapping.
Let $Y$ contain exactly one element.
Then by definition $Y$ is a singleton.
From Mapping to Singleton is Surjection it follows that $f$ is a surjection.
So let $Y$ contain at least two elements.
Call those two elements $a$ and $b$, and we note that $a \ne b$.
We define the two mappings $h, k$ as follows:
:<nowiki>$h: Y \to Y: \forall y \in Y: \map h y = \begin{cases}
y & : y \in \Img f \\
a & : y \notin \Img f
\end{cases}$</nowiki>
:<nowiki>$k: Y \to Y: \forall y \in Y: \map k y = \begin{cases}
y & : y \in \Img f \\
b & : y \notin \Img f
\end{cases}$</nowiki>
It is clear that:
:$\forall x \in X: \map h {\map f x} = \map f x = \map k {\map f x}$
and so:
:$h \circ f = k \circ f$
But by hypothesis, $f$ is right cancellable.
Thus $h = k$.
{{AimForCont}} $Y \ne \Img f$.
Then:
:$\Img f \subsetneq Y$
That is:
:$\exists y \in Y: y \notin \Img f$
It follows that:
:$a = \map h y = \map k y = b$
But we posited that $a \ne b$.
From this contradiction we conclude that:
:$Y = \Img f$
So, by definition, $f$ must be a surjection.
Theorem: Identity Mapping is Surjection

On any set $S$, the identity mapping $I_S: S \to S$ is a surjection.

Proof:
The identity mapping is defined as:
:$\forall y \in S: \map {I_S} y = y$
Then we have:
{{begin-eqn}}
{{eqn | q = \forall y \in S: \exists x \in S
      | l = x
      | r = y
      | c = that is, $y$ itself
}}
{{eqn | ll= \leadsto
      | q = \forall y \in S: \exists x \in S
      | l = \map {I_S} x
      | r = y
      | c = Definition of $I_S$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Restriction of Mapping to Image is Surjection

Let $f: S \to T$ be a mapping.
Let $g: S \to \Img f$ be the restriction of $f$ to $S \times \Img f$.
Then $g$ is a surjective restriction of $f$.

Proof:
From Image is Subset of Codomain:
:$\Img g \subseteq T$
Furthermore, by definition of image, we have:
:$\forall s \in S: g \paren s \in \Img g$
Therefore, $g$ may be viewed as a mapping $g: S \to \Img g$.
Thus, by definition, $g$ is a surjection.
{{qed}}
Theorem: Composite of Surjections is Surjection

A composite of surjections is a surjection.
That is:
:If $g$ and $f$ are surjections, then so is $g \circ f$.

Proof:
Let $f: S_1 \to S_2$ and $g: S_2 \to S_3$ be surjections.
Then:
{{begin-eqn}}
{{eqn | q = \forall z \in S_3: \exists y \in S_2
      | l = \map g y
      | r = z
      | c = {{Defof|Surjection}}
}}
{{eqn | ll= \leadsto
      | q = \exists x \in S_1
      | l = \map f x
      | r = y
      | c = {{Defof|Surjection}}
}}
{{end-eqn}}
By definition of a composite mapping:
:$\map {g \circ f} x = \map g {\map f x} = \map g y = z$
Hence $g \circ f$ is surjective.
{{qed}}
Theorem: Surjection if Composite is Surjection

Let $f: S_1 \to S_2$ and $g: S_2 \to S_3$ be mappings such that $g \circ f$ is a surjection.
Then $g$ is a surjection.

Proof:
Let $g \circ f$ be surjective.
Fix $z \in S_3$. 
Now find an $x \in S_1: \map {g \circ f} x = z$.
The surjectivity of $g \circ f$ guarantees this can be done.
Now find an $y \in S_2: f \paren x = y$.
$f$ is a mapping and therefore a left-total relation; which guarantees this too can be done.
It follows that:
{{begin-eqn}}
{{eqn | l = \map g y
      | r = \map g {\map f x}
}}
{{eqn | r = \map {g \circ f} x
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = z
      | c = Choice of $x$
}}
{{end-eqn}}
{{qed}}
Theorem: Surjection iff Right Inverse

A mapping $f: S \to T, S \ne \O$ is a surjection {{iff}}:
:$\exists g: T \to S: f \circ g = I_T$
where:
:$g$ is a mapping
:$I_T$ is the identity mapping on $T$.
That is, {{iff}} $f$ has a right inverse.

Proof:
Assume $\exists g: T \to S: f \circ g = I_T$.
From Identity Mapping is Surjection, $I_T$ is surjective, so $f \circ g$ is surjective.
So from Surjection if Composite is Surjection, $f$ is a surjection.
Note that the existence of such a $g$ ''requires'' that $S$ is non-empty.
Now, assume $f$ is a surjection.
Consider the indexed family of non-empty sets $\set {\map {f^{-1} } y}_{y \mathop \in T}$ where $\map {f^{-1} } y$ denotes the preimage of $y$ under $f$.
Using the axiom of choice, there exists a mapping $g: T \to S$ such that $\map g y \in \set {\map {f^{-1} } y}$ for all $y \in T$.
:550px
That is, $\map {\paren {f \circ g} } y = y$, as desired.
{{qed}}
Theorem: Surjection iff Right Inverse

A mapping $f: S \to T, S \ne \O$ is a surjection {{iff}}:
:$\exists g: T \to S: f \circ g = I_T$
where:
:$g$ is a mapping
:$I_T$ is the identity mapping on $T$.
That is, {{iff}} $f$ has a right inverse.

Proof:
Take the result Condition for Composite Mapping on Right:
Let $A, B, C$ be sets.
Let $f: B \to A$ and $g: C \to A$ be mappings.
Then:
:$\Img g \subseteq \Img f$
{{iff}}:
:$\exists h: C \to B$ such that $h$ is a mapping and $f \circ h = g$.
Let $C = A = T$, let $B = S$ and let $g = I_T$.
Then the above translates into:
:$\Img {I_T} \subseteq \Img f$
{{iff}}:
:$\exists g: T \to S$ such that $g$ is a mapping and $f \circ g = I_T$.
But we know that:
:$\Img f \subseteq T = \Img {I_T}$
So by definition of set equality, the result follows.
{{qed}}
Theorem: Identity Mapping is Bijection

The identity mapping $I_S: S \to S$ on the set $S$ is a bijection.

Proof:
The identity mapping is:
:an injection, from Identity Mapping is Injection
:a surjection, from Identity Mapping is Surjection
and therefore a bijection.
{{qed}}
Theorem: Identity Mapping is Permutation

The identity mapping $I_S: S \to S$ on the set $S$ is a permutation.

Proof:
The identity mapping $I_S$ is a bijection from $S$ to itself, by Identity Mapping is Bijection.
{{qed}}