avewright/proofwiki-math huggingface dataset:
Theorem: Preimage of Serial Relation is Domain

Let $\RR$ be a serial relation on $S$.
Then the preimage of $\RR$ is $S$ (the domain of $\RR$).

Proof:
{{begin-eqn}}
{{eqn | l = S
      | o = \supseteq
      | r = \Preimg \RR
      | c = {{Defof|Preimage of Relation}}
}}
{{eqn | q = \forall s \in S: \exists t \in S
      | l = \tuple {s, t}
      | o = \in
      | r = \RR
      | c = {{Defof|Serial Relation}}
}}
{{eqn | ll= \leadsto
      | q = \forall s \in S
      | l = s
      | o = \in
      | r = \Preimg \RR
      | c = {{Defof|Preimage of Relation}}
}}
{{eqn | ll= \leadsto
      | l = S
      | o = \subseteq
      | r = \Preimg \RR
      | c = {{Defof|Subset}}
}}
{{eqn | ll= \leadsto
      | l = S
      | r = \Preimg \RR
      | c = {{Defof|Set Equality|index = 2}}
}}
{{end-eqn}}
{{qed}}
Category:Serial Relations
8pdgtd2li0fjwodvz1et0obx9f12b2m
Theorem: Relation is Connected and Reflexive iff Total

Let $S$ be a set.
Let $\RR$ be a relation on $S$.
Then:
:$\RR$ is both a connected relation and a reflexive relation
{{iff}}:
:$\RR$ is a total relation.

Proof:
=== Necessary Condition ===
Let $\RR$ be a relation on $S$ which is both connected and reflexive.
Let $\tuple {a, b} \in S \times S$.
Suppose $a = b$.
Then as $\RR$ is reflexive, $\tuple {a, b} \in \RR$.
Suppose $a \ne b$.
Then as $\RR$ is connected, $\tuple {a, b} \in \RR \lor \tuple {b, a} \in \RR$.
That is:
:$\forall \tuple {a, b} \in S \times S: \tuple {a, b} \in \RR \lor \tuple {b, a} \in \RR$.
Thus $\RR$ is a total relation.
{{qed|lemma}}
Theorem: Total Ordering is Total Relation

Let $S$ be a set.
Let $\RR \subseteq S \times S$ be a total ordering.
Then $\RR$ is a total relation.

Proof:
By definition of total ordering:
:$\RR$ is a reflexive relation on the strength of being an ordering
:$\RR$ is a connected relation on the strength of being a total ordering.
{{qed}}
Category:Total Orderings
Category:Total Relations
ks8n1nv30vxvjpdtoogegijgsgy65gf
Theorem: Natural Number Addition Commutativity with Successor/Proof 2

Let $\N$ be the natural numbers.
Then:
:$\forall m, n \in \N_{> 0}: \left({m + 1}\right) + n = \left({m + n}\right) + 1$

