avewright/proofwiki-math huggingface dataset:
Theorem: Union of Ordinals is Least Upper Bound

Let $A \subset \On$.
That is, let $A$ be a class of ordinals (every member of $A$ is an ordinal).
Then $\bigcup A$, the union of $A$, is the least upper bound of $A$:
:$\ds \forall x \in A: x \le A$
:$\ds \forall y \in A: y \le x \implies \bigcup A \le x$

Proof:
First, we must show that $\ds \bigcup A$ is an upper bound.
Take any member $a \in A$.
Then by Subset of Union:
:$\ds a \subseteq \bigcup A$
By Ordering on Ordinal is Subset Relation:
:$a \le A$
By generalizing for all $a \in A$:
:$\ds \forall x \in A: x \le \bigcup A$
Similarly, suppose now that $x$ is an upper bound of $A$.
We shall denote $<$ for ordering on the ordinal numbers.
By Ordering on Ordinal is Subset Relation and Transitive Set is Proper Subset of Ordinal iff Element of Ordinal, $<$ is the same as both $\in$ and $\subsetneq$.
Then:
{{begin-eqn}}
{{eqn | l = z \in \bigcup A
      | o = \leadsto
      | r = \exists y: \paren {z \in y \land y \in A}
      | c = {{Defof|Union of Set of Sets}}
}}
{{eqn | o = \leadsto
      | r = \exists y: \paren {z \in y \land y < x}
      | c = {{hypothesis}} (as $y \in A$, $y < x$)
}}
{{eqn | o = \leadsto
      | r = z \in x
      | c = transitivity of $\in$: see Alternative Definition of Ordinal
}}
{{end-eqn}}
Thus, by definition of subset:
:$\ds \bigcup A \subseteq x$
Therefore:
:$\ds \forall y \in A: y \le x \implies \bigcup A \le x$
{{qed}}
Theorem: Ordinal is Less than Successor

Let $x$ be an ordinal.
Let $x^+$ denote the successor of $x$.
Then:
:$x \in x^+$
:$x \subset x^+$

Proof:
$x$ is an ordinal and so by definition is also a set.
:$x \in \paren {x \cup \set x} \land x \subset \paren {x \cup \set x}$
so by applying the definition of a successor set:
:$x \in x^+ \land x \subset x^+$
{{qed}}
Theorem: No Natural Number between Number and Successor

Let $\N$ be the natural numbers.
Let $n \in \N$.
Then no natural number $m$ exists strictly between $n$ and its successor $n + 1$:
:$\neg \exists m \in \N: \paren {n < m < n + 1}$
That is:
:If $n \le m \le n + 1$, then $m = n$ or $m = n + 1$.

Proof:
We use the model that $\N \cong \omega$ where $\omega$ is the minimally inductive set.
{{AimForCont}} such an ordinal $m$ exists.
Then, by Ordering on Ordinal is Subset Relation:
:$n \in m$
and from Transitive Set is Proper Subset of Ordinal iff Element of Ordinal:
:$m \in n^+$
Applying the definition of a successor set, we have:
:$n \in m \lor n = m$
But this creates a membership loop, in that:
:$m \in n \in m \lor m \in m$
By No Membership Loops, we have created a contradiction.
The result follows from Proof by Contradiction.
{{qed}}
Theorem: No Natural Number between Number and Successor

Let $\N$ be the natural numbers.
Let $n \in \N$.
Then no natural number $m$ exists strictly between $n$ and its successor $n + 1$:
:$\neg \exists m \in \N: \paren {n < m < n + 1}$
That is:
:If $n \le m \le n + 1$, then $m = n$ or $m = n + 1$.

Proof:
Let $\N$ be defined as the von Neumann construction $\omega$.
By definition of the ordering on von Neumann construction:
:$m \le n \iff m \subseteq n$
From Von Neumann Construction of Natural Numbers is Minimally Inductive, $\omega$ is minimally inductive class under the successor mapping.
The result follows from the Sandwich Principle:
:$\forall m, n \in \omega: m \subseteq n \subseteq m^+ \implies m = n \lor n = m^+$
where $m^+$ is identified as $m + 1$.
{{qed}}
Theorem: No Largest Ordinal

