avewright/proofwiki-math huggingface dataset:
Theorem: Difference of Unbounded Closed Intervals

Let $a, b \in \R$ have $a < b$. 
Then: 
:$\hointl {-\infty} b \setminus \hointl {-\infty} a = \hointl a b$
where $\setminus$ denotes set difference.

Proof:
Note that: 
:$x \in \hointl {-\infty} b \setminus \hointl {-\infty} a$
{{iff}}: 
:$x \in \hointl {-\infty} b$ but $x \not \in \hointl {-\infty} a$.
That is: 
:$x \le b$ but it is not the case that $x \le a$. 
So this is equivalent to: 
:$x \le b$ and $x > a$.
That is: 
:$x \in \hointl a b$
So:
:$\hointl {-\infty} b \setminus \hointl {-\infty} a = \hointl a b$
{{qed}}
Category:Real Intervals
eviyywh86e8uidy0ntj9t1txzcwr9rz
Theorem: Fundamental Theorem of Riemannian Geometry

Let $\struct {M, g}$ be a Riemannian or pseudo-Riemannian manifold with or without boundary.
Let $\nabla$ be a Levi-Civita connection.
Then $\nabla$ is unique.

Proof:
{{ProofWanted}}
{{Namedfor|Bernhard Riemann|cat = Riemann}}
Theorem: Limit of Decreasing Sequence of Left Half-Open Intervals with Lower Bound Converging to Upper Bound

Let $a, b \in \R$ have $a < b$.
Let $\sequence {a_n}_{n \mathop \in \N}$ be an increasing sequence with $a_n \to b$. 
Then we have: 
:$\ds \bigcap_{n \mathop = 1}^\infty \hointl {a_n} b = \set b$ 
That is: 
:$\hointl {a_n} b \downarrow \set b$
where $\downarrow$ denotes the limit of decreasing sequence of sets.

Proof:
Clearly:
:$\ds b \in \bigcap_{n \mathop = 1}^\infty \hointl {a_n} b$
so that: 
:$\ds \set b \subseteq \bigcap_{n \mathop = 1}^\infty \hointl {a_n} b$
Now let: 
:$\ds x \in \bigcap_{n \mathop = 1}^\infty \hointl {a_n} b$
Then: 
:$a_n \le x \le b$ 
for each $n \in \N$.
From Limits Preserve Inequalities, we then have: 
:$b \le x \le b$
so that: 
:$x = b$ 
So: 
:$\ds \bigcap_{n \mathop = 1}^\infty \hointl {a_n} b = \set b$
as required.
{{qed}}
Category:Decreasing Sequences of Sets
lfj2kfml01pyieholwihtzvqea6nd2x
Theorem: Convolution Operator is Continuous Linear Transformation

Let $\map {L^1} \R$ and $\map {L^\infty} \R$ be the real Lebesgue $1$- and  real Lebesgue $\infty$-spaces respectively.
Let $f \in \map {L^1} \R$.
Let $f* : \map {L^\infty} \R \to \map {L^\infty} \R$ be the convolution integral such that:
:$\ds \forall t \in \R : \forall g \in \map {L^\infty} \R : \map {\paren {f * g} } t = \int_{-\infty}^\infty \map f {t - \tau} \map g \tau \rd \tau$
Then $f*$ is well defined and $f* \in \map {CL} {\map {L^\infty} \R}$, where $CL$ denotes the continuous linear transformation space.

