avewright/proofwiki-math huggingface dataset:
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 {a \circ b}^{-1}
      | r = e
      | c = {{Defof|Inverse Element}}
}}
{{eqn | ll= \leadsto
      | l = a \circ \paren {b \circ \paren {a \circ b}^{-1} }
      | r = e
      | c = {{Group-axiom|1}}
}}
{{eqn | ll= \leadsto
      | l = b \circ \paren {a \circ b}^{-1}
      | r = a^{-1}
      | c = Group Product Identity therefore Inverses
}}
{{eqn | ll= \leadsto
      | l = b^{-1} \circ \paren {b \circ \paren {a \circ b}^{-1} }
      | r = b^{-1} \circ a^{-1}
      | c = {{Group-axiom|3}}
}}
{{eqn | ll= \leadsto
      | l = \paren{b^{-1} \circ b} \circ \paren {a \circ b}^{-1}
      | r = b^{-1} \circ a^{-1}
      | c = {{Group-axiom|1}}
}}
{{eqn | ll= \leadsto
      | l = e \circ \paren {a \circ b}^{-1}
      | r = b^{-1} \circ a^{-1}
      | c = {{Defof|Inverse Element}}
}}
{{eqn | ll= \leadsto
      | l = \paren {a \circ b}^{-1}
      | r = b^{-1} \circ a^{-1}
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
{{Qed}}
Theorem: Inverse of Group Product/General Result

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $a_1, a_2, \ldots, a_n \in G$, with inverses $a_1^{-1}, a_2^{-1}, \ldots, a_n^{-1}$.
Then:
:$\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:
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/General Result

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $a_1, a_2, \ldots, a_n \in G$, with inverses $a_1^{-1}, a_2^{-1}, \ldots, a_n^{-1}$.
Then:
:$\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}$
=== 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: Well-Ordered Transitive Subset is Equal or Equal to Initial Segment

Let $\struct {\prec, A}$ be a well-ordered set.
For every $x \in A$, let every $\prec$-initial segment $A_x$ be a set.
Let $B$ be a subclass of $A$ such that
:$\forall x \in A: \forall y \in B: \paren {x \prec y \implies x \in B}$.
That is, $B$ must be $\prec$-transitive.
Then:
:$A = B$
or:
:$\exists x \in A: B = A_x$

Proof:
Let $A \ne B$.
Then $B \subsetneq A$.
Therefore:
{{begin-eqn}}
{{eqn | l = A \setminus B
      | o = \ne
      | r = \O
      | c = Set Difference with Proper Subset
}}
{{eqn | ll= \leadsto
      | q = \exists x \in A \setminus B
      | l = \paren {A \setminus B} \cap A_x
      | r = \O
      | c = Proper Well-Ordering Determines Smallest Elements
}}
{{eqn | ll= \leadsto
      | q = \exists x \in A \setminus B
      | l = A \cap A_x
      | o = \subseteq
      | r = B
      | c = Set Difference with Superset is Empty Set
}}
{{end-eqn}}
One direction of inclusion is proven.
By the hypothesis:
{{begin-eqn}}
{{eqn | l = x \in A \land x \prec y \land y \in B
      | o = \implies
      | r = x \in B
}}
{{end-eqn}}
But $x \in A \land x \notin B$, so:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = B
}}
{{eqn | ll= \leadsto
      | l = \neg x
      | o = \prec
      | r = y
      | c = Modus Tollendo Tollens and other propositional manipulations
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \prec
      | r = x
      | c = $\prec$ is totally ordered and $y \ne x$
}}
{{end-eqn}}
Therefore:
:$B \subseteq A_x$
and so 
:$B \subseteq A \cap A_x$
{{qed}}
Theorem: Inverse of Inverse/General Algebraic Structure

Let $\struct {S, \circ}$ be an algebraic structure with an identity element $e$.
Let $x \in S$ be invertible, and let $y$ be an inverse of $x$.
Then $x$ is also an inverse of $y$.

Proof:
Let $x \in S$ be invertible, where $y$ is an inverse of $x$.
Then:
:$x \circ y = e = y \circ x$
by definition.
{{qed}}
Theorem: Inverse of Group Inverse

Let $\struct {G, \circ}$ be a group.
Let $g \in G$, with inverse $g^{-1}$.
Then:
:$\paren {g^{-1} }^{-1} = g$

