avewright/proofwiki-math huggingface dataset:
Theorem: Signum Function on Integers is Extension of Signum on Natural Numbers

Let $\sgn_\Z: \Z \to \set {-1, 0, 1}$ be the signum function on the integers.
Let $\sgn_\N: \N \to \set {0, 1}$ be the signum function on the natural numbers.
Then $\sgn_\Z: \Z \to \Z$ is an extension of $\sgn_\N: \N \to \N$.

Proof:
Let $n \in \Z: n \ge 0$.
Then by definition of the signum function:
:$\map {\sgn_\Z} n = \begin {cases} 0 & : n = 0 \\ 1 & : n > 0 \end {cases}$
So by definition of the signum function on the natural numbers:
:$\forall n \in \N: \map {\sgn_\Z} n = \map {\sgn_\N} n$
Hence the result, by definition of extension.
{{qed}}
Category:Number Theory
1fee7396mz20grb6ycct0hlcaubyj8u
Theorem: Cartesian Product is Small iff Inverse is Small

Let $A$ and $B$ be classes.
Then the Cartesian product $A \times B$ is a small class {{iff}} $B \times A$ is small.

Proof:
{{begin-eqn}}
{{eqn | l = A \times B
      | r = \set {\tuple {x, y} : x \in A \land y \in B}
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | r = \set {\tuple {y, x} : x \in A \land y \in B}^{-1}
      | c = {{Defof|Inverse Relation}}
}}
{{eqn | r = \paren {B \times A}^{-1}
      | c = {{Defof|Cartesian Product}}
}}
{{end-eqn}}
Let $B \times A$ be a small class.
Then, by Inverse of Small Relation is Small, $A \times B$ is also small.
Similarly, let $A \times B$ be small.
Then, by Inverse of Small Relation is Small, $B \times A$ is also small.
{{qed}}
Theorem: Cartesian Product with Proper Class is Proper Class

Let $A$ be a proper class.
Let $B$ be a class which is not empty.
Then the Cartesian product $\paren {A \times B}$ is a proper class.

Proof:
{{NotZFC}}
{{AimForCont}} that $\paren {A \times B}$ is small.
By Domain of Small Relation is Small, the domain of $\paren {A \times B}$ is small.
Since $B \ne \O$, Nonempty Class has Members shows that $\exists y: y \in B$.
The domain of $\paren {A \times B}$ is the collection of all $x \in A$ such that $\exists y: y \in B$.
The domain of $\paren {A \times B}$ is $A$.
Therefore, $A$ is small, contradicting the fact that it is a proper class.
{{qed}}
Theorem: Uniqueness Condition for Relation Value

Let $\RR$ be a relation.
Let $\tuple {x, y} \in \RR$.
Let:
:$\exists ! y: \tuple {x, y} \in \RR$
Then:
:$\map \RR x = y$
where $\map \RR x$ denotes the image of $\RR$ at $x$.
If $y$ is not unique, then:
:$\map \RR x = \O$

Proof:
{{begin-eqn}}
{{eqn | n = 1
      | l = z \in \map \RR x
      | o = \implies
      | r = \exists y: \paren {z \in y \land \tuple {x, y} \in \RR} \land \exists ! y: \tuple {x, y} \in \RR
      | c = {{Defof|Image (Set Theory)/Relation/Element/Singleton|Image of Element under Relation}}
}}
{{eqn | o = \implies
      | r = \forall w: \paren {\tuple {x, w} \in \RR \iff w = y}
      | c = {{Defof|Unique}} and {{hypothesis}} that $\tuple {x, y} \in \RR$
}}
{{eqn | o = \implies
      | r = z \in w \land \tuple {x, w} \in \RR
      | c = Existential Instantiation from $(1)$
}}
{{eqn | o = \implies
      | r = z \in y
      | c = Substitutivity of Equality from $z \in w \land w = y$
}}
{{end-eqn}}
Conversely:
{{begin-eqn}}
{{eqn | l = z \in y
      | o = \implies
      | r = \paren {z \in y \land \tuple {x, y} \in \RR}
      | c = {{hypothesis}} that $\tuple {x, y} \in \RR$
}}
{{eqn | o = 
      | r = \exists ! y: \tuple {x, y} \in \RR
      | c = {{hypothesis}}
}}
{{eqn | o = \implies
      | r = z \in \map \RR x
      | c = {{Defof|Image (Set Theory)/Relation/Element/Singleton|Image of Element under relation}}
}}
{{end-eqn}}
Generalizing:
:$\forall z: \paren {z \in y \iff z \in \map \RR x}$
Therefore:
:$y = \map \RR x$
by the definition of class equality.
{{qed|lemma}}
Suppose that $\neg \exists ! y: \tuple {x, y} \in \RR$.
Then:
{{begin-eqn}}
{{eqn | l = \neg \exists ! y: \tuple {x, y} \in \RR
      | o = \implies
      | r = z \notin \map \RR x
      | c = {{Defof|Image (Set Theory)/Relation/Element/Singleton|Image of Element under relation}}
}}
{{end-eqn}}
Thus:
:$\forall z: z \notin \map \RR x$
Therefore:
:$\map \RR x = \O$
{{qed}}
Theorem: Value of Relation is Small