Proof:
{{begin-eqn}}
{{eqn | ll= \forall t \in \R : \forall g \in \map {L^\infty} \R :
      | l = \size {\map {\paren {f*g} } t}
      | r = \size {\int_{-\infty}^\infty \map f {t - \tau} \map g \tau \rd \tau }
      | c = {{Defof|Convolution Integral}}
}}
{{eqn | o = \le
      | r = \int_{-\infty}^\infty \size {\map f {t - \tau} } \size {\map g \tau} \rd \tau
}}
{{eqn | o = \le
      | r = \int_{-\infty}^\infty \size {\map f {t - \tau} } \norm g_\infty \rd \tau
      | c = {{Defof|Supremum Norm}}
}}
{{eqn | r = \norm g_\infty \int_{-\infty}^\infty \size {\map f {t - \tau} } \rd \tau
}}
{{eqn | r = \norm g_\infty \int_{-\infty}^\infty \size {\map f \sigma } \rd \sigma
      | c = Integration by Substitution, $\sigma = t - \tau$
}}
{{eqn | r = \norm g_\infty \norm f_1
      | c = {{Defof|P-Seminorm}}
}}
{{eqn | o = <
      | r = \infty
      | c = {{Defof|Lebesgue Space}}
}}
{{end-eqn}}
Thus, an element of the image of $f*$ is bounded.
Therefore, $f*$ is well-defined.
{{Research|What does "well-defined" mean here? How does boundedness translate to well-definedness of $f*$?}}
By definition, $f*$ is integral operator.
By Integral Operator is Linear, $f*$ is linear.
We have that $\norm f_1 \in \R$.
By Continuity of Linear Transformation between Normed Vector Spaces, $f*$ is continuous.
{{qed}}
Theorem: Tests for Finite Set Equality

Let $S$ and $T$ be finite sets.
Let $S \subseteq T$.
{{TFAE}}
:$(a): \quad \card S = \card T$
:$(b): \quad \card {T \setminus S} = 0$
:$(c): \quad T \setminus S = \O$
:$(d): \quad T = S$

Proof:
We have:
{{begin-eqn}}
{{eqn | n = a
      | l = \card S
      | r = \card T
}}
{{eqn | n = b
      | ll = \leadstoandfrom
      | l = \card {T \setminus S}
      | r = \card T - \card S = 0
      | c = Cardinality of Set Difference with Subset
}}
{{eqn | n = c
      | ll = \leadstoandfrom
      | l = T \setminus S
      | r = \O
      | c = Cardinality of Empty Set
}}
{{eqn | ll = \leadstoandfrom
      | l = T 
      | o = \subseteq
      | r = S
      | c = Set Difference with Superset is Empty Set
}}
{{eqn | n = d
      | ll = \leadstoandfrom
      | l = T 
      | r = S
      | c = {{Defof|Set Equality}}
}}
{{end-eqn}}
Category:Set Equality
Category:Finite Sets
m89qsu6wq9xs9ezp1c3gbynk3dr5fni
Theorem: Powers of Field Elements Commute

Let $\struct {F, +, \circ}$ be a field with zero $0_F$ and unity $1_F$.
Let $F^* = F \setminus {0_F}$ denote the set of elements of $F$ without the zero $0_F$.
Then:
:$(a):\quad \forall a \in \F^* : \forall n, m \in \Z : a^m \circ a^n = a^n \circ a^m$
:$(b):\quad \forall a \in F : \forall n, m \in \Z_{\ge 0} : a^m \circ a^n = a^n \circ a^m$

Proof:
=== Statement $(a)$ ===
By {{Defof|Field (Abstract Algebra)|Field}}:
:$\struct{F^*, \circ}$ is an Abelian group
By {{Defof|Power of Field Element}}:
:For all $a \in F^*$ and $n \in \Z$, $a^n$ is defined as the $n$th power of $a$ with respect to the Abelian group $\struct {F^*, \circ}$
From Powers of Group Element Commute:
:$\forall a \in \F^* : \forall n, m \in \Z : a^m \circ a^n = a^n \circ a^m$
{{qed|lemma}}
Theorem: Index Laws/Negative Index/Field

:$\forall a \in \F^* : \forall n \in \Z : \paren{a^n}^{-1} = a^{-n} = \paren{a^{-1}}^n$