Proof:
Let $g \in G$.
Then:
{{begin-eqn}}
{{eqn | l = g
      | o = \in
      | r = G
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e
      | r = g^{-1} \circ g
      | c = {{Defof|Inverse Element}}
}}
{{eqn | ll= \leadsto
      | l = \paren {g^{-1} }^{-1} \circ e
      | r = \paren {g^{-1} }^{-1} \circ \paren {g^{-1} \circ g}
      | c =
}}
{{eqn | ll= \leadsto
      | l = \paren {g^{-1} }^{-1} \circ e
      | r = \paren {\paren {g^{-1} }^{-1} \circ g^{-1} } \circ g
      | c = {{Defof|Associative Operation}}
}}
{{eqn | ll= \leadsto
      | l = \paren {g^{-1} }^{-1} \circ e
      | r = e \circ g
      | c = {{Defof|Inverse Element}}
}}
{{eqn | ll= \leadsto
      | l = \paren {g^{-1} }^{-1}
      | r = g
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse of Group Inverse

Let $\struct {G, \circ}$ be a group.
Let $g \in G$, with inverse $g^{-1}$.
Then:
:$\paren {g^{-1} }^{-1} = g$

Proof:
Let $g \in G$.
Then:
{{begin-eqn}}
{{eqn | l = g g^{-1}
      | r = e
      | c = {{Defof|Inverse Element}}
}}
{{eqn | ll= \leadsto
      | l = g
      | r = \paren {g^{-1} }^{-1}
      | c = Group Product Identity therefore Inverses
}}
{{end-eqn}}
{{qed}}
Theorem: Condition for Injective Mapping on Ordinals

Let $F$ be a mapping satisfying the following properties:
:$(1): \quad$ The domain of $F$ is $\On$, the class of all ordinals
:$(2): \quad$ For all ordinals $x$, $\map F x = \map G {F \restriction x}$
:$(3): \quad$ For all ordinals $x$, $\map G {F \restriction x} \in \paren {A \setminus \Img x}$ where $\Img x$ is the image of $x$ under $F$.
Let $\Img F$ denote the image of $F$.
Then the following properties hold:
:$(1): \quad \Img F \subseteq A$
:$(2): \quad F$ is injective
:$(3): \quad A$ is a proper class.
Note that only the third property of $F$ is the most important.
For any function $G$, a function $F$ can be constructed satisfying the first two using the First Principle of Transfinite Recursion.
{{explain|Exactly which of the above statements is the "third" is unclear. This statement needs to be made precise. It also needs to be explained. Also, it needs to be put in a separate section as it is peripheral to the statement of the theorem.}}

Proof:
{{NotZFC}}
Let $x$ be an ordinal.
Then $\map F x = \map G {F \restriction x}$ and $\map G {F \restriction x} \in A$ by hypothesis.
Therefore, $\map F x \in A$.
This satisfies the first statement.
Take two distinct ordinals $x$ and $y$.
{{WLOG}}, assume $x \in y$ (we are justified in this by Ordinal Membership is Trichotomy).
Then:
{{begin-eqn}}
{{eqn | l = x \in y
      | o = \leadsto
      | r = \map F x \in \Img y
}}
{{eqn | o = \leadsto
      | r = \map F x \in \Img y \land \map F y \notin \Img y
      | c = by hypothesis
}}
{{eqn | o = \leadsto
      | r = \map F x \ne \map F y
}}
{{end-eqn}}
Thus for distinct ordinals $x$ and $y$, $\map F x \ne \map F y$.
Therefore, $F$ is injective.
$F$ is injective and $F: \On \to A$.
Therefore, if $A$ is a set, then $\On$ is a set.
But by the Burali-Forti Paradox, this is impossible, so $A$ is not a set.
Therefore, $A$ is a proper class.
{{qed}}
Theorem: Power of Element/Semigroup

Let $\struct {S, \oplus}$ be a magma.
Let $a \in S$.
Let $n \in \N_{>0}$.
Let $\tuple {a_1, a_2, \ldots, a_n}$ be the ordered $n$-tuple defined by $a_k = a$ for each $k \in \N_n$.
Then:
:$\ds \bigoplus_{k \mathop = 1}^n a_k = \oplus^n a$
where:
:$\ds \bigoplus_{k \mathop = 1}^n a_k$ is the composite of $\tuple {a_1, a_2, \ldots, a_n}$ for $\oplus$
:$\oplus^n a$ is the $n$th power of $a$ under $\oplus$.

Proof:
The proof will proceed by the Principle of Mathematical Induction on $\N$.
Let $T$ be the set defined as:
:$\ds T := \set {n \in \N: \bigoplus_{k \mathop = 1}^n a_k = \oplus^n a}$
First, recall the definition of the composite of $\tuple {a_1, a_2, \ldots, a_n}$ for $\oplus$:
:$\ds \bigoplus_{k \mathop = 1}^n a_k = \begin{cases}
a: & n = 1 \\
\map {\oplus_m} {a_1, \ldots, a_m} \oplus a_{m + 1}: & n = m + 1
\end{cases}$
Secondly, recall the definition of the $n$th power of $a$ under $\oplus$:
:$\forall n \in \N_{>0}: \oplus^n a = \begin{cases}
a & : n = 1 \\
\paren {\oplus^m a} \oplus a & : n = m + 1
\end{cases}$
Theorem: Order Isomorphism between Ordinals and Proper Class

Let $\struct {A, \prec}$ be a strict well-ordering.
Let $A$ be a proper class.
Let the initial segment of $x$ be a set for every $x \in A$.
Then we may make the following definitions:
Set $G$ equal to the collection of ordered pairs $\tuple {x, y}$ such that:
:$y \in A \setminus \Img x$
:$\paren {A \setminus \Img x} \cap A_y = \O$
Use the First Principle of Transfinite Recursion to construct a mapping $F$ such that:
:The domain of $F$ is the class of all ordinals $\On$
:For all ordinals $x$, $\map F x = \map G {F {\restriction_x} }$
Then $F: \On \to A$ is an order isomorphism between $\struct {\On, \in}$ and $\struct {A, \prec}$.

Proof:
{{NotZFC}}
Theorem: Strict Well-Ordering Isomorphic to Unique Ordinal under Unique Mapping

Let $S$ be a set.
Let $\struct {S, \prec}$ be a strict well-ordering.
Then there exists a unique ordinal $x$ and unique mapping $f$ such that $f: x \to S$ is an order isomorphism.

Proof:
The existence of $x$ and $f$ follows from the Counting Theorem.
The uniqueness of $x$ follows from the Counting Theorem.
The uniqueness of $f$ follows from Order Isomorphism between Wosets is Unique.
{{qed}}
Theorem: Unique Isomorphism between Ordinal Subset and Unique Ordinal

Let $\On$ be the class of all ordinals.
Let $S \subset \On$ where $S$ is a set.
Then there exists a unique mapping $\phi$ and a unique ordinal $x$ such that $\phi : x \to S$ is an order isomorphism.

Proof:
Since $S \subset \On$, $\struct {S, \in}$ is a strict well-ordering.
{{explain|Link to result justifying this statement.}}
The result follows directly from Strict Well-Ordering Isomorphic to Unique Ordinal under Unique Mapping.
{{qed}}
Theorem: Initial Segment of Ordinals under Lexicographic Order

Let $\preccurlyeq_l$ denote the lexicographic order for the set $\paren {\On \times \On}$.
Let the ordinal number $1$ denote the successor of $\O$.
Then the initial segment of $\tuple {1, \O}$ with respect to the lexicographic order $\preccurlyeq_l$ is a proper class.
This initial segment shall be denoted $\paren {\On \times \On}_{\tuple {1, \O} }$.
{{explain|The connection between these two statements is not clear.}}

Proof:
Define the mapping $F: \On \to \On \times \On$ as:
:$\forall x \in \On: \map F x = \tuple {\O, x}$
Then, $F: \On \to \paren {\On \times \On}_{\tuple {1, \O} }$, since $\O < 1$.
{{explain|The above statement does not make linguistic sense. The entity $F: \On \to \paren {\On \times \On}_{\tuple {1, \O} }$ is a noun, and there is no verb in the "then" clause.}}
That is, $F$ is a mapping from the class of all ordinals to the initial segment of $\tuple {1, \O}$ with respect to lexicographic order.
By Equality of Ordered Pairs, $F$ is injective.
But since $\On$ is a proper class by the Burali-Forti Paradox, the initial segment of $\tuple {1, \O}$ is a proper class as well.
{{qed}}
Theorem: Canonical Order Well-Orders Ordered Pairs of Ordinals

The canonical order, $R_0$ strictly well-orders the ordered pairs of ordinal numbers.

Proof:
=== Strict Ordering ===
Let $\tuple {x, y} \mathrel {R_0} \tuple {x, y}$.
Then:
:$\map \max {x, y} < \map \max {x, y} \lor \tuple {x, y} \mathrel {\operatorname {Le} } \tuple {x, y}$
{{explain|Where is the construct $\operatorname{Le}$ defined, and why can $\le$ not be used instead?}}
Both lead to contradictions, so:
:$\neg \tuple {x, y} \mathrel {R_0} \tuple {x, y}$
and $R_0$ is antireflexive.
{{qed|lemma}}
Let:
:$(1): \quad \tuple {\alpha, \beta} \mathrel {R_0} \tuple {\gamma, \delta}$
and:
:$(2): \quad \tuple {\gamma, \delta} \mathrel {R_0} \tuple {\epsilon, \zeta}$
There are two cases:
:$\map \max {\alpha, \beta} < \map \max {\gamma, \delta}$
or:
:$\map \max {\alpha, \beta} = \map \max {\gamma, \delta}$
{{begin-eqn}}
{{eqn | l = \map \max {\alpha, \beta} < \map \max {\gamma, \delta}
      | o = \leadsto
      | r = \map \max {\alpha, \beta} < \map \max {\epsilon, \zeta}
      | c = from $(2): \quad \map \max {\gamma, \delta} \le \map \max {\epsilon, \zeta}$
}}
{{eqn | o = \leadsto
      | r = \tuple {\alpha, \beta} \mathrel {R_0} \tuple {\epsilon, \zeta}
      | c = {{Defof|Canonical Order}}
}}
{{end-eqn}}
{{explain|Where does it follow that $\map \max {\gamma, \delta} \le \map \max {\epsilon, \zeta}$? All we have to work on is the relation $R_0$.}}
{{begin-eqn}}
{{eqn | l = \map \max {\alpha, \beta} = \map \max {\gamma, \delta}
      | o = \leadsto
      | r = \tuple {\alpha, \beta} \mathrel {\operatorname {Le} } \tuple {\gamma, \delta}
}}
{{eqn | o = \leadsto
      | r = \map \max {\alpha, \beta} < \max \map {\epsilon, \zeta} \lor \tuple {\alpha, \beta} \mathrel {\operatorname {Le} } \tuple {\epsilon, \zeta}
      | c = Transitivity of $\operatorname{Le}$
}}
{{eqn | o = \leadsto
      | r = \tuple {\alpha, \beta} \mathrel {R_0} \tuple {\epsilon, \zeta}
      | c = {{Defof|Canonical Order}}
}}
{{end-eqn}}
In either case:
:$\tuple {\alpha, \beta} \mathrel {R_0} \tuple {\epsilon, \zeta}$
and $R_0$ is transitive.
{{qed|lemma}}
Theorem: Initial Segment of Canonical Order is Set

Let $R_0$ denote the canonical ordering of $\paren {\On \times \On}$.
Then, for all $\tuple {x, y} \in \paren {\On \times \On}$, the $R_0$-initial segment is a set.
{{explain|The $R_0$-initial segment of what?}}

Proof:
Let $z = \map \max {x, y}^+$.
Let $\tuple {v, w} \mathrel R_0 \tuple {x, y}$.
Then:
{{begin-eqn}}
{{eqn | l = \map \max {v, w}
      | o = \le
      | r = \map \max {x, y}
}}
{{eqn | o = \lt
      | r = z
}}
{{end-eqn}}
Thus, the initial segment:
: $\paren {\On \times \On}_{\tuple {x, y} } \subseteq \paren {z \times z}$
{{explain|Clarify the sentence flow of the above statement.}}
By Axiom of Subsets Equivalents, the initial segment of $\tuple {x, y}$ is a set.
{{qed}}
Theorem: Ordinal Addition is Closed

Let $\On$ be the class of all ordinals.
Then:
:$\forall x, y \in \On: x + y \in \On$
That is: the sum $x+y$ is an ordinal.

Proof:
Using Transfinite Induction on $y$:
Theorem: Ordinal Addition by Zero

Let $x$ be an ordinal.
Let $\O$ be the zero ordinal.
Then:
:$x + \O = x = \O + x$
where $+$ denotes ordinal addition.

Proof:
By definition of ordinal addition, it is immediate that:
:$x + \O = x$
{{qed|lemma}}
We shall use Transfinite Induction on $x$ to prove $\O + x = x$
Theorem: Limit Ordinal Equals its Union

Let $\lambda$ be a limit ordinal.
Then:
:$\lambda = \bigcup \lambda$
where $\bigcup \lambda$ denotes the union of $\lambda$.

Proof:
From Union of Ordinal is Subset of Itself:
:$\bigcup \lambda \subseteq \lambda$
Suppose $x \in \lambda$.
By Successor of Ordinal Smaller than Limit Ordinal is also Smaller:
:$x^+ < \lambda$
and so:
:$x \in x^+$ and $x^+ \in \lambda$
from which:
:$x \in \bigcup \lambda$
That is:
:$\lambda \subseteq \bigcup \lambda$
Hence by set equality:
:$\lambda = \bigcup \lambda$
{{qed}}
Theorem: Substitutivity of Equality

Let $x$ and $y$ be sets.
Let $\map P x$ be a well-formed formula of the language of set theory.
Let $\map P y$ be the same proposition $\map P x$ with some (not necessarily all) free instances of $x$ replaced with free instances of $y$.
Let $=$ denote set equality.
:$x = y \implies \paren {\map P x \iff \map P y}$

Proof:
By induction on the well-formed parts of $\map P x$.
The proof shall use $\implies$ and $\neg$ as the primitive connectives.
Theorem: Membership is Left Compatible with Ordinal Addition

Let $x$, $y$, and $z$ be ordinals.
Let $<$ denote membership relation $\in$, since $\in$ is a strict well-ordering on the ordinals.
Then:
:$x < y \implies \paren {z + x} < \paren {z + y}$

Proof:
The proof proceeds by transfinite induction on $y$.
In the proof, we shall use $\in$, $\subsetneq$, and $<$ interchangeably.
We are justified in this by Transitive Set is Proper Subset of Ordinal iff Element of Ordinal.
Theorem: Ordinal Addition is Left Cancellable

Let $x, y, z$ be ordinals.
Then:
:$\paren {z + x} = \paren {z + y} \implies x = y$
That is, ordinal addition is left cancellable.

Proof:
For the proof, $<$, $\in$, and $\subsetneq$ will be used interchangeably.
This is justified by Transitive Set is Proper Subset of Ordinal iff Element of Ordinal.
Note that:
{{begin-eqn}}
{{eqn | l = x < y
      | o = \implies
      | r = \paren {z + x} < \paren {z + y}
      | c = Membership is Left Compatible with Ordinal Addition
}}
{{eqn | l = y < x
      | o = \implies
      | r = \paren {z + y} < \paren {z + x}
      | c = Membership is Left Compatible with Ordinal Addition
}}
{{end-eqn}}
However:
{{begin-eqn}}
{{eqn | l = \paren {z + x} = \paren {z + y}
      | o = \implies
      | r = \paren {z + x} \not < \paren {z + y} \land \paren {z + y} \not < \paren {z + x}
      | c = No Membership Loops
}}
{{end-eqn}}
This contradicts the consequents of the first two equations, so:
{{begin-eqn}}
{{eqn | o = \implies
      | r = x \not < y \land y \not < x
      | c = Rule of Transposition
}}
{{eqn | o = \implies
      | r = x = y
      | c = Ordinal Membership is Trichotomy
}}
{{end-eqn}}
{{qed}}
Theorem: Supremum Inequality for Ordinals

Let $A \subseteq \On$ and $B \subseteq \On$ be ordinals.
Then:
:$\ds \forall x \in A: \exists y \in B: x \le y \implies \bigcup A \le \bigcup B$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = <
      | r = \bigcup A
}}
{{eqn | ll= \leadsto
      | q = \exists z
      | l = x
      | o = <
      | r = z
      | c = {{Defof|Set Union}}
}}
{{eqn | lo= \land
      | l = z < A
      | o = <
      | r = A
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists y \in B: \exists z
      | l = x
      | o = <
      | r = z
      | c = {{hypothesis}}
}}
{{eqn | lo= \land
      | l = z
      | o = \le
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists y \in B
      | l = x
      | o = <
      | r = y
}}
{{eqn | ll= \leadsto
      | l = x
      | o = <
      | r = \bigcup B
      | c = Union of Ordinals is Least Upper Bound
}}
{{end-eqn}}
Therefore:
:$\ds \bigcup A \subseteq \bigcup B$
and:
:$\ds \bigcup A \le \bigcup B$
{{qed}}
Theorem: Subset is Right Compatible with Ordinal Addition