The value of a relation is always a small class.

Proof:
Let $\RR$ be an arbitrary relation.
Let $s$ be any set.
The value of a relation is either equal to some set $y$ or $\O$ by Uniqueness Condition for Relation Value.
If it is equal to some set $y$, then the value of $s$ under $\RR$ is a small class by the definition of small class.
If it is equal to $\O$, then the result follows from Empty Set is Small.
Theorem: Mapping whose Domain is Small Class is Small

Let $F$ be a mapping.
Let the domain of $F$ be a small class.
Then, $F$ is a small class.

Proof:
Let $A$ denote the domain of $F$.
Let $B$ denote the image of $F$.
Since $F$ is a mapping, $F$ is also a relation. 
Therefore:
:$F \subseteq A \times B$
where $A \times B$ denotes the Cartesian product of $A$ and $B$.
$B$ is the image of $A$ under $F$ and is therefore a small class by Image of Small Class under Mapping is Small.
Since $A$ and $B$ are both small, their Cartesian Product is Small.
By Axiom of Subsets Equivalents, it follows that $F$ is small.
Theorem: Restriction of Mapping to Small Class is Small

Let $F$ be a mapping.
Let $A$ be a small class.
Then the restriction $F {\restriction_A}$ is a small class.

Proof:
The domain of $F {\restriction_A}$ is a subset of $A$.
By Axiom of Subsets Equivalents, the domain is a small class.
By Mapping whose Domain is Small Class is Small, it follows that $F {\restriction_A}$ is a small class.
{{qed}}
Theorem: Preimage of Singleton