Proof:
By {{Defof|Field (Abstract Algebra)|Field}}:
:$\struct{F^*, \circ}$ is an Abelian group
By {{Defof|Power of Field Element}}:
:For all $a \in F^*$ and $n \in \Z$, $a^n$ is defined as the $n$th power of $a$ with respect to the Abelian group $\struct {F^*, \circ}$
From Negative Powers of Group Elements:
:$\forall a \in \F^* : \forall n \in \Z : \paren{a^n}^{-1} = a^{-n} = \paren{a^{-1}}^n$
{{qed}}
Category:Index Laws
31u1orap1ypp4d1g3vjg4jfsv43dqmv
Theorem: Index Laws/Sum of Indices/Field

:$(a):\quad \forall a \in \F^* : \forall n, m \in \Z : a^m \circ a^n = a^\paren{m + n}$
:$(b):\quad \forall a \in \F : \forall n, m \in \Z_{\ge 0} : a^m \circ a^n = a^\paren{m + n}$

Proof:
=== Statement $(a)$ ===
By {{Defof|Field (Abstract Algebra)|Field}}:
:$\struct{F^*, \circ}$ is an Abelian group
By {{Defof|Power of Field Element}}:
:For all $a \in F^*$ and $n \in \Z$, $a^n$ is defined as the $n$th power of $a$ with respect to the Abelian group $\struct {F^*, \circ}$
From Sum of Powers of Group Elements:
:$\forall a \in \F^* : \forall n, m \in \Z : a^m \circ a^n = a^\paren{m + n}$
{{qed|lemma}}
Theorem: Index Laws/Product of Indices/Field

:$(a):\quad \forall a \in \F^* : \forall n, m \in \Z : \paren{a^m}^n = a^\paren{mn}$
:$(b):\quad \forall a \in \F : \forall n, m \in \Z_{\ge 0} : \paren{a^m}^n = a^\paren{mn}$

Proof:
=== Statement $(a)$ ===
By {{Defof|Field (Abstract Algebra)|Field}}:
:$\struct{F^*, \circ}$ is an Abelian group
By {{Defof|Power of Field Element}}:
:For all $a \in F^*$ and $n \in \Z$, $a^n$ is defined as the $n$th power of $a$ with respect to the Abelian group $\struct {F^*, \circ}$
From Product of Powers of Group Elements:
:$\forall a \in \F^* : \forall n, m \in \Z : \paren{a^m}^n = a^\paren{mn}$
{{qed|lemma}}
Theorem: Index Laws/Common Index/Field

{{begin-eqn}}
{{eqn | n = $a$
      | q = \forall a, b \in \F^*
      | qq= \forall n \in \Z
      | l = a^n \circ b^n
      | r = \paren {a b}^n
}}
{{eqn | n = $b$
      | q = \forall a, b \in \F
      | qq= \forall n \in \Z_{\ge 0}
      | l = a^n \circ b^n
      | r = \paren {a b}^n
}}
{{end-eqn}}

Proof:
=== Statement $(a)$ ===
By {{Defof|Field (Abstract Algebra)|Field}}:
:$\struct{F^*, \circ}$ is an Abelian group
By {{Defof|Power of Field Element}}:
:For all $a \in F^*$ and $n \in \Z$, $a^n$ is defined as the $n$th power of $a$ with respect to the Abelian group $\struct {F^*, \circ}$
From Sum of Powers of Group Elements:
:$\forall a \in \F^* : \forall n, m \in \Z : a^m \circ a^n = a^\paren{m + n}$
{{qed|lemma}}
Theorem: G-Tower is G-Ordered

Let $M$ be a class.
Let $g: M \to M$ be a progressing mapping on $M$.
Let $M$ be a $g$-tower.
Then $M$ is $g$-ordered.