Let $x, y, z$ be ordinals.
Then:
:$x \le y \implies \paren {x + z} \le \paren {y + z}$

Proof:
The proof proceeds by transfinite induction on $z$.
Theorem: Ordinal Subtraction when Possible is Unique

Let $x$ and $y$ be ordinals such that $x \le y$.
Then there exists a unique ordinal $z$ such that $x + z = y$.
That is:
:$x \le y \implies \exists! z \in \On: x + z = y$

Proof:
By transfinite induction on $y$.
Theorem: Equality of Successors

Let $x$ and $y$ be ordinals.
Let $x^+$ denote the successor set of $x$.
Then, $x = y \iff x^+ = y^+$

Proof:
{{begin-eqn}}
{{eqn | l = x = y 
      | o = \leadsto
      | r = x^+ = y^+ 
      | c = Substitutivity of Equality
}}
{{end-eqn}}
Conversely,
{{begin-eqn}}
{{eqn | l = x^+ = y^+
      | o = \leadsto
      | r = \bigcup x^+ = \bigcup y^+
      | c = Substitutivity of Equality
}}
{{eqn | o = \leadsto
      | r = x = y
      | c = Union of Successor Ordinal
}}
{{end-eqn}}
{{qed}}
Theorem: Finite Ordinal Plus Transfinite Ordinal