Let $\RR$ be a relation.
Let $\map {\RR^{-1} } t$ denote the preimage of $t$ under $\RR$.
Let $\RR^{-1} \sqbrk {\set t}$ denote the preimage of $\set t$ under $\RR$.
Then:
:$\RR^{-1} \sqbrk {\set t} = \map {\RR^{-1} } t$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\RR^{-1} } t
      | r = \set {s: \paren {s, t} \in \RR}
      | c = {{Defof|Preimage of Element under Relation}}
}}
{{eqn | r = \set {s: \exists y: \paren {y = t \land \tuple {s, y} \in \RR} }
      | c = Equality implies Substitution
}}
{{eqn | r = \set {s: \exists y \in \set t: \tuple {s, y} \in \RR}
      | c = {{Defof|Singleton}}
}}
{{eqn | r = \RR^{-1} \sqbrk {\set t}
      | c = {{Defof|Preimage of Subset under Relation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Order Isomorphism Preserves Strictly Minimal Elements

Let $A_1$ and $A_2$ be classes.
Let $\prec_1$ and $\prec_2$ be relations.
Let $\phi : A_1 \to A_2$ create an order isomorphism between $\struct {A_1, \prec_1}$ and $\struct {A_1, \prec_2}$.
Let $B \subseteq A_1$.
Then $\phi$ maps the strictly minimal elements under $\prec_1$ of $B$ to the strictly minimal elements under $\prec_2$  of $\phi \sqbrk B$.

Proof:
Suppose $x$ is a strictly minimal element of $B$.  That is:
:$\neg \exists y \in B: x \prec_1 y$
This is equivalent to the statement:
:$\neg \exists z \in \phi \sqbrk B: \map \phi x \prec_2 z$ since $z$ is of the form $\map \phi y$ by the definition of order isomorphism.
{{handwaving|Too much corners cut}}
Thus, this statement is true {{iff}} $\map \phi x$ is a strictly minimal element of $B$.
Theorem: Order Isomorphism Preserves Initial Segments

Let $A_1$ and $A_2$ be classes.
Let $\prec_1$ and $\prec_2$ be strict orderings.
Let $\phi: A_1 \to A_2$ create an order isomorphism between $\struct {A_1, \prec_1}$ and $\struct {A_2, \prec_2}$.
Suppose $x \in A_1$.
Then $\phi$ maps the $\prec_1$-initial segment of $x$ to the $\prec_2$-initial segment of $\map \phi x$.

Proof:
$\phi$ maps the $\prec_1$-initial segment of $x$ to:
{{begin-eqn}}
{{eqn | l = \phi \sqbrk {\set {y \in A: y \prec_1 x} }
      | r = \phi \sqbrk {\set {y \in A: \map \phi y \prec_2 \map \phi x} }
      | c = {{Defof|Initial Segment}} and {{Defof|Order Isomorphism}}
}}
{{eqn | r = \set {\map \phi y \in \phi \sqbrk A: \map \phi y \prec_2 \map \phi x}
      | c = {{Defof|Order Isomorphism}} and {{Defof|Image of Subset under Mapping}}
}}
{{end-eqn}}
This is the $\prec_2$-initial segment of $\map \phi x$.
{{qed}}
Theorem: Order Isomorphism on Strictly Well-Founded Relation preserves Strictly Well-Founded Structure

Let $A_1$ and $A_2$ be classes.
Let $\prec_1$ and $\prec_2$ be relations.
Let $\phi: \struct {A_1, \prec_1} \to \struct {A_2, \prec_2}$ be an order isomorphism.
Then $\struct {A_1, \prec_1}$ is a strictly well-founded structure {{iff}} $\struct {A_2, \prec_2}$ is also a strictly well-founded structure.

Proof:
Take any nonempty subset $B \subseteq A_1$.
From Order Isomorphism Preserves Strictly Minimal Elements:
:$x$ is a strictly minimal element of $B$ {{iff}} $\map \phi x$ is a strictly minimal element of $\phi \sqbrk B$.
By the definition of strictly well-founded relation, $\struct {A_1, \prec_1}$ is strictly well-founded {{iff}} $\struct {A_2, \prec_2}$ is strictly well-founded.
{{qed}}
Theorem: Alternating Group is Set of Even Permutations

Let $S_n$ denote the symmetric group on $n$ letters.
Let $A_n$ be the alternating group on $n$ letters.
Then $A_n$ consists of the set of even permutations of $S_n$.

Proof:
Let $\sgn$ denote the sign of permutation on n Letters.
We have that $\map \sgn {S_n}$ is onto $C_2$.
Thus from the First Isomorphism Theorem, $A_n$ consists of the set of even permutations of $S_n$.
{{Qed}}
Theorem: Induced Relation Generates Order Isomorphism

Let $\struct {A_1, \preceq_1}$ be an ordered set.
Let $\phi: A_1 \to A_2$ be a bijection.
Let:
:$\preceq_2 \mathop{:=} \set {\tuple {\map \phi x, \map \phi y}: x \in A_1 \land y \in A_1 \land x \mathop{\preceq_1} y}$
Then $\phi: \struct {A_1, \preceq_1} \to \struct {A_2, \preceq_2}$ is an order isomorphism.

Proof:
Take any $x, y \in A_1$ such that $x \preceq_1 y$.
Since $x, y \in A_1$, it follows by the definition of a mapping that:
:$\map \phi x, \map \phi y \in A_2$
So $x \in A_1$ and $y \in A_1$ and $x \preceq_1 y$.
It follows from the definition of $\preceq_2$ that:
:$\map \phi x \preceq_2 \map \phi y$
Conversely, suppose that:
:$\map \phi x \preceq_2 \map \phi y$
By the definition of $\preceq_2$, it follows that:
:$x \preceq_1 y$
Therefore, the biconditional holds:
:$x \preceq_1 y \iff \map \phi x \preceq_2 \map \phi y$
By definition, it follows that:
:$\phi: \struct {A_1, \preceq_1} \to \struct {A_2, \preceq_2}$
is an order isomorphism.
{{qed}}
Theorem: Ordinal Multiplication is Left Distributive

Let $x$, $y$, and $z$ be ordinals.
Let $\times$ denote ordinal multiplication.
Let $+$ denote ordinal addition.
Then:
:$x \times \paren {y + z} = \paren {x \times y} + \paren {x \times z}$

Proof:
The proof shall proceed by Transfinite Induction, as follows:
Theorem: Ordinal Multiplication is Associative

Let $x, y, z$ be ordinals.
Let $\times$ denote ordinal multiplication.
Then:
:$x \times \paren {y \times z} = \paren {x \times y} \times z$

Proof:
The proof shall proceed by Transfinite Induction on $z$:
Theorem: Division Theorem for Ordinals

Let $x$ and $y$ be ordinals.
Let $0$ denote the zero ordinal.
Suppose $y \ne 0$.
Then there exist unique ordinals $z$ and $w$ such that:
:$x = \paren {y \times z} + w$ and $w < y$.

Proof:
=== Existence of $z$ and $w$ ===
First, it must be proven that such $z$ and $w$ exist.
By Relation between Two Ordinals, it follows that:
:$x < y$ or $y \le x$
The proof shall proceed by cases.
Theorem: Finite Ordinal Times Ordinal

Let $m$ and $n$ be finite ordinals.
Let $m \ne 0$, where $0$ is the zero ordinal.
Let $x$ be a limit ordinal.
Then:
:$m \times \paren {x + n} = x + \paren {m \times n}$
{{expand|Via Cantor normal form, all ordinals are of the form $x + n$}}

Proof:
=== Lemma ===
{{:Finite Ordinal Times Ordinal/Lemma}}{{qed|lemma}}
By Ordinal Multiplication is Left Distributive:
:$m \times \paren {x + n} = \paren {m \times x} + \paren {m \times n}$
It remains to prove that $x = m \times x$.
Since $x$ is a limit ordinal, it follows that:
{{begin-eqn}}
{{eqn | q = \exists y \in \On
      | l = x
      | r = \omega \times y
      | c = Factorization of Limit Ordinals
}}
{{eqn | l = m \times x
      | r = m \times \paren {\omega \times y}
      | c = Substitutivity of Class Equality
}}
{{eqn | l = m \times x
      | r = \paren {m \times \omega} \times y
      | c = Ordinal Multiplication is Associative
}}
{{eqn | r = \omega \times y
      | c = lemma
}}
{{end-eqn}}
{{qed}}
Theorem: Factorization of Limit Ordinals

Let $x$ be a limit ordinal.
Then:
:$x = \paren {\omega \times y}$ for some $y \in \On$
where $\omega$ is the minimally inductive set.

Proof:
By the Division Theorem for Ordinals:
:$x = \paren {\omega \times y} + z$
for some unique $y$ and $z \in \omega$.
{{AimForCont}} $z \ne 0$.
Because $z \in \omega$, $z$ is not a limit ordinal.
Therefore, by the definition of limit ordinal:
:$z = w^+$
for some $w \in \omega$.
But this means that:
{{begin-eqn}}
{{eqn | l = x 
      | r = \paren {\omega \times y} + w^+
      | c = Division Theorem for Ordinals
}}
{{eqn | l = 
      | r = \paren {\paren {\omega \times y} + w}^+
      | c = {{Defof|Ordinal Addition}}
}}
{{end-eqn}}
This means that $x$ is the successor of some ordinal.
Hence $x$ cannot be a limit ordinal.
But this contradicts the assumption that $x$ is a limit ordinal.
It follows that $z = 0$.
Therefore:
{{begin-eqn}}
{{eqn | l = x
      | r = \paren {\omega \times y} + z
      | c = Division Theorem for Ordinals
}}
{{eqn | r = \omega \times y
      | c = Ordinal Addition by Zero
}}
{{end-eqn}}
{{qed}}
Category:Ordinal Arithmetic
Category:Limit Ordinals
83dzw1awrktu0f2slev6xslxjnyrjub
Theorem: Ordinal Exponentiation is Closed

Let $x$ and $y$ be ordinals.
Then:
:$x^y \in \On$
That is, ordinal exponentiation is closed.

Proof:
Let $x = 0$ and $y = 0$.
Then by the definition of ordinal exponentiation:
:$x^y = 1$
Let $x = 0$ and $y \ne 0$.
Then by the definition of ordinal exponentiation:
:$x^y = 0$
In either case, $x^y$ is an ordinal.
Now suppose that $x \ne 0$.
The proof shall proceed by Transfinite Induction on $y$.
Theorem: Exponent Base of One

Let $x$ be an ordinal.
Then:
:$1^x = 1$

Proof:
The proof shall proceed by Transfinite Induction on $x$.
Theorem: Exponent Not Equal to Zero

Let $x$ and $y$ be ordinals.
Let $x \ne 0$.
Then:
:$x^y \ne 0$

Proof:
The proof shall proceed by Transfinite Induction on $y$.
Theorem: Membership is Left Compatible with Ordinal Exponentiation

Let $x$, $y$, and $z$ be ordinals.
Suppose $1 < z$.
Then:
:$x < y \iff z^x < z^y$

Proof:
=== Sufficient Condition ===
The proof shall proceed by Transfinite Induction on $y$.
Theorem: Conjugacy Action on Group Elements is Group Action

Let $\struct {G, \circ}$ be a group whose identity is $e$.
The conjugacy action on $G$:
: $\forall g, h \in G: g * h = g \circ h \circ g^{-1}$
is a  group action on itself.

Proof:
We have that:
:$e * x = e \circ x \circ e^{-1} = x$
and so {{GroupActionAxiom|2}} is fulfilled.
{{GroupActionAxiom|1}} is shown to be fulfilled thus:
{{begin-eqn}}
{{eqn | l = \paren {g_1 \circ g_2} * x
      | r = \paren {g_1 \circ g_2} \circ x \circ \paren {g_1 \circ g_2}^{-1}
      | c = Definition of $*$
}}
{{eqn | r = g_1 \circ g_2 \circ x \circ g_2^{-1} \circ g_1^{-1}
      | c = Inverse of Group Product
}}
{{eqn | r = g_1 * \paren {g_2 \circ x \circ g_2^{-1} }
      | c = Definition of $*$
}}
{{eqn | r = g_1 * \paren {g_2 * x}
      | c = Definition of $*$
}}
{{end-eqn}}
{{Qed}}
Theorem: Conjugacy Action on Group Elements is Group Action

Let $\struct {G, \circ}$ be a group whose identity is $e$.
The conjugacy action on $G$:
: $\forall g, h \in G: g * h = g \circ h \circ g^{-1}$
is a  group action on itself.

Proof:
Let $X$ be the set of all subgroups of $G$.
By definition, the (left) conjugacy action on subgroups is the group action $*_X : G \times X \to X$ defined as:
:$g *_X X = g \circ X \circ g^{-1}$
By Conjugacy Action on Subgroups is Group Action, the (left) conjugacy action on subgroups $*_X$ is a group action.
By Subset Product Action is Group Action, it follows that the conjugacy action $*: G \times G \to G$ such that:
{{explain|How this conclusion follows by Subset Product Action is Group Action?}}
:$\forall g, h \in G: g * h = g \circ h \circ g^{-1}$
is a group action, as required.
{{Qed}}
Theorem: Conjugacy Action on Subgroups is Group Action

Let $X$ be the set of all subgroups of $G$.
For any $H \le G$ and for any $g \in G$, the conjugacy action:
:$g * H := g \circ H \circ g^{-1}$
is a group action.

Proof:
Clearly {{GroupActionAxiom|1}} is fulfilled as $e * H = H$.
{{GroupActionAxiom|2}} is shown to be fulfilled thus:
{{begin-eqn}}
{{eqn | l = \paren {g_1 \circ g_2} * H
      | r = \paren {g_1 \circ g_2} \circ H \circ \paren {g_1 \circ g_2}^{-1}
      | c = Definition of $*$
}}
{{eqn | r = g_1 \circ g_2 \circ H \circ g_2^{-1} \circ g_1^{-1}
      | c = Inverse of Group Product
}}
{{eqn | r = g_1 * \paren {g_2 \circ H \circ g_2^{-1} }
      | c = Definition of $*$
}}
{{eqn | r = g_1 * \paren {g_2 * H}
      | c = Definition of $*$
}}
{{end-eqn}}
{{Qed}}
Theorem: Slice Category of Order Category

Let $\mathbf P$ be a order category, and denote its ordering by $\preceq$.
Let $p \in \mathbf P_0$ be an object of $\mathbf P$.
Then:
:$\mathbf P \mathbin / p \cong p^\preceq$
where:
:$\mathbf P \mathbin / p$ is the slice of $\mathbf P$ over $p$
:$p^\preceq$ is the order category defined by the weak lower closure of $p$.

Proof:
The objects of $\mathbf P \mathbin / p$ are morphisms $q \to p$ of $\mathbf P$.
The morphisms are $q \to r$ fitting into a commutative diagram:
$\quad\quad \begin{xy}\xymatrix@C=1em{
q
\ar[rr]
\ar[rd]
& &
r
\ar[ld]
\\ &
p
}\end{xy}$
Define a functor $U: \mathbf P \mathbin / p \to \mathbf P$ by:
:$U \left({q \to p}\right) := q$
:$U \left({q \to r}\right) := q \to r$
Because there is at most one morphism $q \to p$ for each $q$, $U$ is injective on objects.
That $U$ is faithful is trivial.
Hence by Functor is Embedding iff Faithful and Injective on Objects, $U$ is an embedding.
That is, $\mathbf P \mathbin / p$ is isomorphic to the image of $U$.
Now the objects of the image of $U$ in $\mathbf P$ are those $q$ such that $q \preceq p$.
That is, the image of $U$ has as objects $p^\preceq$.
By Commutative Diagram in Preorder Category, every morphism $q \to r$ in $p^\preceq$ fits into a commutative triangle as above.
Thus all morphisms of $p^\preceq$ are in the image of $U$, so that $p^\preceq$ is precisely the image of $U$.
Hence the result.
{{qed}}
Theorem: Category of Pointed Sets as Coslice Category

Let $\mathbf{Set}_*$ be the category of pointed sets.
Let $\mathbf{Set}$ be the category of sets.
Let $1 := \left\{{*}\right\}$ be any singleton.
Then:
:$\mathbf{Set}_* \cong 1 \mathbin / \mathbf{Set}$
where $1 \mathbin / \mathbf{Set}$ denotes the coslice of $\mathbf{Set}$ under $1$ and $\cong$ signifies isomorphic categories.

Proof:
Define the functor $F: \mathbf{Set}_* \to 1 \mathbin / \mathbf{Set}$ by:
:$\map F {C, c} := \bar c: 1 \to C$
:$F f := f$
where $\bar c: 1 \to C$ is defined by $\bar c (*) = c$.
Further, define $G: 1 \mathbin / \mathbf{Set} \to \mathbf{Set}_*$ by:
:$\map G {x: 1 \to C} := \struct {C, x \paren *}$
:$G f := f$
Theorem: Subset is Right Compatible with Ordinal Exponentiation

Let $x, y, z$ be ordinals.
Then:
:$x \le y \implies x^z \le y^z$

Proof:
The proof shall proceed by Transfinite Induction on $z$.
Theorem: Condition for Membership is Right Compatible with Ordinal Exponentiation

Let $x, y, z$ be ordinals.
Let $z$ be the successor of some ordinal $w$.
Then:
:$x < y \iff x^z < y^z$

Proof:
=== Sufficient Condition ===
Suppose $x < y$.
By Subset is Right Compatible with Ordinal Exponentiation:
:$x^w \le y^w$
Then:
{{begin-eqn}}
{{eqn | l = x^z
      | r = x^w \times x
      | c = {{Defof|Ordinal Exponentiation}}
}}
{{eqn | l = y^z
      | r = y^w \times y
      | c = {{Defof|Ordinal Exponentiation}}
}}
{{eqn | l = x^w \times x
      | o = \le
      | r = y^w \times x
      | c = Subset is Right Compatible with Ordinal Exponentiation
}}
{{eqn | l = 
      | o = <
      | r = y^w \times y
      | c = Membership is Left Compatible with Ordinal Exponentiation
}}
{{end-eqn}}
Thus the sufficient condition is satisfied.
{{qed|lemma}}
Theorem: Lower Bound for Ordinal Exponentiation

Let $x$ and $y$ be ordinals.
Let $x$ be greater than $1$, where $1$ denotes the successor of the zero ordinal.
Then:
:$y \le x^y$

Proof:
The proof shall proceed by Transfinite Induction on $y$.
Theorem: Unique Ordinal Exponentiation Inequality

Let $x$ and $y$ be ordinals.
Let $x > 1$ and $y > 0$.
Then there exists a unique ordinal $z$ such that:
:$x^z \le y$ and $y < x^{z^+}$

Proof:
=== Existence of $z$ ===
By Lower Bound for Ordinal Exponentiation, $y \le x^y$ so $y < x^{y^+}$.
Therefore, $y$ is bounded above by $x^w$ for some $w$, so there is a smallest $w$ such that:
:$y < x^w$ by Subset of Ordinals has Minimal Element.
Moreover, if $w$ is a limit ordinal then there is some $v ∈ w$ such that $y < x^v$, contradicting the fact that $w$ is minimal.
Therefore, $w$ is not a limit ordinal and therefore must be the successor of some ordinal.
So $w = z^+$ for some $z$.
Since $z < z^+$, it follows that $x^z ≤ y$ and $y < x^{z^+}$.
{{qed|lemma}}
Theorem: Limit Ordinals Closed under Ordinal Exponentiation

Let $x$ and $y$ be ordinals.
Let $y$ be a limit ordinal.
Let $x^y$ denote ordinal exponentiation.
Then:
:If $x > 1$, then $x^y$ is a limit ordinal.
:If $x \ne \O$, then $y^x$ is a limit ordinal.

Proof:
Suppose $x > 1$.
{{AimForCont}} also that $x^y$ is the successor of some ordinal $w$.
By definition of ordinal exponentiation:
:$\ds x^y = \bigcup_{z \mathop \in y} x^z$
Then:
{{begin-eqn}}
{{eqn | l = w
      | o = \in
      | r = x^y
      | c = Ordinal is Less than Successor
}}
{{eqn | ll= \leadsto
      | q = \exists z \in y
      | l = w
      | o = \in
      | r = x^z
      | c = {{Defof|Ordinal Exponentiation}}
}}
{{eqn | ll= \leadsto
      | l = w^+
      | o = \subseteq
      | r = x^z
      | c = Successor of Element of Ordinal is Subset
}}
{{eqn | o = \in
      | r = x^{z^+}
      | c = Membership is Left Compatible with Ordinal Exponentiation
}}
{{end-eqn}}
But $z^+ \in y$ by Successor of Ordinal Smaller than Limit Ordinal is also Smaller.
So $w^+ \in x^y$ and $w^+ \in w^+$.
This creates a membership loop and thus is a contradiction by No Membership Loops.
{{qed|lemma}}
For the second part, since $x$ is not the empty set it follows that $x = z^+$ for some $z$ or that $x$ is a limit ordinal.
If $x$ is a limit ordinal, then $y^x$ is a limit ordinal by the first part.
If $x$ is the successor of $z$, then:
:$y^x = y^w × y$ by the definition of ordinal exponentiation.
Then, $y^x$ is a limit ordinal by Limit Ordinals Preserved Under Ordinal Multiplication.
{{qed}}
Theorem: Successor of Element of Ordinal is Subset

Let $x$ and $y$ be ordinals.
Then:
:$x \in y \iff x^+ \subseteq y$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = y
      | c =
}}
{{eqn | ll= \leadstoandfrom
      | l = x^+
      | o = \in
      | r = y^+
      | c = Successor is Less than Successor
}}
{{eqn | ll= \leadstoandfrom
      | l = x^+
      | o = \in
      | r = y
      | c = {{Defof|Successor Set}}
}}
{{eqn | lo= \lor
      | l = x^+
      | r = y
      | c =
}}
{{eqn | ll= \leadstoandfrom
      | l = x^+
      | o = \subsetneq
      | r = y
      | c = Transitive Set is Proper Subset of Ordinal iff Element of Ordinal
}}
{{eqn | lo = \lor
      | l = x^+
      | r = y
      | c =
}}
{{eqn | ll= \leadstoandfrom
      | l = x^+
      | o = \subseteq
      | r = y
      | c =
}}
{{end-eqn}}
{{qed}}
Category:Ordinals
g64k6jmyvcxrd4nwqs85uv61dxds1w2
Theorem: Ordinal is Less than Ordinal to Limit Power

Let $x$, $y$, and $z$ be ordinals.
Let $z$ be a limit ordinal.
Then:
:$x < y^z \iff \exists w \in z: x < y^w$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x < y^z
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = x < \bigcup_{w \mathop \in z} y^w
      | c = {{Defof|Ordinal Exponentiation}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \exists w \in z: x < y^w 
      | c = {{Defof|Union of Family}}
}}
{{end-eqn}}
{{qed}}
Theorem: Ordinal Sum of Powers

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

Proof:
The proof shall proceed by Transfinite Induction on $z$.