Proof:
Recall the definition of a $g$-ordered class:
$M$ is a $g$-ordered class {{iff}} $M$ is well-ordered by the subset relation such that:
{{begin-axiom}}
{{axiom | n = 1
        | t = the smallest element of $M$ is $\O$
}}
{{axiom | n = 2
        | t = every immediate successor $y$ is $\map g x$, where $x$ is the immediate predecessor of $y$
}}
{{axiom | n = 3
        | t = every limit element $x$ of $M$ is the union of the set of all predecessor elements of $x$
}}
{{end-axiom}}
So, let $M$ be a $g$-tower.
From $g$-Tower is Well-Ordered under Subset Relation:
:$M$ is well-ordered under the subset relation.
From $g$-Tower is Well-Ordered under Subset Relation: Empty Set:
:$\O$ is the smallest element of $M$.
From $g$-Tower is Well-Ordered under Subset Relation: Successor of Non-Greatest Element:
:Let $x \in M$ such that $x$ is not the greatest element of $M$.
:Then the immediate successor of $x$ is $\map g x$.
From $g$-Tower is Well-Ordered under Subset Relation: Union of Limit Elements:
:Let $x \in M$ be a limit element of $M$.
:Then:
::$x = \bigcup x^\subset$
:where $\bigcup x^\subset$ denotes the union of the lower section of $x$.
The result follows.
{{qed}}
Theorem: Integer Power of Root of Unity is Root of Unity

Let $n \in \Z_{> 0}$ be a strictly positive integer.
Let $F$ be a field.
Let $\alpha$ be an $n$-th root of unity.
Let $k \in \Z$.
Then:
:$\alpha^k$ is an $n$-th root of unity.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \alpha^n
      | r = 1
      | c = By Assumption
}}
{{eqn | l = \paren{\alpha^n}^k
      | r = 1^k
      | c = 
}}
{{eqn | l = \paren{\alpha^k}^n
      | r = 1
      | c = Product of Indices Law for Field
}}
{{end-eqn}}
{{qed}}
Category:Roots of Unity
kogr9c6m0ik1uo6e99ev1bkenfhu0qc
Theorem: Set is G-Set iff Element of G-Ordered Set

Let $g$ be a progressing mapping.
Let $x$ be a set.
Then:
:$x$ is a $g$-set
{{iff}}:
:$x$ is an element of a $g$-ordered set.

Proof:
Let $M$ be the class of all $g$-sets.
Then $M$ is a $g$-tower.
Theorem: Congruent Powers of Root of Unity are Equal

Let $n \in \Z_{>0}$ be a strictly positive integer.
Let $F$ be a field.
Let $\alpha$ be an $n$th root of unity.
Let $k, l \in \Z$ such that $k \equiv l \pmod n$.
Then:
:$\alpha^k = \alpha^l$

Proof:
By {{Defof|Congruence Modulo Integer}}:
:$\exists c \in \Z : k = l + c n$
We have:
{{begin-eqn}}
{{eqn | l = \alpha^k
      | r = \alpha^{\paren {l + c n} }
}}
{{eqn | r = \alpha^l \alpha^{\paren {c n} }
      | c = Sum of Indices Law for Field
}}
{{eqn | r = \alpha^l \cdot 1
      | c = Integer Power of Root of Unity is Root of Unity
}}
{{eqn | r = \alpha^l
}}
{{end-eqn}}
{{qed}}
Category:Roots of Unity
bfxr80zse326dy0lueg0bi4wbqec530
Theorem: Power of Root of Unity Equals Power of Remainder

Let $n \in \Z_{> 0}$ be a strictly positive integer.
Let $F$ be a field.
Let $\alpha$ be an $n$-th root of unity.
Let $k \in \Z$.
Then:
:$\alpha^k = \alpha^r$
where $0 \le r < n$ is the remainder of $k$ on division by $n$.

Proof:
From Division Theorem:
:$\exists r, c \in \Z : 0 \le r < n : k = r + c n$
By {{Defof|Congruence Modulo Integer}}:
:$k \equiv r \pmod n$
From Congruent Powers of Root of Unity are Equal
:$\alpha^k = \alpha^r$
{{qed}}
Category:Roots of Unity
o141p9qnp7h8wekn6jxfsr1dr8xmzlg
Theorem: Conditional Entropy Given Trivial Sigma-Algebra is Entropy

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $\AA \subseteq \Sigma$ be a finite sub-$\sigma$-algebra.
Let $\NN := \set {\O, \Omega}$ be the trivial $\sigma$-algebra.
Then:
:$\ds \map H {\AA \mid \NN} = \map H \AA$
where:
:$\map H {\cdot \mid \cdot}$ denotes the conditional entropy
:$\map H {\, \cdot \,}$ denotes the entropy