Let $n$ be a finite ordinal.
Let $x$ be a transfinite ordinal.
Then:
: $n + x = x$

Proof:
By Transfinite Induction on $x$.
The proof will use $<$, $\in$, and $\subset$ interchangeably.  This is justified by Transitive Set is Proper Subset of Ordinal iff Element of Ordinal.
Theorem: Class is Transitive iff Union is Subclass

A class $A$ is transitive {{iff}}:
:$\bigcup A \subseteq A$

Proof:
=== Necessary Condition ===
{{:Class is Transitive iff Union is Subclass/Necessary Condition}}{{qed|lemma}}
Theorem: Union of Successor Ordinal

Let $x$ be an ordinal.
Let $x^+$ denote the successor of $x$.
Then:
:$\map \bigcup {x^+} = x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \bigcup {x^+}
      | r = \map \bigcup {x \cup \set x}
      | c = {{Defof|Successor Set}}
}}
{{eqn | r = \paren {\bigcup x \cup \bigcup \set x}
      | c = Set Union is Self-Distributive/Sets of Sets
}}
{{eqn | r = \paren {\bigcup x \cup x}
      | c = Union of Singleton
}}
{{eqn | r = x
      | c = Class is Transitive iff Union is Subclass
}}
{{end-eqn}}
{{qed}}
Category:Ordinals
66mq1rwlwhqxscky31pwnnw5qbbbjtb
Theorem: Set Union is Self-Distributive