Proof:
Using the following axioms:
{{:Axiom:Axiomatization of 1-Based Natural Numbers}}
Proof by induction:
From Axiomatization of $1$-Based Natural Numbers, we have by definition that:
{{begin-eqn}}
{{eqn | q = \forall m, n \in \N
      | l = m + 0
      | r = m
}}
{{eqn | l = \paren {m + n}^+
      | r = m + n^+
}}
{{end-eqn}}
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\forall m \in \N_{> 0}: \paren {m + 1} + n = \paren {m + n} + 1$
=== Basis for the Induction ===
When $n = 1$, we have:
:$\paren {m + 1} + 1 = \paren {m + 1} + 1$
which holds trivially.
Thus $\map P 1$ is seen to be true.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis $\map P k$:
:$\forall m \in \N: \paren {m + 1} + k = \paren {m + k} + 1$
Then we need to show that $\map P {k^+}$ follows directly from $\map P k$:
:$\forall m \in \N: \paren {m + 1} + \paren {k + 1} = \paren {m + \paren {k + 1} } + 1$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = \paren {m + \paren {k + 1} } + 1
      | r = \paren {\paren {m + k} + 1} + 1
      | c = Natural Number Addition is Associative/Proof 3
}}
{{eqn | r = \paren {\paren {m + 1} + k} + 1
      | c = Induction Hypothesis
}}
{{eqn | r = \paren {m + 1} + \paren {k + 1}
      | c = Natural Number Addition is Associative/Proof 3
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall m, n \in \N_{> 0}: \paren {m + 1} + n = \paren {m + n} + 1$
{{qed}}
Theorem: Natural Number Commutes with 1 under Addition

Let $n \in \N_{> 0}$ be a natural number.
Then $n$ commutes with $1$ under the operation of addition:
:$\forall n \in \N_{> 0}: n + 1 = 1 + n$

Proof:
Using the axiomatization:
{{:Axiom:Axiomatization of 1-Based Natural Numbers}}
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$n + 1 = 1 + n$
Theorem: Natural Number Addition is Commutative/Proof 3

The operation of addition on the set of natural numbers $\N_{> 0}$ is commutative:
:$\forall x, y \in \N_{> 0}: x + y = y + x$

Proof:
Using the following axioms:
{{:Axiom:Axiomatization of 1-Based Natural Numbers}}
Let $x \in \N_{> 0}$ be arbitrary.
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$x + n = n + x$
=== Basis for the Induction ===
From Natural Number Commutes with 1 under Addition, we have that:
:$\forall x \in \N_{> 0}: x + 1 = 1 + x$
and so $\map P 1$ holds.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$x + k = k + x$
Then we need to show:
:$x + \paren {k + 1} = \paren {k + 1} + x$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = x + \paren {k + 1}
      | r = \paren {x + k} + 1
      | c = Natural Number Addition is Associative
}}
{{eqn | r = \paren {k + x} + 1
      | c = Induction Hypothesis
}}
{{eqn | r = k + \paren {x + 1}
      | c = Natural Number Addition is Associative
}}
{{eqn | r = k + \paren {1 + x}
      | c = Basis for the Induction
}}
{{eqn | r = \paren {k + 1} + x
      | c = Natural Number Addition is Associative
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
{{qed}}
Theorem: Ordering on Natural Numbers is Trichotomy

Let $\N$ be the natural numbers.
Let $<$ be the (strict) ordering on $\N$.
Then exactly one of the following is true:
:$(1): \quad a = b$
:$(2): \quad a > b$
:$(3): \quad a < b$
That is, $<$ is a trichotomy on $\N$.

Proof:
Applying the definition of $<$, the theorem becomes:
Exactly one of the following is true:
:$(1): \quad a = b$
:$(2): \quad \exists n \in \N_{>0} : b + n = a$
:$(3): \quad \exists n \in \N_{>0} : a + n = b$
We will use the principle of Mathematical Induction.
Let $P \left({a}\right)$ be the proposition that exactly one of the above is true, for all natural numbers $b$, for fixed natural number $a$.
Theorem: Ordering on 1-Based Natural Numbers is Transitive

Let $\N_{> 0}$ be the $1$-based natural numbers.
Let $<$ be the strict ordering on $\N_{>0}$.
Then $<$ is a transitive relation.

Proof:
Let $a < b$ and $b < c$.
Then:
{{begin-eqn}}
{{eqn | q = \exists x \in \N_{> 0}
      | l = a + x
      | r = b
      | c = 
}}
{{eqn | ll= \land
      | q = \exists y \in \N_{> 0}
      | l = b + y
      | r = c
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {a + x} + y
      | r = c
      | c = substituting $a + x$ for $b$
}}
{{eqn | ll= \leadsto
      | l = a + \paren {x + y}
      | r = c
      | c = Natural Number Addition is Associative
}}
{{eqn | ll= \leadsto
      | l = a
      | o = <
      | r = c
      | c = as $x + y \in \N_{> 0}$
}}
{{end-eqn}}
{{qed}}
Theorem: Trichotomy is Antireflexive

Let $\RR$ be a trichotomy.
Then $\RR$ is an antireflexive relation.

Proof:
Let $\RR$ be a trichotomy on a set $S$.
Let $x \in S$.
By definition of a trichotomy, for all $a, b \in S$, either:
:$a \mathrel \RR b$
:$a = b$
:$b \mathrel \RR a$
As $x = x$ it follows directly that $x \not < x$.
Hence the result by definition of antireflexive relation.
{{qed}}
Category:Antireflexive Relations
Category:Trichotomies
inz957y8e3kyaq0d6bnju3kveax7ot6
Theorem: Ordering on 1-Based Natural Numbers is Total Ordering

Let $\N_{> 0}$ be the $1$-based natural numbers.
Let $<$ be the strict ordering on $\N_{>0}$.
Then $<$ is a (strict) total ordering.

Proof:
From Ordering on $1$-Based Natural Numbers is Trichotomy we have that $<$ is trichotomy.
From Ordering on $1$-Based Natural Numbers is Transitive we have that $<$ is transitive.
From Trichotomy is Antireflexive it follows that $<$ is antireflexive.
It follows by definition that $<$ is a strict ordering.
By the trichotomy law it follows that $<$ is a strict total ordering.
{{qed}}
Theorem: Left Cancellable Commutative Operation is Right Cancellable

Let $\struct {S, \circ}$ be an algebraic structure.
Let $\circ$ be left cancellable and also commutative.
Then $\circ$ is also right cancellable.

Proof:
Let $\circ$ be both left cancellable and commutative on a set $S$.
Then:
{{begin-eqn}}
{{eqn | l = a \circ c
      | r = b \circ c
      | c = 
}}
{{eqn | ll= \leadsto
      | l = c \circ a
      | r = c \circ b
      | c = $\circ$ is Commutative
}}
{{eqn | ll= \leadsto
      | l = a
      | r = b
      | c = $\circ$ is Left Cancellable
}}
{{end-eqn}}
{{qed}}
Theorem: Right Cancellable Commutative Operation is Left Cancellable

Let $\struct {S, \circ}$ be an algebraic structure.
Let $\circ$ be right cancellable and also commutative.
Then $\circ$ is also left cancellable.

Proof:
Let $\circ$ be both right cancellable and commutative on a set $S$.
Then:
{{begin-eqn}}
{{eqn | l = a \circ b
      | r = a \circ c
      | c = 
}}
{{eqn | ll= \leadsto
      | l = b \circ a
      | r = c \circ a
      | c = $\circ$ is Commutative
}}
{{eqn | ll= \leadsto
      | l = b
      | r = c
      | c = $\circ$ is Right Cancellable
}}
{{end-eqn}}
{{qed}}
Theorem: Natural Number Addition is Cancellable

Let $\N$ be the natural numbers.
Let $+$ be addition on $\N$.
Then:
:$\forall a, b, c \in \N: a + c = b + c \implies a = b$
:$\forall a, b, c \in \N: a + b = a + c \implies b = c$
That is, $+$ is cancellable on $\N$.

Proof:
Consider the natural numbers $\N$ defined as a naturally ordered semigroup $\struct {\N, +, \le}$.
By {{NOSAxiom|2}}, every element of $\struct {\N, +}$ is cancellable.
{{qed}}
Theorem: Natural Number Addition is Cancellable

Let $\N$ be the natural numbers.
Let $+$ be addition on $\N$.
Then:
:$\forall a, b, c \in \N: a + c = b + c \implies a = b$
:$\forall a, b, c \in \N: a + b = a + c \implies b = c$
That is, $+$ is cancellable on $\N$.

Proof:
By Natural Number Addition is Commutative, we only need to prove the first statement.
Proof by induction.
Consider the natural numbers $\N$ defined in terms of Peano's Axioms.
From the definition of addition in Peano structure, we have that:
{{begin-eqn}}
{{eqn | q = \forall m, n \in \N
      | l = m + 0
      | r = m
}}
{{eqn | l = m + \map s n
      | r = \map s {m + n}
}}
{{end-eqn}}
For all $n \in \N$, let $\map P n$ be the proposition:
:$\forall a, b \in \N: a + n = b + n \implies a = b$
=== Basis for the Induction ===
$\map P 0$ is the proposition:
:$\forall a, b \in \N: a + 0 = b + 0 \implies a = b$
which holds because of the definition of $+$.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \in \N$, then it logically follows that $\map P {\map s k}$ is true.
So this is our induction hypothesis $\map P k$:
:$\forall a, b \in \N: a + k = b + k \implies a = b$
Then we need to show that $\map P {\map s k}$ follows directly from $\map P k$:
:$\forall a, b \in \N: a + \map s k = b + \map s k \implies a = b$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = a + \map s k
      | r = b + \map s k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map s {a + k}
      | r = \map s {b + k}
      | c = Definition of $+$
}}
{{eqn | ll= \leadsto
      | l = a + k
      | r = b + k
      | c = {{PeanoAxiom|3}}
}}
{{eqn | ll= \leadsto
      | l = a
      | r = b
      | c = Induction Hypothesis
}}
{{end-eqn}}
So $\map P k \implies \map P {\map s k}$ and the result follows by the Principle of Mathematical Induction for Peano Structure.
Therefore:
:$\forall a, b \in \N: a + n = b + n \implies a = b$
{{qed}}
Theorem: Natural Number Multiplication is Cancellable