Proof:
{{begin-eqn}}
{{eqn | l = \map H {\AA \mid \NN}
      | r = \map H {\map \xi \AA  \mid \map \xi \NN}
      | c = {{Defof|Conditional Entropy of Finite Sub-Sigma-Algebra|Conditional Entropy of Finite Sub-$\sigma$-Algebra}}
}}
{{eqn | r =  \sum_{\substack {B \mathop \in {\map \xi \NN } \\ \map \Pr B \mathop > 0} } \sum_{A \mathop \in {\map \xi \AA } } \map \Pr B \map \phi {\dfrac {\map \Pr {A \cap B} } {\map \Pr B} }
      | c = {{Defof|Conditional Entropy of Finite Partitions}}
}}
{{eqn | r = \sum_{A \mathop \in {\map \xi \AA } } \map \Pr \Omega \map \phi {\dfrac {\map \Pr {A \cap \Omega} } {\map \Pr \Omega} }
      | c = as $\map \xi \NN = \set \Omega$ by definition of Finite Partition Generated by Finite Sub-$\sigma$-Algebra
}}
{{eqn | r = \sum_{A \mathop \in {\map \xi \AA } } \map \phi {\map \Pr {A \cap \Omega} }
      | c = as $\map \Pr \Omega = 1$ by definition of Probability Measure
}}
{{eqn | r = \sum_{A \mathop \in {\map \xi \AA } } \map \phi {\map \Pr A }
      | c = $\forall A \in \Sigma : A \subseteq \Omega$
}}
{{eqn | r = \map H {\map \xi \AA}
      | c = {{Defof|Entropy of Finite Partition}}
}}
{{eqn | r = \map H \AA
      | c = {{Defof|Entropy of Finite Sub-Sigma-Algebra|Entropy of Finite Sub-$\sigma$-Algebra}}
}}
{{end-eqn}}
{{qed}}
Theorem: Preimage of Union Mapping is Union of Preimages

Let $A$, $B$ and $Y$ be sets.
Let $f: A \to Y$ and $g: B \to Y$ be mappings that agree on $A \cap B$.
Let $f \cup g$ be the union of the mappings $f$ and $g$:
:$\forall x \in A \cup B: \map {f \cup g} x = \begin {cases} \map f x & : x \in A \\ \map g x & : x \in B \end {cases}$
Let $S \subseteq Y$ be a subset of $Y$.
Then:
:$\paren {f \cup g}^{-1} \sqbrk S = f^{-1} \sqbrk S \cup g^{-1} \sqbrk S$

Proof:
From Union of Mappings which Agree is Mapping:
:$f \cup g$ is well-defined
Let $x \in \paren {f \cup g}^{-1} \sqbrk S$
By {{Defof|Inverse Image}}:
:$\paren {f \cup g}^{-1} \sqbrk S \subseteq A \cup B$
Let $x \in A$.
We have:
:$\map f x = \map {\paren {f \cup g} } x \in S$
By {{Defof|Inverse Image}}:
:$x \in f^{-1} \sqbrk S \subseteq f^{-1} \sqbrk S \cup g^{-1} \sqbrk S$
Let $x \in B$.
We have:
:$\map g x = \map {\paren {f \cup g} } x \in S$
By {{Defof|Inverse Image}}:
:$x \in g^{-1} \sqbrk S \subseteq f^{-1} \sqbrk S \cup g^{-1} \sqbrk S$
In both cases: 
:$x \in f^{-1} \sqbrk U \cup g^{-1} \sqbrk S$
By {{Defof|Subset}}:
:$\paren {f \cup g}^{-1} \sqbrk S \subseteq f^{-1} \sqbrk S \cup g^{-1} \sqbrk S$
Let $x \in f^{-1} \sqbrk S \cup g^{-1} \sqbrk S$.
{{WLOG}} consider the case of $x \in f^{-1} \sqbrk S \subseteq A$.
Then:
$\map {\paren {f \cup g} } x = \map f x \in S$
Hence:
:$x \in \paren {f \cup g}^{-1} \sqbrk S$
By {{Defof|Subset}}:
:$f^{-1} \sqbrk S \cup g^{-1} \sqbrk S \subseteq \paren {f \cup g}^{-1} \sqbrk S$
By {{Defof|Set Equality}}:
:$f^{-1} \sqbrk S \cup g^{-1} \sqbrk S = \paren {f \cup g}^{-1} \sqbrk S$
{{qed}}
Category:Preimages under Mappings
Category:Union Mappings
qn19bi7cv443vxr4ylftd959qg3ahgw
Theorem: Square of Norm of Vector Cross Product