Set union is self-distributive:
:$\forall A, B, C: \paren {A \cup B} \cup \paren {A \cup C} = A \cup B \cup C = \paren {A \cup C} \cup \paren {B \cup C}$
where $A, B, C$ are sets.

Proof:
We have:
* Union is Associative
* Union is Commutative
* Set Union is Idempotent
The result follows from Associative Commutative Idempotent Operation is Self-Distributive.
{{qed}}
Category:Set Union
Category:Examples of Self-Distributive Operations
Category:Set Union is Self-Distributive
lmqzsopzfpajvmeihd58p06yoombkpd
Theorem: Subset of Empty Set

Let $A$ be a class.
Then:
:$A$ is a subset of the empty set $\O$
{{iff}}:
:$A$ is equal to the empty set:
:$A \subseteq \O \iff A = \O$

Proof:
{{begin-eqn}}
{{eqn | l = A = \O
      | o = \leadsto
      | r = A \subseteq \O
      | c = {{Defof|Set Equality|index = 2}}
}}
{{end-eqn}}
Conversely:
{{begin-eqn}}
{{eqn | l = A \subseteq \O
      | o = \leadsto
      | r = A \subseteq \O \land \O \subseteq A
      | c = Empty Set is Subset of All Sets
}}
{{eqn | o = \leadsto
      | r = A = \O
      | c = {{Defof|Set Equality|index = 2}}
}}
{{end-eqn}}
{{qed}}
Category:Empty Set
ny8ucuzffhtv221wbn31hy0ecijskbo