avewright/proofwiki-math huggingface dataset:
Theorem: Inclusion of Natural Numbers in Integers is Epimorphism

Let $\mathbf{Mon}$ be the category of monoids.
Let $\struct {\N, +}$ denote the monoid of natural numbers as on Natural Numbers under Addition form Commutative Monoid.
Let $\struct {\Z, +}$ denote the additive group of integers.
Denote with $\iota: \N \to \Z$ the inclusion mapping.
Then $\iota: \N \to \Z$ is an epimorphism in $\mathbf{Mon}$.

Proof:
Let $\struct {M, \circ}$ be a monoid with identity $e$.
Let $f, g: \Z \to M$ be monoid homomorphisms such that:
:$f \circ \iota = g \circ \iota$
that is, by definition of inclusion, such that:
:$\forall n \in \N: \map f n = \map g n$
Now $\iota$ will be epic if we can show that $f = g$.
The morphism property of $f$ and $g$ yields that, for any $m > 0$:
:$\map f {- m} = \map f {-1} \circ \cdots \circ \map f {-1}$
:$\map g {- m} = \map g {-1} \circ \cdots \circ \map g {-1}$
with on the {{RHS}} $m$ copies of $\map f {-1}$ and $\map g {-1}$, respectively.
It thus is necessary and sufficient to show that $\map f {-1} = \map g {-1}$.
To this end, compute:
{{begin-eqn}}
{{eqn|l = \map f {-1}
     |r = \map f {-1} \circ e
     |c = {{Defof|Identity Element}}
}}
{{eqn|r = \map f {-1} \circ \map g 0
     |c = {{Defof|Monoid Homomorphism}}
}}
{{eqn|r = \map f {-1} \circ \map g {1 + \paren {-1} }
}}
{{eqn|r = \map f {-1} \circ \map g 1 \circ \map g {-1}
     |c = {{Defof|Monoid Homomorphism}}
}}
{{eqn|r = \map f {-1} \circ \map f 1 \circ \map g {-1}
     |c = By the assumption on $f$ and $g$
}}
{{eqn|r = \map f {\paren {-1} + 1} \circ \map g {-1}
     |c = {{Defof|Monoid Homomorphism}}
}}
{{eqn|r = \map f 0 \circ \map g {-1}
}}
{{eqn|r = e \circ \map g {-1}
     |c = {{Defof|Monoid Homomorphism}}
}}
{{eqn|r = \map g {-1}
     |c = {{Defof|Identity Element}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Isomorphism (Category Theory) is Monic

Let $\mathbf C$ be a metacategory.
Let $C$ and $D$ be objects of $\mathbf C$.
Let $f: C \to D$ be an isomorphism.
Then $f: C \rightarrowtail D$ is monic.

Proof:
Since $f$ is an isomorphism, it is a fortiori a split monomorphism.
The result follows from Split Monomorphism is Monic.
{{qed}}
Theorem: Stabilizer of Polynomial

Let $n \in \Z: n > 0$.
Let $\map f {x_1, x_2, \ldots, x_n}$ be a polynomial in $n$ variables $x_1, x_2, \ldots, x_n$.
Let $S_n$ denote the symmetric group on $n$ letters.
Let $\pi, \rho \in S_n$.
Let the group action $\pi * f$ be defined as the permutation on the polynomial $f$ by $\pi$.
Then the stabilizer of $f$ is the set of permutations on $n$ letters which fix $f$.

Proof:
Follows directly from the definition of the stabilizer of $f$.
{{qed}}
Theorem: Stabilizer of Element of Group Acting on Itself is Trivial

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $*$ be the group action of $\struct {G, \circ}$ on itself by the rule:
:$\forall g, h \in G: g * h = g \circ h$
Then the stabilizer of an element $x \in G$ is given by:
:$\Stab x = \set e$

Proof:
Let $g \in \Stab x$.
Then:
{{begin-eqn}}
{{eqn | l = g * x
      | r = x
      | c = {{Defof|Stabilizer}}
}}
{{eqn | ll= \leadsto
      | l = g \circ x
      | r = x
      | c = {{Defof|Group Action}} (this particular one)
}}
{{eqn | ll= \leadsto
      | l = g
      | r = e
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
Hence the result, by definition of trivial subgroup.
{{qed}}
Theorem: Stabilizer of Element under Conjugacy Action is Centralizer

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $*$ be the conjugacy action on $G$ defined by the rule:
:$\forall g, h \in G: g * h = g \circ h \circ g^{-1}$
Let $x \in G$.
Then the stabilizer of $x$ under this conjugacy action is:
:$\Stab x = \map {C_G} x$
where $\map {C_G} x$ is the centralizer of $x$ in $G$.

Proof:
From the definition of centralizer:
:$\map {C_G} x = \set {g \in G: g \circ x = x \circ g}$
Then:
{{begin-eqn}}
{{eqn | l = z
      | o = \in
      | r = \Stab x
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = z
      | o = \in
      | r = \set {g \in G: g \circ x \circ g^{-1} = x}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = z
      | o = \in
      | r = \set {g \in G: g \circ x = x \circ g}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Stabilizer of Subset Product Action on Power Set

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $\powerset G$ be the power set of $\struct {G, \circ}$.
Let $*: G \times \powerset G \to \powerset G$ be the subset product action on $\powerset G$ defined as:
:$\forall g \in G: \forall S \in \powerset G: g * S = g \circ S$
where $g \circ S$ is the subset product $\set g \circ S$.
Then the stabilizer of $S$ in $\powerset G$ is the set:
:$\Stab S = S$

Proof:
From the definition of stabilizer:
:$\Stab S = \set {g \in G: g * S = S}$
The result follows from the definition of the group action $*$ given.
{{qed}}
Theorem: Stabilizer of Coset Action on Set of Subgroups

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $\powerset G$ denote the power set of $G$.
Let $\HH \subseteq \powerset G$ denote the set of subgroups of $G$.
Let $*$ be the subset product action on $\HH \subseteq \powerset G$ defined as:
:$\forall g \in G: \forall H \in \HH: g * H = g \circ H$
where $g \circ H$ is the (left) coset of $g$ by $H$.
Then the stabilizer of $H$ in $\powerset G$ is $H$ itself:
:$\Stab H = H$

Proof:
From the definition of Stabilizer of Subset Product Action on Power Set:
:$\Stab H = H = \set {g \in G: g * H = H}$
The result follows from Left Coset Equals Subgroup iff Element in Subgroup.
{{qed}}
Theorem: Isomorphism (Category Theory) is Epic

Let $\mathbf C$ be a metacategory.
Let $C$ and $D$ be objects of $\mathbf C$.
Let $f: C \to D$ be an isomorphism.
Then $f: C \twoheadrightarrow D$ is epic.

Proof:
Since $f$ is an isomorphism, it is a fortiori a split epimorphism.
The result follows from Split Epimorphism is Epic.
{{qed}}
Theorem: Split Epimorphism is Epic

Let $\mathbf C$ be a metacategory.
Let $C$ and $D$ be objects of $\mathbf C$.
Let $f: C \to D$ be a split epimorphism.
Then $f: C \twoheadrightarrow D$ is epic.

Proof:
Let $g: D \to C$ be a morphism such that:
:$f \circ g = \operatorname{id}_D$
which is guaranteed to exist by definition of a split epimorphism.
Suppose $x, y: D \to E$ are morphisms, such that:
:$x \circ f = y \circ f$
Then:
:$x \circ f \circ g = y \circ f \circ g$
Hence:
:$f \circ g = \operatorname{id}_D$
It follows that:
:$x \circ \operatorname{id}_D = y \circ \operatorname{id}_D$
which yields the result, by the definition of an identity morphism.
The situation is illustrated by the following commutative diagram:
$\quad\quad \begin{xy}
<0em,0em> *+{C} = "C",
<0em,-4em>*+{D} = "D",
<4em,0em> *+{D} = "D2",
<8em,0em> *+{E} = "E",
"D2"+/r.5em/+/^.25em/;"E"+/l.5em/+/^.25em/ **@{-} ?>*@{>} ?*!/_.6em/{x},
"D2"+/r.5em/+/_.25em/;"E"+/l.5em/+/_.25em/ **@{-} ?>*@{>} ?*!/^.6em/{y},
"C";"D2"  **@{-} ?>*@{>} ?*!/_.6em/{f},
"D";"D2" **@{-} ?>*@{>} ?*!/^.6em/{\operatorname{id}_C},
"D";"C" **@{-} ?>*@{>} ?*!/_.6em/{g},
\end{xy}$
{{qed}}
Theorem: Split Monomorphism is Monic

Let $\mathbf C$ be a metacategory.
Let $C$ and $D$ be objects of $\mathbf C$.
Let $f: C \to D$ be a split monomorphism.
Then $f: C \rightarrowtail D$ is monic.

Proof:
Let $g: D \to C$ be a morphism such that:
:$g \circ f = \operatorname{id}_C$
which is guaranteed to exist by definition of split monomorphism.
Suppose that $x, y: B \to C$ are morphisms such that:
:$f \circ x = f \circ y$
Then necessarily also:
:$g \circ \paren {f \circ x} = g \circ \paren {f \circ y}$
and by Composition of Morphisms is Associative:
:$\paren {g \circ f} \circ x = \paren {g \circ f} \circ y$
We are given that $g \circ f = \operatorname{id}_C$.
Hence:
:${\operatorname{id}_C} \circ x = {\operatorname{id}_C} \circ y$
So by definition of identity morphism:
:$x = y$
Let $\mathbf C_1$ denotes the collection  morphisms $f, g, h, \ldots$ between its objects for the metacategory $\mathbf C$.
We have that $f \in \mathbf C_1$ such that:
:$f \circ x = f \circ y \implies x = y$
for all morphisms $x, y \in \mathbf C_1$ for which these compositions are defined.
Hence the result by definition of monic.
The situation is illustrated by the following commutative diagram:
:<nowiki>$\begin{xy}
<-4em,0em>*+{B} = "B",
<0em,0em> *+{C} = "C",
<4em,0em> *+{D} = "D",
<4em,-4em>*+{C} = "C2",
"B"+/r.5em/+/^.25em/;"C"+/l.5em/+/^.25em/ **@{-} ?>*@{>} ?*!/_.6em/{x},
"B"+/r.5em/+/_.25em/;"C"+/l.5em/+/_.25em/ **@{-} ?>*@{>} ?*!/^.6em/{y},
"C";"D"  **@{-} ?>*@{>} ?*!/_.6em/{f},
"C";"C2" **@{-} ?>*@{>} ?*!/^.6em/{\operatorname{id}_C},
"D";"C2" **@{-} ?>*@{>} ?*!/_.6em/{g},
\end{xy}$</nowiki>
{{qed}}
Theorem: Epimorphism into Projective Object Splits

Let $\mathbf C$ be a metacategory.
Let $P \in \mathbf C_0$ be a projective object of $\mathbf C$.
Let $e: E \twoheadrightarrow P$ be an epimorphism.
Then $e$ is a split epimorphism, i.e. it admits a retraction $f: P \to E$.

Proof:
Consider the identity morphism $\operatorname{id}_P: P \to P$.
By definition of projective object, we obtain the following commutative diagram:
$\quad\quad \begin{xy}
<0em,0em>*+{P} = "P",
<4em,0em>*+{P} = "P2",
<4em,4em>*+{E} = "E",
"P";"E" **@{-} ?>*@{>} ?*!/_.6em/{f},
"P";"P2" **@{-} ?>*@{>} ?*!/^.6em/{\operatorname{id}_P},
"E";"P2" **@{-} ?>*@2{>} ?<>(.7)*{\vee} ?*!/_.6em/{e},
\end{xy}$
where $f = \bar{\operatorname{id}_P}$.
It follows that $e \circ f = \operatorname{id}_P$, and so $e$ is a split epimorphism.
{{qed}}
Theorem: Relational Closure Exists for Set-Like Relation

Let $A$ be a class.
Let $\prec$ be a relation on $A$.
Furthermore, let $\map {\prec^{-1} } a$ be a small class for each $a \in A$.
Let $S$ be a small class that is a subset of the class $A$.
Let $G$ be a mapping such that:
:$\map G x = A \cap \paren {\map {\prec^{-1} } x}$
Let $F$ be defined using the Principle of Recursive Definition:
:$\map F 0 = S$
:$\map F {n^+} = \map F n \cup \map G {\map F n}$
Let $\ds T = \bigcup_{n \mathop \in \omega} \map F n$.
Then:
:$(1): \quad T$ is a set and satisfies:
::::$\forall x \in A: \forall y \in T: \paren {x \prec y \implies x \in T}$
::::In other words, $T$ is $\prec$-transitive.
:$(2): \quad S \subseteq T$
:$(3): \quad$ If $R$ is $\prec$-transitive and $S \subseteq R$, then $T \subseteq R$.
That is, given any set $S$, there is an explicit construction for its relational closure.

Proof:
=== Proof of $(1)$ ===
Let $x \in A$ and $y \in T$ such that $x \prec y$.
Then by definition:
:$x \in \map {\prec^{-1} } y$
Moreover, since $y \in T$:
:$\exists n \in \omega: y \in \map F n$
Therefore:
:$x \in \map F {n + 1}$
and so:
:$x \in T$
{{qed|lemma}}
Theorem: Well-Founded Proper Relational Structure Determines Minimal Elements

Let $A$ and $B$ be classes.
Let $\struct {A, \prec}$ be a proper relational structure.
Let $\prec$ be a strictly well-founded relation.
Suppose $B \subset A$ and $B \ne \O$.
Then $B$ has a strictly minimal element under $\prec$.

Proof:
$B$ is not empty.
So $B$ has at least one element $x$.
By Singleton of Element is Subset:
:$\set x \subseteq B$
By Relational Closure Exists for Set-Like Relation:
:$\set x$ has a $\prec$-relational closure.
{{explain|Set-like relation: it needs to be shown that $\prec$ is one of those.}}
This $\prec$-relational closure shall be denoted $y$.
By Intersection is Subset:
:$y \cap B \subseteq A$
As $x \in y$ and $x \in B$:
:$y \cap B \ne \O$
By the definition of strictly well-founded relation:
:$(1): \quad \exists x \in \paren {y \cap B}: \forall w \in \paren {y \cap B}: w \nprec x$
{{AimForCont}} that $w \in B$ such that $w \prec x$.
Since $x \in y$, it follows that $w \in y$, so $w \in \paren {B \cap y}$ by the definition of intersection.
This contradicts $(1)$.
Therefore:
:$w \nprec x$
and so $B$ has a strictly minimal element under $\prec$.
{{qed}}
Theorem: Initial Object is Unique

Let $\mathbf C$ be a metacategory.
Let $0$ and $0'$ be two initial objects of $\mathbf C$.
Then there is a unique isomorphism $u: 0 \to 0'$.
Hence, initial objects are unique up to unique isomorphism.

Proof:
Consider the following commutative diagram:
$\quad\quad \begin{xy}
<-4em,0em>*+{0} = "M",
<0em,0em> *+{0'}= "N",
<0em,-4em>*+{0} = "M2",
<4em,-4em>*+{0'}= "N2",
"M";"N"  **@{-} ?>*@{>} ?*!/_.6em/{u},
"M";"M2" **@{-} ?>*@{>} ?*!/^.6em/{\operatorname{id}_0},
"N";"M2" **@{-} ?>*@{>} ?*!/_.6em/{v},
"N";"N2" **@{-} ?>*@{>} ?*!/_1em/{\operatorname{id}_{0'}},
"M2";"N2"**@{-} ?>*@{>} ?*!/^.6em/{u},
\end{xy}$
It commutes as each of the morphisms in it originates from an initial object, and hence is unique.
Thus, $v$ is an inverse to $u$, and so $u$ is an isomorphism.
{{qed}}
Theorem: Terminal Object is Unique

Let $\mathbf C$ be a metacategory.
Let $1$ and $1'$ be two terminal objects of $\mathbf C$.
Then there is a unique isomorphism $u: 1 \to 1'$.
Hence, terminal objects are unique up to unique isomorphism.

Proof:
Consider the following commutative diagram:
$\quad\quad \begin{xy}
<-4em,0em>*+{1} = "M",
<0em,0em> *+{1'}= "N",
<0em,-4em>*+{1} = "M2",
<4em,-4em>*+{1'}= "N2",
"M";"N"  **@{-} ?>*@{>} ?*!/_.6em/{u},
"M";"M2" **@{-} ?>*@{>} ?*!/^.6em/{\operatorname{id}_1},
"N";"M2" **@{-} ?>*@{>} ?*!/_.6em/{v},
"N";"N2" **@{-} ?>*@{>} ?*!/_1em/{\operatorname{id}_{1'}},
"M2";"N2"**@{-} ?>*@{>} ?*!/^.6em/{u},
\end{xy}$
It commutes, as each of the morphisms in it points to a terminal object, and hence is unique.
Thus, $v$ is an inverse to $u$, and so $u$ is an isomorphism.
{{qed}}
Theorem: Empty Set is Initial Object

Let $\mathbf{Set}$ be the category of sets.
Then the empty set $\O$ is an initial object of $\mathbf{Set}$.

Proof:
Follows from Empty Mapping is Unique and the definition of initial object.
{{qed}}
Theorem: Singleton is Terminal Object of Category of Sets

Let $\mathbf {Set}$ be the category of sets.
Let $S = \set x$ be any singleton set.
Then $S$ is a terminal object of $\mathbf {Set}$.

Proof:
Let $T$ be a set, and let $f: T \to S$ be a mapping.
Then since for all $t \in T$, we have $\map f t \in S$, it follows that:
:$\forall t \in T: \map f t = x$
By Equality of Mappings, there is precisely one such mapping $f: T \to S$.
Hence the result, by definition of terminal object.
{{qed}}
Theorem: Zero (Category) is Initial Object

Let $\mathbf{Cat}$ be the category of categories.
Let $\mathbf 0$ be the zero category.
Then $\mathbf 0$ is an initial object of $\mathbf{Cat}$.

Proof:
Let $\mathbf C$ be an object of $\mathbf{Cat}$, i.e. a small category.
By Empty Mapping is Unique, there are unique mappings:
:$F_0: \mathbf 0_0 = \O \to \mathbf C_0$
:$F_1: \mathbf 0_1 = \O \to \mathbf C_1$
making $F: \mathbf 0 \to \mathbf C$ a functor by vacuous truth.
That $F_0$ and $F_1$ are actually mappings follows from $\mathbf C$ being a small category.
Hence the result, by definition of initial object.
{{qed}}
Theorem: One (Category) is Terminal Object

Let $\mathbf{Cat}$ be the category of categories.
Let $\mathbf 1$ be the category one.
Then $\mathbf 1$ is a terminal object of $\mathbf{Cat}$.

Proof:
Let $\mathbf C$ be an object of $\mathbf{Cat}$, i.e. a small category.
From Singleton is Terminal Object of Category of Sets, there exist unique mappings:
:$F_0: \mathbf C_0 \to \mathbf 1_0 = \left\{{*}\right\}$
:$F_1: \mathbf C_1 \to \mathbf 1_1 = \left\{{\operatorname{id}_*}\right\}$
since the latter sets are singletons.
It remains to verify that $F: \mathbf C \to \mathbf 1$ so defined, in fact is a functor.
Trivially, $F$ preserves identity morphisms.
That $F$ has the morphism property follows from:
:$\operatorname{id}_* \circ \operatorname{id}_* = \operatorname{id}_*$
Hence $F: \mathbf C \to \mathbf 1$ constitutes a functor.
The result follows by definition of terminal object.
{{qed}}
Theorem: Empty Mapping is Mapping

Let $T$ be a set.
Let $e: \O \to T$ be the empty mapping.
Then $e$ is indeed a mapping.

Proof:
Let $e: \O \to T$ be the empty mapping.
Vacuously:
:$\forall x \in \O: \exists y \in T: \tuple {x, y} \in e$
thus showing that $e$ is left-total.
Also vacuously:
:$\forall x \in \O: \forall y_1, y_2 \in T: \tuple {x, y_1} \in e \land \tuple {x, y_2} \in e \implies y_1 = y_2$
thus showing that $e$ is many-to-one.
Hence the result, from the definition of a mapping.
{{qed}}
Theorem: Empty Mapping is Unique

For each set $T$ there exists exactly one empty mapping $e: \O \to T$ whose domain is the empty set.

Proof:
By definition a mapping from $\O$ to $T$ is a subset of the cartesian product $\O \times T$:
:$e: \O \to T \subseteq \O \times T$
From Empty Mapping is Mapping, we have that the empty mapping from $\O$ to $T$ exists.
From Cartesian Product is Empty iff Factor is Empty it follows that the empty mapping equals the empty set:
:$\O \times T = \O$
The result follows by Empty Set is Unique.
{{qed}}
Theorem: Null Relation is Mapping iff Domain is Empty Set

Let $S$ and $T$ be sets.
The null relation $\RR = \O \subseteq S \times T$ is a mapping {{iff}} $S = \O$.

Proof:
=== Sufficient Condition ===
Let $S = \O$.
Then the null relation $\RR = \O \subseteq S \times T$ is a mapping from Empty Mapping is Mapping.
{{qed|lemma}}
Theorem: Orbit of Element of Group Acting on Itself is Group

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $*$ be the group action of $\struct {G, \circ}$ on itself by the rule:
:$\forall g, h \in G: g * h = g \circ h$
Then the orbit of an element $x \in G$ is given by:
:$\Orb x = G$

Proof:
Let $y \in G$.
Then:
{{begin-eqn}}
{{eqn | q = \exists g \in G
      | l = y
      | r = g \circ x
      | c = Group has Latin Square Property
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = \Orb x
      | c = {{Defof|Orbit (Group Theory)|Orbit}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Orbit of Element under Conjugacy Action is Conjugacy Class

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $*$ be the conjugacy group action on $G$:
: $\forall g, h \in G: g * h = g \circ h \circ g^{-1}$
Let $x \in G$.
Then the orbit of $x$ under this group action is:
:$\Orb x = \conjclass x$
where $\conjclass x$ is the conjugacy class of $x$.

Proof:
Follows from the definition of the conjugacy class.
{{explain|Needs expansion.}}
{{qed}}
Theorem: Axiom of Foundation (Strong Form)

Let $B$ be a class.
Suppose $B$ is non-empty.
Then $B$ has a strictly minimal element under $\in$.

Proof:
{{NotZFC}}
By Epsilon Relation is Strictly Well-Founded, $\Epsilon$, the epsilon relation, is a strictly well-founded relation on $B$.
By Epsilon Relation is Proper, $\struct {\mathbb U, \Epsilon}$ is a proper relational structure, where $\mathbb U$ is the universal class.
By Well-Founded Proper Relational Structure Determines Minimal Elements, $B$ has a strictly minimal element under $\Epsilon$.
{{qed}}
Theorem: Axiom of Foundation (Strong Form)

Let $B$ be a class.
Suppose $B$ is non-empty.
Then $B$ has a strictly minimal element under $\in$.

Proof:
{{NotZFC}}
Let $x \in B$.
Let $x'$ be the transitive closure of $x$.
Let $L = x' \cap B$.
Then $x \in L$, so $L$ is not empty.
Since $x'$ is a set, so is $L$, by the axiom of subset.
Thus by the Axiom of Foundation, $L$ has an $\in$-minimal element $m$.
By the definition of intersection, $m \in B$.
{{AimForCont}} that there is an element $b \in B$ such that $b \in m$.
Then since $m \in x'$ and $x'$ is transitive, $b \in x'$.
Thus $b \in L$, contradicting the minimality of $m$.
So $m$ is an $\in$-minimal element of $B$.
{{qed}}
Theorem: Trivial Group is Initial Object

Let $\mathbf{Grp}$ be the category of groups.
Let $1 = \set e$ be the trivial group.
Then $1$ is an initial object of $\mathbf{Grp}$.

Proof:
Let $\struct {G, \circ}$ be a group with identity $e_G$.
By Group Homomorphism Preserves Identity, any hypothetical group homomorphism $\phi: 1 \to G$ must satisfy:
:$\map \phi e = e_G$
Let us define the mapping $\phi$ in this way.
By Equality of Mappings, only one such mapping $1 \to G$ can exist, establishing uniqueness.
Now to verify that $\phi$ is actually a group homomorphism.
Since $1$ has only the element $e$, this is verified by:
{{begin-eqn}}
{{eqn | l = \map \phi e \circ \map \phi e
      | r = e_G \circ e_G
      | c = Definition of $\phi$
}}
{{eqn | r = e_G
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = \map \phi e
}}
{{eqn | r = \map \phi {e * e}
}}
{{end-eqn}}
where we used $*$ to denote the group operation on $1$.
Thus $\phi$ is a group homomorphism.
We have thus established that there is a unique morphism $1 \to G$ in $\mathbf{Grp}$ for all $G$.
That is, $1$ is an initial object in $\mathbf{Grp}$.
{{qed}}
Theorem: Trivial Group is Terminal Object of Category of Groups

Let $\mathbf {Grp}$ be the category of groups.
Let $\set e$ be the trivial group.
Then $\set e$ is a terminal object of $\mathbf {Grp}$.

Proof:
Let $\struct {G, \circ}$ be any group.
By Singleton is Terminal Object of Category of Sets, there is precisely one mapping:
:$!: G \to \set e$
defined by:
:$\forall g \in G: ! (g) = e$
By definition, any group homomorphism is also a mapping.
Hence, there is at most one morphism $\struct {G, \circ} \to \set e$ in $\mathbf {Grp}$.
Now to verify that the mapping $!$ is a group homomorphism.
For any $g, h \in G$, we have (using $*$ for the group operation on $\set e$):
{{begin-eqn}}
{{eqn | l = ! (g) * ! (h)
      | r = e * e
      | c = Definition of $!$
}}
{{eqn | r = e
      | c = Definition of $*$
}}
{{eqn | r = ! \paren {g \circ h}
      | c = Definition of $!$
}}
{{end-eqn}}
That is, $!$ is a group homomorphism.
Thus for all groups $\struct {G, \circ}$, there is a unique group homomorphism $!: G \to \set e$.
That is, $\set e$ is a terminal object of $\mathbf {Grp}$.
{{qed}}
Theorem: Orbit of Subgroup under Coset Action is Coset Space

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $\powerset G$ be the power set of $G$.
Let $H \in \powerset G$ be a subgroup of $G$.
Let $*$ be the group action on $H$ defined as:
:$\forall g \in G: g * H = g \circ H$
where $g \circ H$ is the (left) coset of $g$ by $H$.
Then the orbit of $H$ in $\powerset G$ is the (left) coset space of $H$:
:$\Orb H = G / H^l$

Proof:
From the definition of orbit:
:$\Orb H = \set {y \in G: \exists g \in G: y = g * H}$
By the definition of $*$:
:$\Orb H = \set {y \in G: \exists g \in G: y = g \circ H}$
The result follows from the definition of (left) coset space.
{{qed}}
Theorem: Orbit of Conjugacy Action on Subgroup is Set of Conjugate Subgroups

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $X$ be the set of all subgroups of $G$.
Let $*$ be the conjugacy action on $H$ defined as:
: $\forall g \in G, H \in X: g * H = g \circ H \circ g^{-1}$
Then the orbit $\Orb H$ of $H$ in $\powerset G$ is the set of subgroups of $G$ conjugate to $H$.

Proof:
We have that:
:$\Orb H = \set {g \circ H \circ g^{-1}: g \in G}$
from the definition.
The result follows by definition of conjugate subgroup.
{{Qed}}
Theorem: Closure for Finite Collection of Relations and Operations

Let $\RR_1, \RR_2, \ldots \RR_n$ be relations.
Let $\SS_1, \SS_2, \ldots \SS_m$ be operations.
Let $T$ be a small class.
Let the image of $\RR_i$ over any small class $x$ be small classes for $1 \le i \le n$.
Let the image of $\SS_i$ over any Cartesian product $x \times x$ be small classes for $1 \le i \le m$.
Then there exists a small class $X$ such that:
:$(1): \quad$ $T \subseteq X$
:$(2): \quad$ Each $\RR_i$ is closed {{WRT}} $X$.  Each $\SS_i$ is closed {{WRT}} $X \times X$.
:$(3): \quad$ $X$ is the smallest small class satisfying conditions $(1)$ and $(2)$ above.
If $Y$ satisfies conditions $(1)$ and $(2)$, then $X \subseteq Y$.

Proof:
Let $R \sqbrk x$ denote the image of $x$ under $R$.
Set:
:$\ds \map G x = x \cup \bigcup_{i \mathop = 1}^n \RR_i \sqbrk x \cup \bigcup_{i \mathop = 1}^m \SS_i \sqbrk x$
Using the Principle of Recursive Definition, construct the function $F$ as follows:
:$\map F 0 = T$
:$\map F {n + 1} = \map G {\map F n}$
Define $X$ as follows:
:$\ds X = \bigcup_{n \mathop \in \omega} \map F n$
Theorem: Von Neumann Hierarchy is Supertransitive

Let $V$ denote the Von Neumann Hierarchy.
Let $x$ be an ordinal.
Then $\map V x$ is supertransitive.

Proof:
{{NotZFC}}
The proof shall proceed by Transfinite Induction on $x$.
Theorem: Von Neumann Hierarchy Comparison

Let $x$ and $y$ be ordinals such that $x < y$.
Then:
:$\map V x \in \map V y$
:$\map V x \subset \map V y$
{{explain|$\map V x$ etc.}}

Proof:
{{NotZFC}}
The proof shall proceed by Transfinite Induction on $y$.