Let $\mathbf a$ and $\mathbf b$ be vectors in the real Euclidean space $\R^3$.
Let $\times$ denote the vector cross product.
Then:
:$\norm {\mathbf a \times \mathbf b}^2 = \norm {\mathbf a}^2 \norm {\mathbf b}^2 - \paren {\mathbf a \cdot \mathbf b}^2$

Proof:
Let $\mathbf a = \begin{bmatrix} a_1 \\ a_2 \\ a_3 \end{bmatrix}$, and $\mathbf b = \begin{bmatrix} b_1 \\ b_2 \\ b_3 \end{bmatrix}$.
Then:
{{begin-eqn}}
{{eqn | l = \norm {\mathbf a \times \mathbf b }^2
      | r = \paren {\mathbf a \times \mathbf b } \cdot \paren {\mathbf a \times \mathbf b}
      | c = {{Defof|Euclidean Norm}}
}}
{{eqn | r = \begin {bmatrix} a_2 b_3 - a_3 b_2 \\ a_3 b_1 - a_1 b_3 \\ a_1 b_2 - a_2 b_1 \end {bmatrix} \cdot \begin {bmatrix} a_2 b_3 - a_3 b_2 \\ a_3 b_1 - a_1 b_3 \\ a_1 b_2 - a_2 b_1 \end {bmatrix}
      | c = {{Defof|Vector Cross Product}}
}}
{{eqn | r = {a_2}^2 {b_3}^2 + {a_3}^2 {b_2}^2 - 2 a_2 a_3 b_2 b_3 + {a_3}^2 {b_1}^2 + {a_1}^2 {b_3}^2 - 2 a_1 a_3 b_1 b_3 + {a_1}^2 {b_2}^2 + {a_2}^2 {b_1}^2 - 2 a_1 a_2 b_1 b_2
      | c = {{Defof|Dot Product}}
}}
{{eqn | r = \paren { {a_1}^2 + {a_2}^2 + {a_3}^2} \paren { {b_1}^2 + {b_2}^2 + {b_3}^2} - \paren {a_1 b_1 + a_2 b_2 + a_3 b_3}^2
      | c = by algebraic manipulations
}}
{{eqn | r = \paren {\mathbf a \cdot \mathbf a} \paren {\mathbf b \cdot \mathbf b} - \paren {\mathbf a \cdot \mathbf b}^2
      | c = {{Defof|Dot Product}}
}}
{{eqn | r = \norm {\mathbf a}^2 \norm {\mathbf b}^2 - \paren {\mathbf a \cdot \mathbf b}^2
      | c = {{Defof|Euclidean Norm}}
}}
{{end-eqn}}
{{qed}}
Theorem: Class of All Ordinals is Minimally Superinductive over Successor Mapping

The class of all ordinals $\On$ is the unique class which is minimally superinductive under the successor mapping.