Let $\N$ be the natural numbers.
Let $\times$ be multiplication on $\N$.
Then:
:$\forall x, y, z \in \N_{>0}: x \times z = y \times z \implies x = y$
:$\forall x, y, z \in \N_{>0}: x \times y = x \times z \implies y = z$
That is, $\times$ is cancellable on $\N_{>0}$.

Proof:
By Natural Number Multiplication is Commutative, proving one of the assertions suffices.
From Ordering on Natural Numbers is Compatible with Multiplication it follows that:
:$\forall x, y, z \in \N: x < y \iff x \times z < y \times z$
Interchanging $x$ and $y$, we obtain:
:$\forall x, y, z \in \N: y < x \iff y \times z < x \times z$
From Ordering on Natural Numbers is Trichotomy, the only remaining possibility is:
:$\forall x, y, z \in \N: x = y \iff x \times z = y \times z$
Hence, $\times$ is cancellable on $\N_{>0}$.
{{qed}}
Theorem: Natural Number Addition is Cancellable for Ordering

Let $\N$ be the natural numbers.
Let $<$ be the strict ordering on $\N$.
Let $+$ be addition on $\N$.
Then:
:$\forall a, b, c \in \N_{>0}: a + c < b + c \implies a < b$
:$\forall a, b, c \in \N_{>0}: a + b < a + c \implies b < c$
That is, $+$ is cancellable on $\N$ for $<$.

