avewright/proofwiki-math huggingface dataset:
Theorem: Kleene Closure is Monoid

Let $S$ be a set, and let $S^*$ be its Kleene closure.
Let $*$ denote concatenation of ordered tuples.
Then $\struct {S^*, *}$ is a monoid.

Proof:
First, to prove that $\struct {S^*, *}$ is a semigroup.
That is, to prove $*$ is associative.
Let $s, s', s'' \in S^*$ be sequences of lengths $n, n', n''$, respectively.
Then:
{{begin-eqn}}
{{eqn | l = \map {s * \paren {s' * s''} } i
      | r = \begin {cases} \map s i & \text {if } 1 \le i \le n \\ \map {s' * s''} {i - n} & \text {if } n < i \le n + n' + n'' \end {cases}
}}
{{eqn | r = \begin {cases} \map s i & \text {if } 1 \le i \le n \\ \map {s'} {i - n} & \text {if } n < i \le n + n' \\ \map {s''} {i - n - n'} & \text {if } n + n' < i \le n + n' + n'' \end {cases}
}}
{{eqn | l = \map {\paren {s * s'} * s''} i
      | r = \begin {cases} \map {s * s'} i & \text {if } 1 \le i \le n + n' \\ \map {s''} {i - n - n'} & \text {if } n + n' < i \le n + n' + n'' \end {cases}
}}
{{eqn | r = \begin {cases} \map s i & \text {if } 1 \le i \le n \\ \map {s'} {i - n} & \text {if } n < i \le n + n' \\ \map {s''} {i - n - n'} & \text {if } n + n' < i \le n + n' + n'' \end {cases}
}}
{{end-eqn}}
Hence, by Equality of Mappings:
:$s * \paren {s' * s''} = \paren {s * s'} * s''$
that is, $*$ is associative.
Now, to prove $\struct {S^*, *}$ has an identity $e$.
It follows immediately from the length of a concatenation that $e$ must have length $0$.
That is, the only choice for $e$ is the empty sequence.
Now, for any $s \in S^*$:
:$\map {e * s} i = \begin {cases} \map e i & \text {if } 1 \le i \le 0 \\ \map s i & \text {if } 0 < i < 0 + n \end {cases}$
from which we see that $e * s = s$.
Also:
:$\map {s * e} i = \begin {cases} \map s i & \text {if } 1 \le i \le n \\ \map e i & \text {if } n < i < n + 0 \end {cases}$
which shows $s * e = s$.
So indeed the empty sequence is an identity element of $\struct {S^*, *}$.
Hence $\struct {S^*, *}$ is a monoid.
{{qed}}
Theorem: Kleene Closure is Free Monoid

Let $S$ be a set.
Let $S^*$ be its Kleene closure, and let $i: S \to S^*$ be the insertion of generators.
Then $\struct {S^*, i}$ is a free monoid over $S$.

Proof:
By Kleene Closure is Monoid, $S^*$ is a monoid.
It remains to verify the universal mapping property:{{Property|Free Monoid UMP}}
Theorem: Free Monoid is Unique

Let $S$ be a set.
Let $\struct {M, i}$ and $\struct {N, j}$ be free monoids over $S$.
Then there is a unique monoid isomorphism $f: M \to N$ such that:
:$\size f \circ i = j$
:$\size {f^{-1} } \circ j = i$
where $\size {\, \cdot \,}$ denotes the underlying set functor on $\mathbf{Mon}$.

Proof:
By the (categorial) definition of free monoid, we have the following commutative diagram:
$\quad\quad \begin{xy}
<-4em,4em>*{\mathbf{Mon} :},
<-4em,1em>*{\mathbf{Set} :},
<0em,4em>*+{N} = "N",
<4em,4em>*+{M} = "M",
<8em,4em>*+{N} = "N2",
"N";"M" **@{.} ?>*@{>} ?*!/_1em/{\bar i},
"M";"N2" **@{.} ?>*@{>} ?*!/_1em/{\bar j},
<0em,1em>*+{\left\vert{N}\right\vert} = "NN",
<4em,1em>*+{\left\vert{M}\right\vert} = "MM",
<8em,1em>*+{\left\vert{N}\right\vert} = "NN2",
<4em,-3em>*+{S} = "S",
"NN";"MM" **@{-} ?>*@{>} ?*!/_1em/{\left\vert{\bar i}\right\vert},
"MM";"NN2" **@{-} ?>*@{>} ?*!/_1em/{\left\vert{\bar j}\right\vert},
"S";"NN" **@{-} ?>*@{>} ?*!/_1em/{j},
"S";"MM" **@{-} ?>*@{>} ?<>(.7)*!/_.6em/{i},
"S";"NN2" **@{-} ?>*@{>} ?*!/^1em/{j},
\end{xy}$
The outer rim of these diagrams also needs to satisfy the universal property.
Since obviously $\operatorname{id}_N$ fits in place of $\bar j \circ \bar i$, we conclude these are equal.
Exchanging the rôles of $\struct {M, i}$ and $\struct {N, j}$ proves that $\bar i \circ \bar j = \operatorname{id}_M$ as well.
Hence $\bar i$ is the sought monoid isomorphism.
Its uniqueness follows from the universal property of the free monoid.
{{qed}}
Theorem: Ordinal Power of Power

Let $x$, $y$, and $z$ be ordinals.
Then:
:$\paren {x^y}^z = x^{y \mathop \times z}$

Proof:
The proof shall proceed by Transfinite Induction on $z$.
Theorem: Upper Bound of Ordinal Sum

Let $x$ and $y$ be ordinals.
Suppose $x > 1$.
Let $\sequence {a_n}$ be a finite sequence of ordinals such that:
:$a_n < x$ for all $n$
Let $\sequence {b_n}$ be a strictly decreasing finite sequence of ordinals such that:
:$b_n < y$ for all $n$
Then:
:$\ds \sum_{i \mathop = 1}^n x^{b_i} a_i < x^y$

Proof:
The proof shall proceed by finite induction on $n$:
For all $n \in \N_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds \sum_{i \mathop = 1}^n x^{b_i} a_i < x^y$
Theorem: General Associative Law for Ordinal Sum

Let $x$ be a finite ordinal.
Let $\sequence {a_i}$ be a sequence of ordinals.
Then:
:$\ds \sum_{i \mathop = 1}^{x + 1} a_i = a_1 + \sum_{i \mathop = 1}^x a_{i + 1}$

Proof:
The proof shall proceed by induction on $x$.
=== Basis for the Induction ===
If $x = 0$, then:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 1}^{0 + 1} a_i
      | r = \sum_{i \mathop = 1}^0 a_i + a_1
      | c = {{Defof|Ordinal Sum}}
}}
{{eqn | r = a_1
      | c = Ordinal Addition by Zero
}}
{{eqn | r = a_1 + \sum_{i \mathop = 1}^0 a_i
      | c = Ordinal Addition by Zero
}}
{{end-eqn}}
This proves the basis for the induction.
{{qed|lemma}}
=== Induction Step ===
Suppose:
:$\ds \sum_{i \mathop = 1}^{x + 1} a_i = a_1 + \sum_{i \mathop = 1}^x a_{i + 1}$
Then:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 1}^{x + 2} a_i
      | r = \sum_{i \mathop = 1}^{x + 1} a_i + a_{i + 2}
      | c = {{Defof|Ordinal Sum}}
}}
{{eqn | r = \paren {a_1 + \sum_{i \mathop = 1}^x a_{i + 1} } + a_{i + 2}
      | c = Inductive Hypothesis
}}
{{eqn | r = a_1 + \paren {\sum_{i \mathop = 1}^x a_{i + 1} + a_{i + 2} }
      | c = Ordinal Addition is Associative
}}
{{eqn | r = a_1 + \sum_{i \mathop = 1}^{x + 1} a_{i + 1}
      | c = {{Defof|Ordinal Sum}}
}}
{{end-eqn}}
This proves the induction step.
{{qed}}
Theorem: General Associative Law for Ordinal Sum

Let $x$ be a finite ordinal.
Let $\sequence {a_i}$ be a sequence of ordinals.
Then:
:$\ds \sum_{i \mathop = 1}^{x + 1} a_i = a_1 + \sum_{i \mathop = 1}^x a_{i + 1}$

Proof:
From Ordinal Addition is Associative we have that:
:$\forall a, b, c \in \On: a + \paren {b + c} = \paren {a + b} + c$
The result follows directly from the General Associativity Theorem.
{{qed}}
Theorem: Basis Representation Theorem for Ordinals

Let $x$ and $y$ be ordinals.
Let $x > 1$ and $y > 0$.
Then there exist unique finite sequences of ordinals:
:$\sequence {a_i}, \sequence {b_i}$
both of unique length $n$ such that:
:$(1): \quad \sequence {a_i}$ is a strictly decreasing sequence for $1 \le i \le n$
:$(2): \quad 0 < b_i < x$ for all $1 \le i \le n$
:$(3): \quad \ds y = \sum_{i \mathop = 1}^n x^{a_i} b_i$

Proof:
The proof shall proceed by Transfinite Induction (Strong Induction) on $y$.
The inductive hypothesis states that for all $v < y$, there exist unique finite sequences of ordinals:
:$\sequence {c_i}, \sequence {d_i}$
both of unique length $n$ such that:
:$(1): \quad \sequence {c_i}$ is strictly decreasing sequence for $1 \le i \le n$
:$(2): \quad 0 < d_i < x$ for all $1 \le i \le n$.
:$(3): \quad \ds v = \sum_{i \mathop = 1}^n x^{c_i} d_i$
Since $x > 1$, it follows by Unique Ordinal Exponentiation Inequality that:
:$x^z \le y < x^{z + 1}$
for some unique $z$.
By the Division Theorem for Ordinals:
:$y = x^z w + v$ and $v < x^z$
for some unique $z$, $w$, and $v$.
Thus:
{{begin-eqn}}
{{eqn | l = v
      | o = <
      | r = x^z
      | c = Division Theorem for Ordinals, as shown above
}}
{{eqn | o = \le
      | r = y
      | c = Unique Ordinal Exponentiation Inequality, as shown above
}}
{{end-eqn}}
So $v < y$.
If $v = 0$, then the statement is proven.
If $v \ne 0$, then we may apply the inductive hypothesis.
By the inductive hypothesis:
:$\ds v = \sum_{i \mathop = 1}^n x^{c_i} d_i$
Therefore:
:$\ds y = x^z w + \sum_{i \mathop = 1}^n x^{c_i} d_i$
{{qed|lemma}}
Set:
:$a_1 = z$
:$a_{i + 1} = c_i$ for $1 \le i \le n$
:$b_1 = w$
:$b_{i + 1} = d_i$ for $1 \le i \le n$
Since $w \ne 0$ and $d_i \ne 0$, it follows that $b_i \ne 0$ for all $1 \le i \le n+1$.
{{qed|lemma}}
Moreover, since $z > c_1$ and $\sequence {c_i}$ is strictly decreasing, it follows that also $\sequence {a_i}$ is strictly decreasing.
{{qed|lemma}}
The equation for the first lemma can be rewritten:
:$\ds y = x^{a_1} b_1 + \sum_{i \mathop = 1}^n x^{a_{i + 1} } b_{i + 1}$
By General Associative Law for Ordinal Sum, it follows that:
:$\ds y = \sum_{i \mathop = 1}^{n + 1} x^{a_i} b_i$
Thus, existence is proven.
{{qed|lemma}}
Furthermore, since $z$ and $\sequence {c_i}$ are unique, and $w$ and $\sequence {a_i}$ are unique, then $\sequence {a_i}$ and $\sequence {b_i}$ are unique.
{{qed}}
Theorem: Ordinal Multiplication via Cantor Normal Form/Infinite Exponent

Let $x$ and $y$ be ordinals.
Let $x > 1$.
Let $y \ge \omega$ where $\omega$ denotes the minimally inductive set.
Let $\sequence {a_i}$ be a sequence of ordinals that is strictly decreasing on $1 \le i \le n$.
Let $\sequence {b_i}$ be a sequence of ordinals such that $0 < b_i < x$ for all $1 \le i \le n$.
Then:
:$\ds \sum_{i \mathop = 1}^n \paren {x^{a_i} b_i} \times x^y = x^{a_1 \mathop + y}$

Proof:
It follows that:
{{begin-eqn}}
{{eqn | l = x^{a_1}
      | o = \le
      | r = \sum_{i \mathop = 1}^n \paren {x^{a_i} b_i}
      | c = Ordinal is Less than Sum
}}
{{eqn | o = <
      | r = x^{a_1 + 1}
      | c = Upper Bound of Ordinal Sum
}}
{{end-eqn}}
By multiplying the inequalities by $x^y$ on the left:
{{begin-eqn}}
{{eqn | l = x^{a_1} \times x^y
      | o = \le
      | r = \sum_{i \mathop = 1}^n \paren {x^{a_i} b_i} \times x^y
      | c = Subset is Right Compatible with Ordinal Multiplication
}}
{{eqn | o = \le
      | r = x^{a_1 \mathop + 1} \times x^y
      | c = 
}}
{{end-eqn}}
Solving for both sides of the inequality:
{{begin-eqn}}
{{eqn | l = x^{a_1} \times x^y
      | r = x^{a_1 \mathop + y}
      | c = Ordinal Sum of Powers
}}
{{eqn | l = x^{a_1 \mathop + 1} \times x^y
      | r = x^{\paren {a_1 \mathop + 1} \mathop + y}
      | c = Ordinal Sum of Powers
}}
{{eqn | r = x^{a_1 \mathop + \paren {1 \mathop + y} }
      | c = Ordinal Addition is Associative
}}
{{eqn | r = x^{a_1 \mathop + y}
      | c = Finite Ordinal Plus Transfinite Ordinal
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = x^{a_1 \mathop + y}
      | o = \le
      | r = \sum_{i \mathop = 1}^n \paren {x^{a_i} b_i} \times x^y
      | c = Substitutivity of Class Equality
}}
{{eqn | o = \le
      | r = x^{a_1 \mathop + y}
      | c = Substitutivity of Class Equality
}}
{{eqn | ll= \leadsto
      | l = \sum_{i \mathop = 1}^n \paren {x^{a_i} b_i} \times x^y
      | r = x^{a_1 \mathop + y}
      | c = {{Defof|Set Equality|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Ordinal Multiplication via Cantor Normal Form/Limit Base

Let $x$ and $y$ be ordinals.
Let $x$ be a limit ordinal.
Let $y > 0$.
Let $\sequence {a_i}$ be a sequence of ordinals that is strictly decreasing on $1 \le i \le n$.
Let $\sequence {b_i}$ be a sequence of finite ordinals.
Then:
:$\ds \sum_{i \mathop = 1}^n \paren {x^{a_i} b_i} \times x^y = x^{a_1 \mathop + y}$

Proof:
The proof shall proceed by finite induction on $n$:
For all $n \in \N_{\le 0}$, let $\map P n$ be the proposition:
:$\ds \sum_{i \mathop = 1}^n \paren {x^{a_i} b_i} \times x^y = x^{a_1 \mathop + y}$
Since $x$ is a limit ordinal, it follows that $x^y$ is a limit ordinal by Limit Ordinals Closed under Ordinal Exponentiation.
Theorem: Ordinal Exponentiation of Terms

Let $x, y, z$ be ordinals.
Let $n$ be a finite ordinal.
Let $x$ be a limit ordinal.
Let $y, z, n$ all be greater than $0$.
Then:
:$\paren {x^y \times n}^z = x^{y \mathop \times z} \times n$ if $z$ is not a limit ordinal
:$\paren {x^y \times n}^z = x^{y \mathop \times z}$ if $z$ is a limit ordinal.

Proof:
The proof shall proceed by Transfinite Induction on $z$.
Theorem: Unique Sequence of Consecutive Odd Numbers which are Prime

Let $n \in \Z$ be an integer such that $n > 3$.
Then $n$, $n + 2$, $n + 4$ cannot all be prime.
That is, the only set of $3$ consecutive odd numbers all of which are prime is $\set {3, 5, 7}$.

Proof:
Let $n \in \Z_{>0}$.
For $n \le 3$ the cases can be examined in turn.
:$\set {1, 3, 5}$ are not all prime, as $1$ is not classified as prime.
:$\set {2, 4, 6}$ are not all prime, as $4$ and $6$ both have $2$ as a divisor.
:$\set {3, 5, 7}$ is the set of three consecutive odd primes which is asserted as being the unique set of odd numbers all of which are prime.
Suppose $n > 3$.
If $n$ is even then it has $2$ as a divisor, and so the set $\set {n, n + 2, n + 4}$ contains only composite numbers.
So, suppose now that $n$ is an odd integer such that $n > 3$.
Any integer $n$ can be represented as either:
{{begin-eqn}}
{{eqn | l = n
      | r = 3 k
}}
{{eqn | l = n
      | r = 3 k + 1
}}
{{eqn | l = n
      | r = 3 k + 2
}}
{{end-eqn}}
If $n = 3 k$, then $n$ is not prime because $3 \divides 3 k$.
If $n = 3 k + 1$, then $n + 2$ is not prime because $3 \divides 3 k + 3$.
If $n = 3 k + 2$, then $n + 4$ is not prime because $3 \divides 3 k + 6$.
Therefore no such $n$ exists for which $n$, $n + 2$, and $n + 4$ are all prime.
{{Qed}}
Theorem: Inequality for Ordinal Exponentiation

Let $x$ and $y$ be ordinals.
Let $x$ be a limit ordinal and let $y > 0$.
Let $\sequence {a_i}$ be a sequence of ordinals that is strictly decreasing on $1 \le i \le n$.
Let $\sequence {b_i}$ be a sequence of natural numbers.
Then:
:$\ds \paren {\sum_{i \mathop = 1}^n x^{a_i} \times b_i}^y \le x^{a_1 \mathop \times y} \times \paren {b_1 + 1}$

Proof:
By Upper Bound of Ordinal Sum:
:$\ds \sum_{i \mathop = 1}^n \paren {x^{a_i} \times b_i} \le x^{a_1} \times \paren {b_1 + 1}$
So:
{{begin-eqn}}
{{eqn | l = \paren {\sum_{i \mathop = 1}^n x^{a_i} \times b_i}^y
      | o = \le
      | r = \paren {x^{a_1} \times \paren {b_1 + 1} }^y
      | c = Subset is Right Compatible with Ordinal Exponentiation
}}
{{eqn | r = \paren {x^{a_1} }^y \times \paren {b_1 + 1}
      | c = Ordinal Multiplication via Cantor Normal Form/Limit Base
}}
{{eqn | r = x^{a_1 \mathop \times y} \times \paren {b_1 + 1}
      | c = Ordinal Power of Power
}}
{{end-eqn}}
{{qed}}
{{explain|I can't see how $\paren {x^{a_1} \times \paren {b_1 + 1} }^y {{=}} \paren {x^{a_1} }^y \times \paren {b_1 + 1}$, from the link suggested or otherwise. I would have expected the RHS to be $\paren {x^{a_1} }^y \times \paren {b_1 + 1}^y$, unless $\paren {b_1 + 1} {{=}} \paren {b_1 + 1}^y$, which I can't get my head round without a specific link to it somewhere.}}
Theorem: Ordinal Exponentiation via Cantor Normal Form/Limit Exponents

Let $x$ and $y$ be ordinals.
Let $x$ and $y$ be limit ordinals.
Let $\sequence {a_i}$ be a sequence of ordinals that is strictly decreasing on $1 \le i \le n$.
Let $\sequence {b_i}$ be a sequence of natural numbers.
Then:
:$\ds \paren {\sum_{i \mathop = 1}^n x^{a_i} \times b_i}^y = x^{a_1 \mathop \times y}$

Proof:
By Upper Bound of Ordinal Sum:
:$\ds \sum_{i \mathop = 1}^n \paren {x^{a_i} \times b_i} \le x^{a_1} \times \paren {b_1 + 1}$
Furthermore:
:$\ds x^{a_1} \le \sum_{i \mathop = 1}^n \paren {x^{a_i} \times b_i}$
It follows that:
{{begin-eqn}}
{{eqn | l = \paren {x^{a_1} }^y
      | o = \le
      | r = \paren {\sum_{i \mathop = 1}^n x^{a_i} \times b_i}^y
      | c = Subset is Right Compatible with Ordinal Exponentiation
}}
{{eqn | o = \le
      | r = \paren {x^{a_1} \times \paren {b_1 + 1} }^y
      | c = Subset is Right Compatible with Ordinal Exponentiation
}}
{{eqn | r = x^{a_1 \times y}
      | c = Ordinal Exponentiation of Terms
}}
{{end-eqn}}
It follows that:
{{begin-eqn}}
{{eqn | l = x^{a_1 \mathop + y}
      | o = \le
      | r = \paren {\sum_{i \mathop = 1}^n x^{a_i} b_i}^y
      | c = Ordinal Power of Power
}}
{{eqn | o = \le
      | r = x^{a_1 \mathop + y}
      | c = proven above
}}
{{eqn | ll= \leadsto
      | l = \paren {\sum_{i \mathop = 1}^n x^{a_i} b_i}^y
      | r = x^{a_1 \mathop + y}
      | c = {{Defof|Set Equality|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Ordinal Exponentiation via Cantor Normal Form/Corollary

Let $x$ and $y$ be ordinals.
Let $x$ be a limit ordinal and let $y > 0$.
Let $\sequence {a_i}$ be a sequence of ordinals that is strictly decreasing on $1 \le i \le n$.
Let $\sequence {b_i}$ be a sequence of natural numbers.
Then:
:$\ds \paren {\sum_{i \mathop = 1}^n x^{a_i} \times b_i}^{x^y} = x^{a_1 \mathop \times x^y}$
{{explain|what "Cantor normal form" is in the exposition of the above.}}

Proof:
By the hypothesis, $x^y$ is a limit ordinal by Limit Ordinals Closed under Ordinal Exponentiation.
The result follows from Ordinal Exponentiation via Cantor Normal Form/Limit Exponents.
{{qed}}
Theorem: Inverse Relation Functor is Contravariant Functor

Let $\mathbf{Rel}$ be the category of relations.
Let $C: \mathbf{Rel} \to \mathbf{Rel}$ be the inverse relation functor.
Then $C$ is a contravariant functor.

Proof:
For any set $X$. we have:
{{begin-eqn}}
{{eqn|l = C \operatorname{id}_X
     |r = \operatorname{id}_X^{-1}
     |c = {{Defof|Inverse Relation Functor}}
}}
{{eqn|r = \set {\tuple {x, x}: \tuple {x, x} \in \operatorname{id}_X}
     |c = {{Defof|Inverse Relation}}
}}
{{eqn|r = \operatorname{id}_X
}}
{{end-eqn}}
For any two relations $\RR \subseteq X \times Y$ and $\SS \subseteq Y \times Z$, we have:
{{begin-eqn}}
{{eqn|l = C \paren {\SS \circ \RR}
     |r = \paren {\SS \circ \RR}^{-1}
     |c = {{Defof|Inverse Relation Functor}}
}}
{{eqn|r = \RR^{-1} \circ \SS^{-1}
     |c = Inverse of Composite Relation
}}
{{eqn|r = C \RR \circ C \SS
     |c = {{Defof|Inverse Relation Functor}}
}}
{{end-eqn}}
Hence $C$ is shown to be a contravariant functor.
{{qed}}
Theorem: Injection iff Monomorphism in Category of Sets

Let $\mathbf{Set}$ be the category of sets.
Let $f: X \to Y$ be a morphism in $\mathbf{Set}$, that is, a mapping.
Then $f$ is an injection {{iff}} it is a monomorphism.

Proof:
=== Necessary Condition ===
Suppose that $f$ is injective.
Suppose further that we have mappings $g, h: Z \to X$ such that $g \ne h$.
Then necessarily there exists some $z \in Z$ such that $\map g z \ne \map h z$ by Equality of Mappings.
As $f$ is injective, it follows that:
:$\map f {\map g z} \ne \map f {\map h z}$
which, again by Equality of Mappings, means that:
:$f \circ g \ne f \circ h$
Hence $f$ is monic, by the Rule of Transposition.
{{qed|lemma}}
Theorem: Transitive Closure of Set Always Exists

Let $S$ be a set.
Let $G$ be a mapping such that $\map G x = x \cup \bigcup x$.
{{explain|Domain and range of $G$ needed}}
Let $F$ be defined using the Principle of Recursive Definition:
:$\map F 0 = S$
:$\map F {n^+} = \map G {\map F n}$
Let $\ds T = \bigcup_{n \mathop \in \omega} \map F n$.
Then:
:$T$ is a set and is transitive
:$S \subseteq T$
:If $R$ is transitive and $S \subseteq R$, then $T \subseteq R$.
That is, given any set $S$, there is an explicit construction for its transitive closure.

Proof:
$\omega$ is a set by the {{Axiom-link|Infinity}}.
Thus by the {{Axiom-link|Replacement}}, the image of $\omega$ under $F$ is also a set.
Since $T$ is the union of $\map F \omega$, it is thus a set by the {{Axiom-link|Unions|Set Theory}}.
Furthermore:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = T
      | c = Assumption
}}
{{eqn | ll= \leadsto
      | q = \exists n
      | l = x
      | o = \in
      | r = \map F n
      | c = {{Defof|Union of Family}}
}}
{{eqn | ll= \leadsto
      | q = \exists n
      | l = x
      | o = \subseteq
      | r = \bigcup \map F n
      | c = Set is Subset of Union of Family
}}
{{eqn | l = y
      | o = \in
      | r = x
      | c = Assumption
}}
{{eqn | ll= \leadsto
      | q = \exists n
      | l = y
      | o = \in
      | r = \bigcup \map F n
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists n
      | l = y
      | o = \in
      | r = \map F {n + 1}
      | c = Definition of $F$
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = T
      | c = Definition of $T$
}}
{{end-eqn}}
{{explain|domain of $n$}}
By the above equations:
:$x \in T \land y \in x \implies y \in T$
Thus by definition $T$ is transitive.
{{qed|lemma}}
We have that:
:$S = \map F 0$
By Set is Subset of Union of Family:
:$\ds S \subseteq \bigcup_{n \mathop \in \omega} \map F n$
So $S \subseteq T$.
{{qed|lemma}}
Finally, suppose that $S \subseteq R$ and $R$ is transitive.
$T \subseteq R$ follows by finite induction:
For all $n \in \omega$, let $\map P n$ be the proposition:
:$\map F n \subseteq R$
Theorem: Morphism in Preorder Category is Monic

Let $\mathbf P$ be a preorder category.
Let $f \in \mathbf P_1$ be a morphism.
Then $f$ is monic.

Proof:
Suppose that $g, h \in \mathbf P_1$ are morphisms such that:
:$f \circ g = f \circ h$
In particular then, $g$ and $h$ have equal domain and codomain.
Since $\mathbf P$ is a preorder category, there is at most one morphism between any two objects.
Thus necessarily $g = h$, and hence $f$ is monic.
{{qed}}
Theorem: Morphism in Preorder Category is Epic

Let $\mathbf P$ be a preorder category.
Let $f \in \mathbf P_1$ be a morphism.
Then $f$ is epic.

Proof:
Suppose that $g, h \in \mathbf P_1$ are morphisms such that:
:$g \circ f = h \circ f$
In particular then, $g$ and $h$ have equal domain and codomain.
Since $\mathbf P$ is a preorder category, there is at most one morphism between any two objects.
Thus necessarily $g = h$, and hence $f$ is epic.
{{qed}}
Theorem: Surjection iff Epimorphism in Category of Sets

Let $\mathbf{Set}$ be the category of sets.
Let $f: X \to Y$ be a morphism in $\mathbf{Set}$, i.e. a mapping.
Then:
:$f$ is a surjection {{iff}} it is an epimorphism.

Proof:
=== Necessary Condition (proof 1 - contrapositive) ===
Let $f$ be surjective.
{{:Surjection iff Epimorphism in Category of Sets/Necessary Condition Proof 1}}{{qed|lemma}}
Theorem: Surjection iff Epimorphism in Category of Sets

Let $\mathbf{Set}$ be the category of sets.
Let $f: X \to Y$ be a morphism in $\mathbf{Set}$, i.e. a mapping.
Then:
:$f$ is a surjection {{iff}} it is an epimorphism.

Proof:
By definition of epimorphism:
:$f$ is an epimorphism
{{iff}}
:for all mappings $g, h: Y \to Z : g \circ f = h \circ f \implies g = h$
In the following we prove the contrapositive statement:
:for all mappings $g, h: Y \to Z : g \ne h \implies g \circ f \ne h \circ f$
Let $g, h: Y \to Z$ be mappings such that $g \ne h$.
From Equality of Mappings:
:$\exists y \in Y : \map g y \ne \map h y$
By definition of surjection:
:$(1) \quad \exists x \in X : \map f x = y$.
We have:
{{begin-eqn}}
{{eqn | l = \map {\paren{g \circ f} } x
      | r = \map g {\map f x}
      | c = {{Defof|Composite Mapping}}
}}
{{eqn | r = \map g y
      | c = By $(1)$
}}
{{eqn | o = \ne
      | r = \map h y
      | c = {{hypothesis}}
}}
{{eqn | r = \map h {\map f x}
      | c = By $(1)$
}}
{{eqn | r = \map {\paren{h \circ f} } x
      | c = {{Defof|Composite Mapping}}
}}
{{end-eqn}}
From Equality of Mappings:
:$g \circ f \ne h \circ f$.
By the Rule of Transposition:
:$f$ is epic.
Theorem: Surjection iff Epimorphism in Category of Sets

Let $\mathbf{Set}$ be the category of sets.
Let $f: X \to Y$ be a morphism in $\mathbf{Set}$, i.e. a mapping.
Then:
:$f$ is a surjection {{iff}} it is an epimorphism.

Proof:
Let $g, h: Y \to Z$ be mappings such that $g \circ f = h \circ f$.
Let $y \in Y$ be an arbitrary element of $Y$.
By definition of surjection:
:$(1) \quad \exists x \in X : \map f x = y$.
We have:
{{begin-eqn}}
{{eqn | l = \map g y
      | r = \map g {\map f x}
      | c = By $(1)$
}}
{{eqn | r = \map {\paren{g \circ f} } x
      | c = {{Defof|Composite Mapping}}
}}
{{eqn | r = \map {\paren{h \circ f} } x
      | c = {{hypothesis}}
}}
{{eqn | r = \map h {\map f x}
      | c = {{Defof|Composite Mapping}}
}}
{{eqn | r = \map h y
      | c = By $(1)$
}}
{{end-eqn}}
Since $y$ was arbitrary we have:
:$\forall x \in X : \map g x = \map h x$.
From Equality of Mappings:
:$g = h$
Since $g$ and $h$ were arbitrary we have:
:$\forall g, h: Y \to Z : g \circ f = h \circ f \implies g = h$.
It follows that $f$ is epic by definition.