Proof:
We need to show that:
:$\On$ is a superinductive class under the successor mapping
and:
:no proper subclass of $\On$ is superinductive class under the successor mapping.
We recall immediately that Successor Mapping is Progressing.
This validates the definition of superinductive class under the successor mapping.
By definition of '''ordinal''':
:$S \in \On$
{{iff}}:
:$S$ is an element of every superinductive class under the successor mapping.
Hence $\On$ is a subclass of every superinductive class under the successor mapping.
Let $\cap S$ denote the  intersection of every superinductive class under the successor mapping.
Thus by definition of class intersection:
:$\On$ is a subclass of $\cap S$.
Let $M$ be an arbitrary superinductive class under the successor mapping.
We have by definition of superinductive class:
:$\O \in M$
Thus as $M$ is arbitrary:
:$\O \in \cap S$
Thus $\O$ is an element of every superinductive class.
Hence:
:$\O \in \On$
{{qed|lemma}}
Now let $\alpha \in \On$.
Then by definition of ordinal:
:$\alpha$ is an element of every superinductive class under the successor mapping.
Hence by definition of superinductive class:
:$\alpha^+$ is an element of every superinductive class under the successor mapping
where $\alpha^+$ denotes the successor set of $\alpha$.
Hence by definition:
:$\alpha^+ \in \On$
Thus $\On$ is closed under the successor mapping.
{{qed|lemma}}
Let $C$ be a chain in $\On$.
Then $C$ is a chain in every superinductive class under the successor mapping.
By definition of superinductive class:
:$\cup C$ is an element of every superinductive class under the successor mapping
where $\cup C$ denotes the union of $C$.
That is:
:$\cup C \in \On$
demonstrating that $\On$ is closed under chain unions.
{{qed|lemma}}
Thus $\On$ is a superinductive class.
{{qed|lemma}}
{{AimForCont}} $A$ is a superinductive class which is a proper subclass of $\On$.
Then:
:$\exists x \in \On: x \notin A$
Hence $\On \not \subseteq A$
But this contradicts the statement that $\On$ is a subclass of every superinductive class.
Hence by Proof by Contradiction no proper subclass of $\On$ is superinductive class under the successor mapping.
Hence by definition $\On$ is a minimally superinductive under the successor mapping.
{{qed|lemma}}
It remains to prove uniqueness.
Suppose $\On'$ is another minimally superinductive class under the successor mapping.
Then we have:
:$\On' \subseteq \On$
but also we have:
:$\On \subseteq \On'$
and so:
:$\On' = \On$
Thus $\On$ is the unique minimally superinductive class under the successor mapping.
{{qed}}
Theorem: Properties of Class of All Ordinals/Zero is Ordinal

The natural number $0$ is an element of $\On$.

Proof:
We have the result that Class of All Ordinals is Minimally Superinductive over Successor Mapping.
Hence $\On$ is {{afortiori}} a superinductive class {{WRT}} the successor mapping.
Hence, by definition of superinductive class:
:$\O \in \On$
We identify the natural number $0$ via the von Neumann construction of the natural numbers as:
:$0 := \O$
and the result follows.
{{qed}}
Theorem: Properties of Class of All Ordinals/Union of Chain of Ordinals is Ordinal

Let $C$ be a chain of elements of $\On$.
Then its union $\bigcup C$ is also an element of $\On$.

Proof:
We have the result that Class of All Ordinals is Minimally Superinductive over Successor Mapping.
Hence $\On$ is {{afortiori}} a superinductive class {{WRT}} the successor mapping.
Hence, by definition of superinductive class:
:$\On$ is closed under chain unions.
That is:
:$\forall C \in \On: \bigcup C \in \On$
where:
:$C$ is a chain of elements of $\On$
:$\bigcup C$ is the union of $C$.
{{qed}}
Theorem: Properties of Class of All Ordinals/Superinduction Principle

Let $A$ be a class which satisfies the following $3$ conditions:
{{begin-axiom}}
{{axiom | n = 1
        | lc= $A$ contains the zero ordinal $0$:
        | q = 
        | m = 0 \in A
}}
{{axiom | n = 2
        | lc= $A$ is closed under successor mapping:
        | q = \forall \alpha
        | m = \paren {\alpha \in A \implies \alpha^+ \in A}
}}
{{axiom | n = 3
        | lc= $A$ is closed under chain unions:
        | q = \forall C
        | m = \bigcup C \in A
        | rc= where $C$ is a chain of elements of $A$
}}
{{end-axiom}}
That is, let $A$ be a superinductive class under the successor mapping.
Then $A$ contains all ordinals:
:$\On \subseteq A$