Proof:
{{ProofWanted}}
Category:Natural Number Addition
Category:Examples of Cancellable Operations
nbgpynwtclm58j7no3ognibx6pfc6nq
Theorem: Natural Number Multiplication is Cancellable for Ordering

Let $\N$ be the natural numbers.
Let $\times$ be multiplication on $\N$.
Let $<$ be the strict ordering on $\N$.
Then:
:$\forall a, b, c \in \N: a \times c < b \times c \implies a < b$
:$\forall a, b, c \in \N: a \times b < a \times c \implies b < c$
That is, $\times$ is cancellable on $\N$ for $<$.

Proof:
{{proof wanted}}
Category:Examples of Cancellable Operations
Category:Natural Number Multiplication
4jy5waacgramzyozgw5mrge19x723xf
Theorem: Successor to Natural Number

Let $\N_{> 0}$ be the 1-based natural numbers:
:$\N_{> 0} = \left\{{1, 2, 3, \ldots}\right\}$
Let $<$ be the ordering on $\N_{> 0}$:
:$\forall a, b \in \N_{>0}: a < b \iff \exists c \in \N_{>0}: a + c = b$
Let $a \in \N_{>0}$.
Then there exists no natural number $n$ such that $a < n < a + 1$.

Proof:
Using the following axioms:
{{:Axiom:Axiomatization of 1-Based Natural Numbers}}
Suppose that $\exists n \in \N_{>0}: a < n < a + 1$.
Then by the definition of ordering on natural numbers:
{{begin-eqn}}
{{eqn | l = a + x
      | r = n
      | c = Definition of Ordering on Natural Numbers: $a < n$
}}
{{eqn | l = n + y
      | r = a + 1
      | c = Definition of Ordering on Natural Numbers: $a < n$
}}
{{eqn | ll= \implies
      | l = \left({a + x}\right) + y
      | r = a + 1
      | c = substitution for $n$
}}
{{eqn | ll= \implies
      | l = a + \left({x + y}\right)
      | r = a + 1
      | c = Natural Number Addition is Associative
}}
{{eqn | ll= \implies
      | l = x + y
      | r = 1
      | c = Addition on $1$-Based Natural Numbers is Cancellable
}}
{{end-eqn}}
By Axiom $D$, either:
:$y = 1$
or:
:$y = t + 1$ for some $t \in \N_{>0}$
Then either:
:$x + 1 = 1$ when $y = 1$
or:
:$x + \left({t + 1}\right) = \left({x + t}\right) + 1 = 1$ when $y = t + 1$
Both of these conclusions violate Natural Number is Not Equal to Successor.
Hence the result.
{{qed}}
Theorem: Natural Number is Not Equal to Successor