Let $a$ be a set of ordinals.
Then:
:$\forall x \in a: x \prec \paren {\bigcup a}^+$

Proof:
For this proof, we shall use $\prec$, $\in$, and $\subset$ interchangeably.
We are justified in doing this because of Ordering on Ordinal is Subset Relation and Transitive Set is Proper Subset of Ordinal iff Element of Ordinal.
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = a
      | c = {{Hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \subseteq
      | r = \bigcup A
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \preceq
      | r = \bigcup A
      | c = 
}}
{{eqn | o = \prec
      | r = \paren {\bigcup A}^+
      | c = Ordinal is Less than Successor
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \prec
      | r = \paren {\bigcup A}^+
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Minimally Inductive Set is Ordinal

Let $\omega$ denote the minimally inductive set.
Then $\omega$ is an ordinal.

Proof:
The minimally inductive set is a set of ordinals by definition.
From {{Corollary|Ordinals are Well-Ordered}}, it is seen that $\struct {\omega, \Epsilon \restriction_\omega}$ is a strictly well-ordered set.
It is to be shown by induction on minimally inductive set that $\forall n \in \omega: \omega_n = n$
=== Basis for the Induction ===
{{begin-eqn}}
{{eqn | l = \omega_\O
      | r = \set {x \in \omega: x \in \O}
      | c = {{Defof|Initial Segment}}
}}
{{eqn | r = \O
      | c = {{Defof|Empty Set}}
}}
{{end-eqn}}
=== Induction Hypothesis ===
Suppose that $\omega_n = n$ for some $n \in \omega$.
=== Induction Step ===
{{begin-eqn}}
{{eqn | l = \omega_{n^+}
      | r = \set {x \in \omega: x \in n^+}
}}
{{eqn | r = \set {x \in \omega: x \in n \lor x \in \set n}
      | c = {{Defof|Successor Set}}
}}
{{eqn | r = \set {x \in \omega: x \in n \lor x = n}
      | c = {{Defof|Singleton}}
}}
{{eqn | r = \set {x \in \omega: x \in n} \cup \set {x \in \omega: x = n}
      | c = {{Defof|Set Union}}
}}
{{eqn | r = \omega_n \cup \set n
}}
{{eqn | r = n \cup \set n
      | c = Induction Hypothesis
}}
{{eqn | r = n^+
      | c = {{Defof|Successor Set}}
}}
{{end-eqn}}
And so $\omega$ is an ordinal.
{{qed}}
Theorem: Minimally Inductive Set is Ordinal

Let $\omega$ denote the minimally inductive set.
Then $\omega$ is an ordinal.

Proof:
Let $K_I$ denote the set of all nonlimit ordinals.
Let $\On$ denote the set of all ordinals.
Let $a \in \omega$.
It follows that $a^+ \subseteq K_I$, so $a \in K_I$.
Thus:
:$\omega \subseteq K_I \subseteq \On$
We now must prove that $\omega$ is a transitive set, at which point it will satisfy the Alternative Definition of Ordinal.
Let $x \in y$ and $y \in \omega$.
Then:
:$y \in \On \land y^+ \subseteq K_I$
Because $y$ is an ordinal, it is transitive.
Therefore:
:$x \subseteq y$
and:
:$x^+ \subseteq y^+ \subseteq K_I$
Therefore, $x^+ \subseteq K_I$.
Applying the definition of minimally inductive set:
:$x \in \omega$
so $\omega$ is transitive.
{{qed}}
Theorem: Minimally Inductive Set is Limit Ordinal

Let $\omega$ denote the minimally inductive set.
Then $\omega$ is a limit ordinal.

Proof:
Let $K_I$ denote the class of all nonlimit ordinals.
{{AimForCont}} $\omega$ is not a limit ordinal.
Every element of $\omega$ is a nonlimit ordinal.
So, if $\omega$ is also a nonlimit ordinal, $\omega + 1 \subseteq K_I$.
By the definition of $\omega$:
:$\omega \in \omega$
which violates No Membership Loops and is thus contradictory.
It follows from Proof by Contradiction that $\omega$ is a limit ordinal.
{{Qed}}
Theorem: No Infinitely Descending Membership Chains

Let $\omega$ denote the minimally inductive set.
Let $F$ be a mapping whose domain is $\omega$.
Then:
:$\exists n \in \omega: \map F {n^+} \notin \map F n$

Proof:
Let $F$ be a mapping whose domain is $\omega$.
By the axiom of replacement, the image of $F$ is a set.
Let the image of $F$ be denoted $\map \WW F$.
Then:
{{begin-eqn}}
{{eqn | o = 
      | r = \exists x \in \map \WW F: \paren {\map \WW F \cap x} = \O
      | c = Axiom of Foundation
}}
{{eqn | o = \leadsto
      | r = \exists x: \paren {\paren {\map \WW F \cap x} = \O \land \exists n \in \omega: x = \map F n}
      | c = as $x \in \map \WW F$, $x = \map F n$ for some $n \in \omega$
}}
{{eqn | o = \leadsto
      | r = \exists n \in \omega: \paren {\map \WW F \cap \map F n} = \O
      | c = Logical manipulation eliminating $x$
}}
{{end-eqn}}
But:
:$\map F {n^+} \in \map \WW F$
So:
:$\map F {n^+} \notin \map F n$
{{qed}}
Theorem: Ordinals Isomorphic to the Same Well-Ordered Set

Let $A$ and $B$ be ordinals.
Let $\left({\prec, S}\right)$ be a strict well-ordering.
Let $\left({\in, A}\right)$ and $\left({\prec, S}\right)$ be order isomorphic.
Let $\left({\in, B}\right)$ and $\left({\prec, S}\right)$ be order isomorphic.
Then:
: $A = B$

Proof:
Let $\phi_1$ denote the mapping creating the order isomorphism between $\left({\in, A}\right)$ and $\left({\prec, S}\right)$.
Let $\phi_2$ denote the mapping creating the order isomorphism between $\left({\in, B}\right)$ and $\left({\prec, S}\right)$.
Then $\phi_2^{-1}: S \to B$ is an order isomorphism by Inverse of Order Isomorphism is Order Isomorphism.
$\phi_1 \circ \phi_2^{-1}: A \to B$ is an order isomorphism by Composite of Order Isomorphisms is Order Isomorphism.
So $\left({\in, A}\right)$ and $\left({\in, B}\right)$ are order isomorphic ordinals.
By Isomorphic Ordinals are Equal:
:$A = B$
{{qed}}
Theorem: Transfinite Recursion Theorem/Uniqueness

Let $f$ be a mapping with a domain $y$ where $y$ is an ordinal.
Let $f$ satisfy the condition that:
:$\forall x \in y: \map f x = \map G {f \restriction x}$
where $f \restriction x$ denotes the restriction of $f$ to $x$.
Let $g$ be a mapping with a domain $z$ where $z$ is an ordinal.
Let $g$ satisfy the condition that:
:$\forall x \in z: \map g x = \map G {g \restriction x}$
Let $y \subseteq z$.
Then:
:$\forall x \in y: \map f x = \map g x$

Proof:
Proof by transfinite induction:
Suppose that:
:$\forall x \in \alpha: \map f x = \map g x$
for some arbitrary ordinal $\alpha < y$.
Then $\alpha < z$.
{{explain|Find the link to the result proving this.}}
Hence:
{{begin-eqn}}
{{eqn | q = \forall x \in \alpha
      | l = \map f x
      | r = \map g x
}}
{{eqn | ll= \leadsto
      | l = f \restriction \alpha
      | r = g \restriction \alpha
      | c = Equality of Restrictions
}}
{{eqn | ll= \leadsto
      | l = \map G {f \restriction \alpha}
      | r = \map G {g \restriction \alpha}
      | c = Substitution
}}
{{eqn | ll= \leadsto
      | l = \map f \alpha
      | r = \map g \alpha
      | c = {{Hypothesis}}
}}
{{end-eqn}}
So applying induction:
:$\forall \alpha < y: \map f \alpha = \map g \alpha$
{{qed}}
Theorem: Transfinite Induction/Schema 1

Let $\map P x$ be a property 
Suppose that:
:If $\map P x$ holds for all ordinals $x$ less than $y$, then $\map P y$ also holds.
Then $\map P x$ holds for all ordinals $x$.

Proof:
It should be noted that for any two ordinals, $x < y \iff x \in y$.
Let $\map P x$ be a property that satisfies the above conditions.
{{AimForCont}} $y$ is an ordinal such that $\neg \map P y$.
By the Rule of Transposition, it follows that if $y$ is an ordinal such that $\neg \map P y$, then there exists an ordinal $x < y \iff x \in y$ such that $\neg \map P x$.
Let $\alpha$ be the smallest ordinal in $y$ such that $\neg \map P \alpha$.
We can choose such an element because an ordinal is strictly well-ordered by definition.
Since $\neg \map P \alpha$, let $\beta$ be the smallest ordinal in $\alpha$ such that $\neg \map P \beta$.
Since $y$ is transitive by definition:
:$\beta \in \alpha \land \alpha \in y \implies \beta \in y$
And so $\beta$ is an ordinal in $y$ such that $\neg \map P \beta$.
But since $\beta < \alpha$, this contradicts the fact that $\alpha$ is the smallest ordinal of $y$ such that $\neg \map P \alpha$.
Therefore $\map P x$ holds for all ordinals.
Hence the result.
{{qed}}
Theorem: Transfinite Induction/Schema 1

Let $\map P x$ be a property 
Suppose that:
:If $\map P x$ holds for all ordinals $x$ less than $y$, then $\map P y$ also holds.
Then $\map P x$ holds for all ordinals $x$.

Proof:
It should be noted that for any two ordinals, $x < y \iff x \in y$.
Let $\map P x$ be a property that satisfies the above conditions.
{{AimForCont}} $y$ is an ordinal such that $\neg \map P y$.
Let $S$ be the set defined as:
:$S = \set {x \in y^+: \neg \map P x}$
It is seen that this set is non-empty because by Set is Element of Successor:
:$y \in y^+$
$y^+$ is an ordinal because of Successor Set of Ordinal is Ordinal.
By Element of Ordinal is Ordinal, $S$ is a set of ordinals.
By the Rule of Transposition, it follows that for every $x \in S$, there exists an ordinal $\alpha < x \iff \alpha \in x$ such that $\neg \map P \alpha$.
But by transitivity:
:$\alpha \in x \land x \in y^+ \implies \alpha \in y^+$
So the epsilon restriction $\in_S$ is a right-total relation on $S$.
Therefore by the Axiom of Dependent Choice there exists a sequence $\sequence {x_n}_{n \mathop \in \N}$ in $S$ such that:
:$\forall n \in \N: x_{n + 1} \in x_n$
But this contradicts No Infinitely Descending Membership Chains.
Thus $\map P x$ holds for all ordinals.
Hence the result.
{{qed}}
Theorem: Transfinite Induction/Principle 2

Let $A$ be a class satisfying the following conditions:
* $\O \in A$
* $\forall x \in A: x^+ \in A$
* If $y$ is a limit ordinal, then $\paren {\forall x < y: x \in A} \implies y \in A$
where $x^+$ denotes the successor of $x$.
Then $\On \subseteq A$.

Proof:
{{NotZFC}}
We shall prove this using the first principle of transfinite induction.
Assume $y$ is an ordinal such that $y \subseteq A$.
This implies $\forall x < y: x \in A$.
By definition, $y$ is a limit ordinal, $y = \O$, or $\exists x: y = x^+$.
If $y$ is a limit ordinal, then, since:
:$\forall x < y: x \in A$
it follows that $y \in A$.
If $y = \O$, then $y \in A$ {{hypothesis}}.
Finally, assume $y = z^+$ for some ordinal $z$.
Since $z < z^+ = y$ and $\forall x < y: x \in A$, it follows that $z \in A$.
By hypothesis, we conclude $y = z^+ \in A$.
In any case, $y \in A$.
Therefore, for all ordinals $y$, if $y \subseteq A$, then $y \in A$.
By the first principle of transfinite induction, $\On \subseteq A$.
{{qed}}
Category:Transfinite Induction
ndgd0yxstkd6tiqmmnclh2hzvvecacf
Theorem: Transfinite Induction/Schema 2

Let $\map \phi x$ be a property satisfying the following conditions:
:$(1): \quad \map \phi \O$ is true
:$(2): \quad$ If $x$ is an ordinal, then $\map \phi x \implies \map \phi {x^+}$
:$(3): \quad$ If $y$ is a limit ordinal, then $\paren {\forall x < y: \map \phi x} \implies \map \phi y$
where $x^+$ denotes the successor of $x$.
Then, $\map \phi x$ is true for all ordinals $x$.

Proof:
It should be noted that for any two ordinals, $x \lt y \iff x \in y$.
Let $\map \phi x$ be a property that satisfies the above conditions.
{{AimForCont}} $y$ be an ordinal such that $\neg \map \phi y$.
It is noted that $y \ne \O$.
Therefore $y$ must be either a successor ordinal or a limit ordinal.
If $y$ is a successor ordinal, then let $x$ be the ordinal such that $x^+ = y$.
By the Rule of Transposition, it is seen that $\neg \map \phi x$.
By Set is Element of Successor, it follows that $x \in y$, and so $x \lt y$.
If $y$ is a limit ordinal, then by the Rule of Transposition there exists an ordinal $x \lt y \iff x \in y$ such that $\neg \map \phi x$.
It has been shown that if $y$ is an ordinal such that $\neg \map \phi y$, then there exists an ordinal $x \in y$ such that $\neg \map \phi x$.
The rest follows from the proof of Schema 1.
{{qed}}
Theorem: Transfinite Induction/Schema 2

Let $\map \phi x$ be a property satisfying the following conditions:
:$(1): \quad \map \phi \O$ is true
:$(2): \quad$ If $x$ is an ordinal, then $\map \phi x \implies \map \phi {x^+}$
:$(3): \quad$ If $y$ is a limit ordinal, then $\paren {\forall x < y: \map \phi x} \implies \map \phi y$
where $x^+$ denotes the successor of $x$.
Then, $\map \phi x$ is true for all ordinals $x$.

Proof:
Define the class:
:$A := \set {x \in \On: \map \phi x = \T}$.
Then $\map \phi x = \T$ is equivalent to the statement:
:that $x \in A$
The three conditions in the hypothesis become:
:$(1a): \quad \O \in A$
:$(2a): \quad x \in A \implies x^+ \in A$
:$(3a): \quad \paren {\forall x < y: x \in A} \implies y \in A$
These are precisely the conditions for the class $A$ in the second principle of transfinite induction.
Therefore, $\On \subseteq A$.
Thus, $\map \phi x$ holds for all $x \in \On$.
{{qed}}
Theorem: Transfinite Recursion Theorem/Theorem 2

Let $\Dom x$ denote the domain of $x$.
Let $\Img x$ denote the image of the mapping $x$.
{{explain|We infer that $x$ is a mapping, but what is its context?}}
Let $G$ be a class of ordered pairs $\tuple {x, y}$ satisfying at least one of the following conditions:
:$(1): \quad x = \O$ and $y = a$
{{explain|What is $a$?}}
:$(2): \quad \exists \beta: \Dom x = \beta^+$ and $y = \map H {\map x {\bigcup \Dom x} }$
{{explain|What is $H$?}}
:$(3): \quad \Dom x$ is a limit ordinal and $y = \bigcup \Rng x$.
{{explain|Is this invoking well-founded recursion?}}
Let $\map F \alpha = \map G {F \restriction \alpha}$ for all ordinals $\alpha$.
Then:
:$F$ is a mapping and the domain of $F$ is the class of all ordinals, $\On$.
:$\map F \O = a$
:$\map F {\beta^+} = \map H {\map F \beta}$
:For limit ordinals $\beta$, $\ds \map F \beta = \bigcup_{\gamma \mathop \in \beta} \map F \gamma$
:$F$ is unique.
::That is, if there is another function $A$ satisfying the above three properties, then $A = F$.

Proof:
{{begin-eqn}}
{{eqn | l = \map F \O
      | r = \map G {F \restriction \O}
      | c = {{Hypothesis}}
}}
{{eqn | r = \map G \O
      | c = Restriction of $\O$
}}
{{eqn | r = a
      | c = Definition of $G$
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = \map F {\beta^+}
      | r = \map G {F \restriction \beta^+}
      | c = {{Hypothesis}}
}}
{{eqn | r = \map H {\map {F \restriction \beta^+} {\bigcup \beta^+} }
      | c = Definition of $G$
}}
{{eqn | r = \map H {\map F \beta}
      | c = Union of successor set is the original set by Union of Ordinals is Least Upper Bound
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = \map F \beta
      | r = \map G {F \restriction \beta}
      | c = {{Hypothesis}}
}}
{{eqn | r = \bigcup \Img {F \restriction \beta}
      | c = Definition of $G$
}}
{{eqn | r = \bigcup_{\gamma \mathop \in \beta} \map F \gamma
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
We can proceed in the fourth part by Transfinite Induction.
Theorem: Transfinite Recursion Theorem/Corollary

Let $x$ be an ordinal.
Let $G$ be a mapping
There exists a unique mapping $f$ that satisfies the following properties:
:The domain of $f$ is $x$
:$\forall y \in x: \map f y = \map G {f \restriction y}$

Proof:
Construct $K$ and $F$ as in the First Principle of Transfinite Recursion.
Set $f = \paren {F \restriction x}$.
Then since $x \subseteq \Dom F$, the domain of $f$ is $x$.
{{begin-eqn}}
{{eqn | q = \forall y \in x
      | l = \map f y
      | r = \map F y
      | c = from the fact that $f$ is a restriction
}}
{{eqn | r = \map G {F \restriction y}
      | c = First Principle of Transfinite Recursion
}}
{{eqn | r = \map G {f \restriction y}
      | c = 
}}
{{end-eqn}}
Thus such a mapping $f$ exists.
Suppose there are two mappings $f$ and $g$ that satisfy these conditions.
We will use the first principle of transfinite induction to show that $f = g$.
Take $y \in x$.
Suppose $\forall z \in y: \map f z = \map g z$.
Then:
:$\paren {f \restriction y} = \paren {g \restriction y}$
and so:
{{begin-eqn}}
{{eqn | l = \map f y
      | r = \map G {f \restriction y}
      | c = Assumption
}}
{{eqn | r = \map G {g \restriction y}
      | c = Substitutivity of Equality
}}
{{eqn | r = \map g y
      | c = {{Hypothesis}}
}}
{{end-eqn}}
So $\map f y = \map g y$ for all $y \in x$ by transfinite induction.
Since $x$ is the domain of $f$ and $g$, it follows that $f = g$.
Thus the mapping $f$ is unique.
{{qed}}
Theorem: Inverse of Product/Monoid/General Result

Let $\struct {S, \circ}$ be a monoid whose identity is $e$.
Let $a_1, a_2, \ldots, a_n \in S$ be invertible for $\circ$, with inverses ${a_1}^{-1}, {a_2}^{-1}, \ldots, {a_n}^{-1}$.
Then $a_1 \circ a_2 \circ \cdots \circ a_n$ is invertible for $\circ$, and:
:$\forall n \in \N_{> 0}: \paren {a_1 \circ a_2 \circ \cdots \circ a_n}^{-1} = {a_n}^{-1} \circ \cdots \circ {a_2}^{-1} \circ {a_1}^{-1}$

Proof:
Proof by induction:
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\paren {a_1 \circ a_2 \circ \cdots \circ a_n}^{-1} = {a_n}^{-1} \circ \cdots \circ {a_2}^{-1} \circ {a_1}^{-1}$
$\map P 1$ is (trivially) true, as this just says:
:$\paren {a_1}^{-1} = {a_1}^{-1}$
Theorem: Inverse of Group Product

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $a, b \in G$, with inverses $a^{-1}, b^{-1}$.
Then:
:$\paren {a \circ b}^{-1} = b^{-1} \circ a^{-1}$

Proof:
We have that a group is a monoid, all of whose elements are invertible.
The result follows from Inverse of Product/Monoid/General Result.
{{Qed}}
Theorem: Inverse of Group Product

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $a, b \in G$, with inverses $a^{-1}, b^{-1}$.
Then:
:$\paren {a \circ b}^{-1} = b^{-1} \circ a^{-1}$

Proof:
Proof by induction:
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\paren {a_1 \circ a_2 \circ \cdots \circ a_n}^{-1} = a_n^{-1} \circ \cdots \circ a_2^{-1} \circ a_1^{-1}$
$\map P 1$ is (trivially) true, as this just says:
:$\paren {a_1}^{-1} = a_1^{-1}$
=== Basis for the Induction ===
$\map P 2$ is the case:
:$\paren {a_1 \circ a_2}^{-1} = a_2^{-1} \circ a_1^{-1}$
which has been proved in Inverse of Group Product.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\paren {a_1 \circ a_2 \circ \cdots \circ a_k}^{-1} = a_k^{-1} \circ \cdots \circ a_2^{-1} \circ a_1^{-1}$
Then we need to show:
:$\paren {a_1 \circ a_2 \circ \cdots \circ a_{k + 1} }^{-1} = a_{k + 1}^{-1} \circ \cdots \circ a_2^{-1} \circ a_1^{-1}$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = \paren {a_1 \circ a_2 \circ \cdots \circ a_k \circ a_{k + 1} }^{-1}
      | r = \paren {\paren {a_1 \circ a_2 \circ \cdots \circ a_k} \circ a_{k + 1} }^{-1}
      | c = General Associativity Theorem
}}
{{eqn | r = a_{k + 1}^{-1} \circ \paren {a_1 \circ a_2 \circ \cdots \circ a_k}^{-1}
      | c = Basis for the Induction
}}
{{eqn | r = a_{k + 1}^{-1} \circ \paren {a_k^{-1} \circ \cdots \circ a_2^{-1} \circ a_1^{-1} }
      | c = Induction Hypothesis
}}
{{eqn | r = a_{k + 1}^{-1} \circ a_k^{-1} \circ \cdots \circ a_2^{-1} \circ a_1^{-1}
      | c = General Associativity Theorem
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall n \in \N_{> 0}: \paren {a_1 \circ a_2 \circ \cdots \circ a_n}^{-1} = a_n^{-1} \circ \cdots \circ a_2^{-1} \circ a_1^{-1}$
{{qed}}
Theorem: Inverse of Group Product

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $a, b \in G$, with inverses $a^{-1}, b^{-1}$.
Then:
:$\paren {a \circ b}^{-1} = b^{-1} \circ a^{-1}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {a \circ b} \circ \paren {b^{-1} \circ a^{-1} }
      | r = \paren {\paren {a \circ b} \circ b^{-1} } \circ a^{-1}
      | c = {{Group-axiom|1}}
}}
{{eqn | r = \paren {a \circ \paren {b \circ b^{-1} } } \circ a^{-1}
      | c = {{Group-axiom|1}}
}}
{{eqn | r = \paren {a \circ e} \circ a^{-1}
      | c = {{Group-axiom|3}}
}}
{{eqn | r = a \circ a^{-1}
      | c = {{Group-axiom|2}}
}}
{{eqn | r = e
      | c = {{Group-axiom|3}}
}}
{{end-eqn}}
The result follows from Group Product Identity therefore Inverses:
:$\paren {a \circ b} \circ \paren {b^{-1} \circ a^{-1} } = e \implies \paren {a \circ b}^{-1} = b^{-1} \circ a^{-1}$
{{Qed}}
Theorem: Inverse of Group Product

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $a, b \in G$, with inverses $a^{-1}, b^{-1}$.
Then:
:$\paren {a \circ b}^{-1} = b^{-1} \circ a^{-1}$

Proof:
We have that a group is a monoid, all of whose elements are invertible.
The result follows from Inverse of Product in Monoid.
{{Qed}}