Proof:
We note that the zero ordinal, denoted $0$, is identified as the empty set:
:$0 \:= \O$
Hence by definition $A$ is indeed a superinductive class under the successor mapping.
By the definition of ordinal:
:$\alpha$ is an '''ordinal''' {{iff}} $\alpha$ is an element of every superinductive class.
Hence $\On$ is a subclass of every superinductive class.
The result follows.
{{qed}}
Theorem: Class of All Ordinals is G-Tower

Let $\On$ denote the class of all ordinals.
Let $g$ be the successor mapping:
:$\forall x \in \On: \map g x = x \cup \set x$
Then $\On$ is a $g$-tower.

Proof:
From Successor Mapping is Progressing, $g$ is a progressing mapping.
From Class of All Ordinals is Minimally Superinductive over Successor Mapping, $\On$ is superinductive over $g$.
Hence the result by definition of $g$-tower.
{{qed}}
Category:G-Towers
Category:Class of All Ordinals
42w18hcsmtascq5stlvt4kp9n3i9fq5
Theorem: Natural Number is Ordinal

Let $n \in \N$ be a natural number.
Then $n$ is an ordinal.

Proof:
From the von Neumann construction of the natural numbers, $\N$ is identified with the minimally inductive set $\omega$.
From Superinductive Class under Successor Mapping contains All Ordinals, it follows by the Principle of Mathematical Induction that every natural number is an ordinal.
{{qed}}
Theorem: Zero is Smallest Ordinal

The natural number $0$ is the smallest ordinal.

Proof:
Let $\On$ denote the class of all ordinals.
By Zero is Ordinal, $0$ is an element of $\On$.
We identify the natural number $0$ via the von Neumann construction of the natural numbers as:
:$0 := \O$
By Empty Class is Subclass of All Classes:
:$\forall \alpha \in \On: \O \subseteq \alpha$
Hence the result by definition of smallest element.
{{qed}}
Category:Ordinals
Category:Zero
a3miqc3n95jw76xpabehol0nyrdv538
Theorem: Empty Set is Ordinary

The empty set is an ordinary set:
:$\O \notin \O$

Proof:
By definition:
:$\forall x: x \notin \O$
and so in particular:
:$\O \notin \O$
Hence the result.
{{qed}}
Category:Empty Set
Category:Ordinary Sets
rgi3smowkehxpv2nnbxd3ahvbwl0v2m
Theorem: Successor Set of Ordinary Transitive Set is Ordinary

Let $x$ be a transitive set which is also ordinary.
Let $x^+$ denote the successor set of $x$:
:$x^+ = x \cup \set x$
Then $x^+$ is also an ordinary set.

Proof:
By definition of ordinary set:
:$x \notin x$
{{AimForCont}} $x^+ \in x^+$.
Then we have:
{{begin-eqn}}
{{eqn | l = x^+
      | r = x \cup \set x
      | c = {{Defof|Successor Set}}
}}
{{eqn | ll= \leadsto
      | l = x^+
      | r = x
      | c = {{Defof|Set Union}}
}}
{{eqn | lo= \lor
      | l = x^+
      | o = \in
      | r = x
      | c = 
}}
{{end-eqn}}
;Let $x^+ \in x$
We have that $x$ is transitive.
Hence:
:$x^+ \subseteq x$
;Let $x^+ = x$
We have that:
$x^+ = x \cup \set x$
Hence by definition of union of set of sets:
:$x^+ \subseteq x$
Hence by Proof by Cases:
:$x^+ \subseteq x$
But we have:
:$x \in x^+$
and because $x^+ \subseteq x$ it follows that:
:$x \in x$
But this contradicts our supposition that $x \notin x$.
Hence by Proof by Counterexample:
:$x^+ \notin x^+$
{{qed}}