Let $\N_{> 0}$ be the $1$-based natural numbers:
:$\N_{> 0} = \set {1, 2, 3, \ldots}$
Then:
:$\forall n \in \N_{> 0}: n \ne n + 1$

Proof:
Using the following axioms:
{{:Axiom:Axiomatization of 1-Based Natural Numbers}}
Proof by induction:
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$n \ne n + 1$
=== Basis for the Induction ===
$\map P 1$ is the case:
:$1 \ne 1 + 1$
From axiom $E$:
:$E: \quad \forall a, b \in \N_{> 0}: \text{ exactly 1 of these three holds: } a = b \lor \paren {\exists x \in \N_{> 0}: a + x = b} \lor \paren {\exists y \in \N_{> 0}: a = b + y}$
Putting $a = b = 1$ this means:
:$1 = 1$
or
:$1 = 1 + 1$
As $1 = 1$ it follows that $1 \ne 1 + 1$ and so $\map P 1$ holds.
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:
:$k \ne k + 1$
Then we need to show:
:$k + 1 \ne \paren {k + 1} + 1$
=== Induction Step ===
This is our induction step:
As $k \ne k + 1$  from the induction hypothesis, it follows that:
:$k + 1 \ne \paren {k + 1} + 1$
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}: n \ne n + 1$
{{qed}}
Theorem: Biconditional is Commutative

==== Formulation 1 ====
{{:Biconditional is Commutative/Formulation 1}}
==== Formulation 2 ====
{{:Biconditional is Commutative/Formulation 2}}

Proof:
{{BeginTableau|p \iff q \vdash q \iff p}}
{{Premise|1|p \iff q}}
{{BiconditionalElimination|2|1|p \implies q|1|1}}
{{BiconditionalElimination|3|1|q \implies p|1|2}}
{{BiconditionalIntro|4|1|q \iff p|3|2}}
{{EndTableau}}
{{qed|lemma}}
{{BeginTableau|q \iff p \vdash p \iff q}}
{{Premise|1|q \iff p}}
{{BiconditionalElimination|2|1|q \implies p|1|1}}
{{BiconditionalElimination|3|1|p \implies q|1|2}}
{{BiconditionalIntro|4|1|p \iff q|3|2}}
{{EndTableau}}
{{qed}}
Theorem: Biconditional is Commutative

==== Formulation 1 ====
{{:Biconditional is Commutative/Formulation 1}}
==== Formulation 2 ====
{{:Biconditional is Commutative/Formulation 2}}

Proof:
{{BeginTableau|p \iff q \vdash q \iff p}}
{{Premise|1|p \iff q}}
{{SequentIntro|2|1|\paren {p \implies q} \land \paren {q \implies p}|1|Rule of Material Equivalence}}
{{Commutation|3|1|\paren {q \implies p} \land \paren {p \implies q}|2|Conjunction}}
{{SequentIntro|4|1|q \iff p|3|Rule of Material Equivalence}}
{{EndTableau|lemma}}
{{BeginTableau|q \iff p \vdash p \iff q}}
{{Premise|1|q \iff p}}
{{SequentIntro|2|1|\paren {q \implies p} \land \paren {p \implies q}|1|Rule of Material Equivalence}}
{{Commutation|3|1|\paren {p \implies q} \land \paren {q \implies p}|2|Conjunction}}
{{SequentIntro|4|1|p \iff q|3|Rule of Material Equivalence}}
{{EndTableau|qed}}
Theorem: Biconditional is Commutative

==== Formulation 1 ====
{{:Biconditional is Commutative/Formulation 1}}
==== Formulation 2 ====
{{:Biconditional is Commutative/Formulation 2}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccc||ccc|} \hline
p & \iff & q & q & \iff & p \\
\hline
\F & \T & \F & \F & \T & \F \\
\F & \F & \T & \T & \F & \F \\
\T & \F & \F & \F & \F & \T \\
\T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Biconditional is Reflexive

:$\vdash p \iff p$

Proof:
{{BeginTableau|\vdash p \iff p}}
{{TheoremIntro|1|p \implies p|Law of Identity: Formulation 2}}
{{BiconditionalIntro|2||p \iff p|1|1}}
{{EndTableau|qed}}
Theorem: Biconditional is Reflexive

:$\vdash p \iff p$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective match for both boolean interpretations.
:<nowiki>$\begin {array} {|ccc|} \hline
p & \iff & p \\
\hline
\F & \T & \F \\
\T & \T & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Biconditional is Transitive

The biconditional operator is transitive:

Proof:
{{BeginTableau|p \iff q, q \iff r \vdash p \iff r}}
{{Premise|1|p \iff q}}
{{Premise|2|q \iff r}}
{{BiconditionalElimination|3|1|p \implies q|1|1}}
{{BiconditionalElimination|4|2|q \implies r|2|1}}
{{SequentIntro|5|1, 2|p \implies r|1, 2|Hypothetical Syllogism: Formulation 1}}
{{BiconditionalElimination|6|1|q \implies p|1|2}}
{{BiconditionalElimination|7|2|r \implies q|2|2}}
{{SequentIntro|8|1, 2|r \implies p|7, 6|Hypothetical Syllogism: Formulation 1}}
{{BiconditionalIntro|9|1, 2|p \iff r|5|8}}
{{EndTableau|qed}}
Theorem: Biconditional is Transitive

The biconditional operator is transitive:

Proof:
We apply the Method of Truth Tables.
As can be seen for all boolean interpretations by inspection, where the truth values under the main connective on the {{LHS}} is $T$, that under the one on the {{RHS}} is also $T$:
:<nowiki>$\begin {array} {|ccccccc||ccc|} \hline
(p & \iff & q) & \land & (q & \iff & r) & p & \iff & r \\
\hline
\F & \T & \F & \T & \F & \T & \F & \F & \T & \F \\
\F & \T & \F & \F & \F & \F & \T & \F & \F & \T \\
\F & \F & \T & \F & \T & \F & \F & \F & \T & \F \\
\F & \F & \T & \F & \T & \T & \T & \F & \F & \T \\
\T & \F & \F & \F & \F & \T & \F & \T & \F & \F \\
\T & \F & \F & \F & \F & \F & \T & \T & \T & \T \\
\T & \T & \T & \F & \T & \F & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end {array}$</nowiki>
Hence the result.
{{qed}}
Theorem: Ordinals are Totally Ordered

The ordinals are totally ordered.

Proof:
Follows directly from Relation between Two Ordinals and Subset Relation is Ordering.
{{qed}}
Category:Ordinals
7j5gt4exlrw1dxv82z8s62oow1hw3bv
Theorem: Successor Set of Transitive Set is Transitive

Let $S$ be a transitive set.
Then its successor set $S^+ = S \cup \set S$ is also transitive.

Proof:
Recall that $S$ is '''transitive''' {{iff}}:
:$x \in S \implies x \subseteq S$
Hence:
{{begin-eqn}}
{{eqn | q = \forall x \in S^+
      | l = x
      | o = \in
      | r = S
      | c = 
}}
{{eqn | lo= \lor
      | l = x
      | r = S
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \subseteq
      | r = S
      | c = {{Defof|Transitive Set}}: $x \in S \implies x \subseteq S$
}}
{{eqn | lo= \lor
      | l = x
      | o = \subseteq
      | r = S
      | c = Set is Subset of Itself: $x = S \implies x \subseteq S$
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \subseteq
      | r = S
      | c = Proof by Cases: both $x \in S$ and $x = S$ lead to $x \subseteq S$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | q = \forall S
      | l = S
      | o = \subseteq
      | r = S^+
      | c = Set is Subset of Union
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \subseteq
      | r = S^+
      | c = 
}}
{{end-eqn}}
Thus we have:
:$x \in S \implies x \subseteq S$
Hence the result.
{{qed}}
Theorem: Successor Set of Ordinal is Ordinal

Let $\On$ denote the class of all ordinals.
Let $\alpha \in \On$ be an ordinal.
Then its successor set $\alpha^+ = \alpha \cup \set \alpha$ is also an ordinal.

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 the successor mapping.
That is:
:$\forall \alpha \in \On: \alpha^+ \in \On$
{{qed}}
Theorem: Successor Set of Ordinal is Ordinal

Let $\On$ denote the class of all ordinals.
Let $\alpha \in \On$ be an ordinal.
Then its successor set $\alpha^+ = \alpha \cup \set \alpha$ is also an ordinal.

Proof:
{{explain|Would be insightful to make the definition of ordinal being used explicit.}}
From Ordinal is Transitive, it follows by Successor Set of Transitive Set is Transitive that $\alpha^+$ is transitive.
We now have to show that $\alpha^+$ is strictly well-ordered by the epsilon restriction $\Epsilon {\restriction_{\alpha^+} }$.
So suppose that a subset $A \subseteq \alpha^+$ is non-empty.
Then:
{{begin-eqn}}
{{eqn | l = A
      | r = A \cap \paren {\alpha \cup \set \alpha}
      | c = Intersection with Subset is Subset and {{Defof|Successor Set}}
}}
{{eqn | n = 1
      | r = \paren {A \cap \alpha} \cup \paren {A \cap \set \alpha}
      | c = Intersection Distributes over Union
}}
{{end-eqn}}
We need to show that $A$ has a smallest element.
We first consider the case where $A \cap \alpha$ is empty.
By equation $\paren 1$, it follows that $A \cap \set \alpha$ is non-empty (because $A$ is non-empty).
Therefore:
:$\alpha \in A$
That is:
:$\set \alpha \subseteq A$
By Union with Empty Set and Intersection with Subset is Subset, equation $\paren 1$ implies that $A \subseteq \set \alpha$.
Therefore, $A = \set \alpha$ by the definition of set equality.
So $\alpha$ is the smallest element of $A$.
We now consider the case where $A \cap \alpha$ is non-empty.
By Intersection is Subset:
:$A \cap \alpha \subseteq \alpha$
By the definition of a well-ordered set, there exists a smallest element $x$ of $A \cap \alpha$.
Let $y \in A$.
If $y \in \alpha$, then $y \in A \cap \alpha$
Therefore, by the definition of the smallest element, either $x \in y$ or $x = y$.
Otherwise, $y = \alpha$, and so $x \in \alpha = y$.
That is, $x$ is the smallest element of $A$.
{{qed}}