avewright/proofwiki-math huggingface dataset:
Theorem: Frobenius's Theorem

An algebraic associative real division algebra $A$ is isomorphic to $\R, \C$ or $\Bbb H$.

Proof:
Recall that an algebra $A$ is said to be quadratic if it is unital and the set $\set {1, x, x^2}$ is linearly dependent for every $x \in A$.
{{explain|This needs to be reviewed, as Definition:Quadratic Algebra as currently posted up does not match the above.}}
Thus, for every $x \in A$ there exist $\map t x, \map n x \in \R$ such that:
:$x^2 - \map t x x + \map n x = 0$
Obviously, $\map t x$ and $\map n x$ are uniquely determined if $x \notin \R$.
{{handwaving|Obviously?}}
{{Proofread}}
Suppose $x \notin \R$.
Then $x$ can be expressed as $x = a + b i$, with $a, b \in \R$ and $b \ne 0$.
Then:
:$x^2 = a^2 - b^2 + 2 a b i$
and:
:$x^2 - \map t x x + \map n x = a^2 - b^2 - a \map t x + \map n x + \paren {2 a b - b \map t x} i = 0$
It follows that both:
:$(1): \quad 2 a b - b \map t x = 0$
and:
:$(2): \quad a^2 - b^2 - a \map t x + \map n x = 0$
$(1)$ leads to:
:$\map t x = 2 a$
and $(2)$ leads to;
:$\map n x = a^2 + b^2$
Setting $\map t \lambda = 2 \lambda$ and $\map n \lambda = \lambda^2$ for $\lambda \in \R$, we can then consider $t$ and $n$ as maps from $A$ into $\R$.
(In this way $t$ becomes a linear functional).
We call $\map t x$ and $\map n x$ the trace and the norm of $x$ respectively.
{{explain|Trace most certainly has not been disambiguated, and I'm not sure that "norm" is directly the same as the complex modulus}}
{{Disambiguate|Definition:Norm}}
{{Disambiguate|Definition:Trace}}
From $x^2 - \paren {x + x^*} x + x^* x = 0$ we see that all algebras $\Bbb A_n$ are quadratic.
Further, every real division algebra $A$ that is algebraic and power-associative (this means that every subalgebra generated by one element is associative) is automatically quadratic.
Indeed, if $x \in A$ then there exists a nonzero polynomial $\map f X \in \R \sqbrk X$ such that $\map f x = 0$.
Writing $\map f X$ as the product of linear and quadratic polynomials in $\R \sqbrk X$ it follows that $\map p x = 0$ for some $\map p X \in \R \sqbrk X$ of degree $1$ or $2$.
In particular, algebraic alternative (and hence associative) real division algebras are quadratic.
Finally, if $A$ is a real unital algebra, that is, an algebra over $\R$ with unity $1$, then we shall follow a standard convention and identify $\R$ with $\R 1$.
Thus we shall write $\lambda$ for $\lambda 1$, where $\lambda \in \R$.
Theorem: Preimages All Exist iff Surjection

Let $f: S \to T$ be a mapping.
Let $f^{-1}$ be the inverse of $f$.
Let $\map {f^{-1} } t$ be the preimage of $t \in T$.
Then $\map {f^{-1} } t$ is empty for no $t \in T$ {{iff}} $f$ is a surjection.

Proof:
=== Necessary Condition ===
We use a Proof by Contraposition.
To that end, suppose:
:$\exists t \in T: \map {f^{-1} } t = \O$
That is:
:$\neg \paren {\forall t \in T: \exists s \in S: \map f s = t}$
So, by definition, $f: S \to T$ is not a surjection.
From Rule of Transposition it follows that if $f$ is a surjection:
$\neg \exists t \in T: \map {f^{-1} } t = \O$
{{qed|lemma}}
=== Sufficient Condition ===
We again use a Proof by Contraposition.
To that end, suppose $f$ is not a surjection.
Then by definition:
:$\exists t \in T: \neg \paren {\exists s \in S: \map f s = t}$
That is:
:$\exists t \in T: \map {f^{-1} } t = \O$
From Rule of Transposition it follows that if $\neg \exists t \in T: \map {f^{-1} } t = \O$, then $f$ is a surjection.
{{Qed}}
Theorem: Preimages All Exist iff Surjection

Let $f: S \to T$ be a mapping.
Let $f^{-1}$ be the inverse of $f$.
Let $\map {f^{-1} } t$ be the preimage of $t \in T$.
Then $\map {f^{-1} } t$ is empty for no $t \in T$ {{iff}} $f$ is a surjection.

Proof:
Suppose that there is no $t \in T$ such that $\map {f^{-1} } t$ is empty.
By Denial of Existence, this is equivalent to saying that for all $t \in T$, $\map {f^{-1} } t$ is not empty.
This is equivalent to the statement that $\map {f^{-1} } t$ contains at least one element for each $t \in T$.
In other words, for each $t \in T$, there exists an $s\in S$ such that $\map f s = t$.
This is the definition of $f$ being surjective.
Thus if there is no $t \in T$ such that $\map {f^{-1} } t$ is empty, then $f$ is surjective.
Since this proof only uses statements of equivalence, it also shows that $f$ being surjective implies that there is no $t \in T$ such that $\map {f^{-1} } t$ is empty.
{{qed}}
Theorem: Non-Successor Element of Peano Structure is Unique

Let $\struct {P, s, 0}$ be a Peano structure.
Then:
:$P \setminus s \sqbrk P$ is a singleton
where:
:$\setminus$ denotes set difference
:$s \sqbrk P$ denotes the image of the mapping $s$.
It follows that the non-successor element $0$ is the only element of $P$ with this property.

Proof:
{{handwaving|It is not explicit which formulation of Peano's axioms is used, while this is very relevant for this elementary result}}
Let $T = P \setminus s \sqbrk P$.
From Axiom $(\text P 4)$ we know that $T \ne \O$.
Now suppose that $t_1 \in T$ and $t_2 \in T$.
{{AimForCont}} $t_1 \ne t_2$.
Define $A = P \setminus \set {t_2}$.
Thus $t_1 \in A \ne P$.
Moreover, by the nature of $t_2$:
:$x \in A \implies \map s x \in A$
Thus, by the induction axiom $(\text P 5)$, $A = P$.
From this contradiction it follows that $P \setminus s \sqbrk P$ cannot contain two different elements.
{{qed}}
Theorem: Equivalence of Formulations of Peano's Axioms

Let $P$ be a set.
Let $s: P \to P$ be a mapping.
Let $0 \in P$ be a distinguished element.
{{TFAE|def = Peano's Axioms|view = Peano's Axioms}}

Proof:
=== Formulation 1 implies Formulation 2 ===
For $(\text P 3)$, there is nothing to prove.
Next, axiom $(\text P 4)$ of Formulation 2.
Recall the definition of the image of a mapping as applicable to $s$:
:$\Img s = \set {n \in P: \exists m \in P: \map s m = n}$
From this definition, it follows that $0 \notin \Img s$, and hence:
:$\Img s \ne P$
Lastly, axiom $(\text P 5)$ of Formulation 2.
By Non-Successor Element of Peano Structure is Unique, we know that there is exactly one element of $P$ that is not in the image of $s$.
By axiom $(\text P 3)$ of Formulation 1, we know this element is $0$.
Therefore, the premises:
:$0 \in A$
and:
:$\exists x \in A: \neg \exists y \in P: x = \map s y$
are logically equivalent, and hence so are both forms of axiom $(\text P 5)$.
{{qed|lemma}}
Theorem: Product of Row Sum Unity Matrices

Let $\mathbf A = \sqbrk a_{m n}$ be an $m \times n$ matrix.
Let $\mathbf B = \sqbrk b_{n p}$ be an $n \times p$ matrix.
Let the row sum of $\mathbf A$ and $\mathbf B$ be equal to $1$.
Then the row sum of their (conventional) product is also $1$.

Proof:
We have that:
:$\ds \sum_{i \mathop = 1}^n a_{i j} = \sum_{i \mathop = 1}^n b_{i j} = 1$
Then:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 1}^n \paren {\mathbf A \mathbf B}_{i j}
      | r = \sum_{i \mathop = 1}^n \paren {\sum_{k \mathop = 1}^n a_{i k} b_{k j} }
      | c = 
}}
{{eqn | r = \sum_{i, k \mathop = 1}^n a_{i k} b_{k j}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^n \paren {b_{k j} \sum_{i \mathop = 1}^n a_{i k} }
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^n \paren {b_{k j} \cdot 1}
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Matrix Algebra
fhumvruv3wofbxlo82hj1i1pbeyhihs
Theorem: Image of Successor Mapping forms Peano Structure

Let $\struct {P, s, 0}$ be a Peano structure.
Let $P'$ be the set $s \sqbrk P$, that is:
:$P' = \set {\map s n: n \in P}$
Let $s'$ be the restriction of $s$ to $P'$.
Then $\struct {P', s', \map s 0}$ is also a Peano structure.

Proof:
{{Improve| Expressions generated by {{TL|PeanoAxiom}} template (starting with Peano's Axiom) should not be confused with the intended ones.}}
We need to check that all of Peano's axioms hold for $\struct {P', s', \map s 0}$.
Now from Restriction of Injection is Injection, because $s$ is an injection then so is $s'$.
So {{PeanoAxiom|3}} holds.
{{AimForCont}} that for some $n \in P'$, we would have:
:$\map {s'} n = \map s 0$
Then by definition of $s'$ as the restriction of $s$:
:$\map s n = \map s 0$
However, since $0 \notin P'$, it follows that $n \ne 0$.
This contradicts the fact that $s$ is an injection.
Hence for all $n \in P'$:
:$\map {s'} n \ne \map s 0$
So {{PeanoAxiom|4}} holds as well.
Let $A \subseteq P'$ be such that $\map s 0 \in A$ and:
:$\forall z \in A: \map {s'} z \in A$
Let $A_0$ be defined as:
:$A_0 = A \cup \set 0$
Then $0 \in A_0$, and since:
:$\forall z \in A: \map {s'} z \in A$
:$\map s 0 \in A$
it follows that:
:$\forall z \in A_0: \map s z \in A_0$
Therefore, since $\struct {P, s, 0}$ is a Peano structure:
:$A_0 = P$
Therefore, since $\map s n \ne 0$ for all $n \in P$:
:$\forall n \in P: \map s n \in A$
Hence, by definition of $P'$:
:$P' \subseteq A$
By definition of set equality:
:$A = P'$
meaning that {{PeanoAxiom|5}} holds as well.
{{Finish|{{PeanoAxiom|2}}. $n \in P' \implies \map {s'} n \in P'$ in this context.}}
Having verified all axioms, it follows that $\struct {P', s', \map s 0}$ is a Peano structure.
{{qed}}
Category:Peano's Axioms
Category:Peano Structures
ta01qrzhjfmc4lkz3wak4cpiw9avfv5
Theorem: Restriction of Injection is Injection

Let $f: S \to T$ be an injection.
Let $X \subseteq S$ be a subset of $S$.
Let $f \sqbrk X$ denote the image of $X$ under $f$.
Let $Y \subseteq T$ be a subset of $T$ such that $f \sqbrk X \subseteq Y$.
The restriction $f \restriction_{X \times Y}$ of $f$ to $X \times Y$ is an injection from $X$ to $Y$.

Proof:
First we show that $f \restriction_{X \times Y}$ is a mapping from $X$ to $Y$.
By Restriction of Mapping is Mapping, $f \restriction_{X \times T}$ is a mapping from $X$ to $T$.
If $x \in X$, then by the definition of image:
:$\map f x \in f \sqbrk X$
{{explain|More explanation required.}}
Since $f \sqbrk X \subseteq Y$, $f \restriction_{X \times Y}$ is a mapping from $X$ to $Y$.
By definition of an injection:
:$\forall s_1, s_2 \in S: \map f {s_1} = \map f {s_2} \implies s_1 = s_2$.
{{AimForCont}} $f \restriction_{X \times Y}: X \to Y$ were ''not'' an injection.
Then:
:$\exists x_1, x_2 \in X: x_1 \ne x_2, \map f {x_1} = \map f {x_2}$
But then:
:$\exists x_1, x_2 \in S: x_1 \ne x_2, \map f {x_1} = \map f {x_2}$
So $f: S \to T$ would not then be an injection.
Hence the result.
{{qed}}
Category:Injections
cjlhkrj0b6mhp1hbfnelm8lste85t5v
Theorem: Diagonal Relation is Many-to-One

The diagonal relation is many-to-one.
That is:
:$\forall x \in \Dom {\Delta_S}: \tuple {x, y_1} \in \Delta_S \land \tuple {x, y_2} \in \Delta_S \implies y_1 = y_2$
where $\Delta_S$ is the diagonal relation on a set $S$.

Proof:
Let $S$ be a set and let $\Delta_S$ be the diagonal relation on $S$.
Let $\tuple {x, y_1} \in \Delta_S \land \tuple {x, y_2} \in \Delta_S$.
From the definition of the diagonal relation:
:$\tuple {x, y_1} = \tuple {x, x}$
:$\tuple {x, y_2} = \tuple {x, x}$
and so $y_1 = y_2$.
{{qed}}
Theorem: Absolute Value is Many-to-One

Let $f: \R \to \R$ be the absolute value function:
:$\forall x \in \R:  \map f x = \begin{cases}
x & : x \ge 0 \\
-x & : x < 0
\end{cases}$
Then $f$ is a many-to-one relation.

Proof:
{{AimForCont}} $f$ is not a many-to-one relation.
Then there exists $y_1 \in \R$ and $y_2 \in \R$ where $y_1 \ne y_2$ such that:
:$\exists x \in \R: \map f x = y_1, \map f x = y_2$
There are two possibilities:
{{begin-eqn}}
{{eqn | n = 1
      | l = x
      | o = \ge
      | r = 0
      | c = 
}}
{{eqn | n = 2
      | l = x
      | o = <
      | r = 0
      | c = 
}}
{{end-eqn}}
Suppose $x \ge 0$.
Then:
{{begin-eqn}}
{{eqn | l = y_1 = \map f x
      | r = x
}}
{{eqn | l = y_2 = \map f x
      | r = x
}}
{{end-eqn}}
That is:
:$y_2 = y_1 = x$
Suppose $x < 0$.
Then:
{{begin-eqn}}
{{eqn | l = y_1 = \map f {x_1}
      | r = -x
}}
{{eqn | l = y_2 = \map f {x_2}
      | r = -x
}}
{{end-eqn}}
That is:
:$y_2 = y_1 = -x$
So by Proof by Cases we have that $y_1 = y_2$ whatever $x$ may be.
This contradicts our assertion that $y_1 \ne y_2$.
Hence it follows by Proof by Contradiction that $f$ is many-to-one.
{{qed}}
Theorem: Subset of Preimage under Relation is Preimage of Subset

Let $\RR \subseteq S \times T$ be a relation.
Let $X \subseteq S, Y \subseteq T$.
Then:
:$X \subseteq \RR^{-1} \sqbrk Y \iff \RR \sqbrk X \subseteq Y$
In the language of direct image mappings, this can be written:
:$X \subseteq \map {\RR^\gets} Y \iff \map {\RR^\to} X \subseteq Y$

Proof:
As $\RR$ is a relation, then so is its inverse $\RR^{-1}$.
Let $\RR \sqbrk X \subseteq Y$.
Thus:
{{begin-eqn}}
{{eqn | l = \RR \sqbrk X
      | o = \subseteq
      | r = Y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \RR^{-1} \sqbrk {\RR \sqbrk X}
      | o = \subseteq
      | r = \RR^{-1} \sqbrk Y
      | c = {{Corollary|Image of Subset under Relation is Subset of Image|1}}
}}
{{eqn | ll= \leadsto
      | l = X
      | o = \subseteq
      | r = \RR^{-1} \sqbrk Y
      | c = Image of Preimage under Relation is Subset, Subset Relation is Transitive
}}
{{end-eqn}}
So:
:$\RR \sqbrk X \subseteq Y \implies X \subseteq \RR^{-1} \sqbrk Y$
{{qed|lemma}}
Now let $X \subseteq \RR^{-1} \sqbrk Y$.
The same argument applies:
{{begin-eqn}}
{{eqn | l = X
      | o = \subseteq
      | r = \RR^{-1} \sqbrk Y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \RR \sqbrk X
      | o = \subseteq
      | r = \RR \sqbrk {\RR^{-1} \sqbrk Y}
      | c = Image of Subset under Relation is Subset of Image
}}
{{eqn | ll= \leadsto
      | l = \RR \sqbrk X
      | o = \subseteq
      | r = Y
      | c = Image of Preimage under Relation is Subset, Subset Relation is Transitive
}}
{{end-eqn}}
So:
:$X \subseteq \RR^{-1} \sqbrk Y \implies \RR \sqbrk X \subseteq Y$
{{qed|lemma}}
Thus we have:
:$X \subseteq \RR^{-1} \sqbrk Y \implies \RR \sqbrk X \subseteq Y$
:$\RR \sqbrk X \subseteq Y \implies X \subseteq \RR^{-1} \sqbrk Y$
Hence the result.
{{qed}}
Category:Subsets
Category:Preimages under Relations
45j06iscjfgnm82x6w1ipybjykzp76y
Theorem: Composition of Direct Image Mappings of Relations

Let $A, B, C$ be non-empty sets.
Let $\RR_1 \subseteq A \times B, \RR_2 \subseteq B \times C$ be relations.
Let:
:${\RR_1}^\to: \powerset A \to \powerset B$
and
:${\RR_2}^\to: \powerset B \to \powerset C$
be the direct image mappings of $\RR_1$ and $\RR_2$.
Then:
:$\paren {\RR_2 \circ \RR_1}^\to = {\RR_2}^\to \circ {\RR_1}^\to$

Proof:
Let $S \subseteq A, S \ne \O$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\paren { {\RR_2}^\to \circ {\RR_1}^\to} } S
      | r = \map { {\RR_2}^\to} {\map { {\RR_1}^\to } S}
      | c = 
}}
{{eqn | r = \set {\map {\RR_2} x: x \in \map { {\RR_1}^\to } S}
      | c = 
}}
{{eqn | r = \set {\map {\RR_2} x: \exists y \in S: \tuple {x, y} \in \RR_1}
      | c = 
}}
{{eqn | r = \set {\map {\RR_2} {\map {\RR_1} y}: y \in S}
      | c = 
}}
{{eqn | r = \set {\map {\RR_2 \circ \RR_1} y: y \in S}
      | c = 
}}
{{eqn | r = \map {\paren {\RR_2 \circ \RR_1}^\to} S
      | c = 
}}
{{end-eqn}}
Now we treat the case where $S = \O$:
{{begin-eqn}}
{{eqn | l = \map {\paren { {\RR_2}^\to \circ {\RR_1}^\to} } \O
      | r = \O
      | c = 
}}
{{eqn | r = \map {\paren {\RR_2 \circ \RR_1}^\to} \O
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Composite Relations
Category:Composite Mappings
Category:Direct Image Mappings
ebxd07cvo7dwya0vf76r9fd7zkkcin7
Theorem: Subset equals Preimage of Image iff Mapping is Injection

Let $f: S \to T$ be a mapping.
Let $f^{-1}$ denote the inverse of $f$.
Then:
:$\forall A \subseteq S: A = \paren {f^{-1} \circ f} \sqbrk A$ {{iff}} $f$ is an injection
where:
:$f \sqbrk A$ denotes the image of $A$ under $f$
:$f^{-1} \circ f$ denotes the composition of $f^{-1}$ and $f$.
This can be expressed in the language and notation of direct image mappings and inverse image mappings as:
:$\forall A \in \powerset S: A = \map {\paren {f^\gets \circ f^\to} } A$ {{iff}} $f$ is an injection

Proof:
=== Sufficient Condition ===
Let $g$ be such that:
:$\forall A \subseteq S: A = \paren {f^{-1} \circ f} \sqbrk A$
Then by Subset equals Preimage of Image implies Injection, $f$ is an injection.
{{qed|lemma}}
Theorem: Subset equals Image of Preimage iff Mapping is Surjection

Let $f: S \to T$ be a mapping.
Let $f^\to: \powerset S \to \powerset T$ be the direct image mapping of $f$.
Similarly, let $f^\gets: \powerset T \to \powerset S$ be the inverse image mapping of $f$.
Then:
:$\forall B \in \powerset T: B = \map {\paren {f^\to \circ f^\gets} } B$
{{iff}} $f$ is a surjection.

Proof:
=== Sufficient Condition ===
Let $f$ be such that:
:$\forall B \in \powerset T: B = \map {\paren {f^\to \circ f^\gets} } B$
From Subset equals Image of Preimage implies Surjection, $f$ is a surjection.
{{qed|lemma}}
Theorem: Inverse of Injection is Many-to-One Relation

Let $f: S \to T$ be an injection.
Let $f^{-1}: T \to S$ be the inverse relation of $f$.
Then $f^{-1}$ is many-to-one.

Proof:
Let $f: S \to T$ be an injection.
We have by definition of inverse relation that:
:$f^{-1} = \set {\tuple {t, s}: t = \map f s}$
Let $f: S \to T$ be an injection.
Let $\tuple {t, s_1} \in f^{-1}$ and $\tuple {t, s_2} \in f^{-1}$.
By definition, we have that $\map f {s_1} = t = \map f {s_2}$.
But as $f$ is an injection:
:$\map f {s_1} = \map f {s_2} \implies s_1 = s_2$
So we have that:
:$\tuple {t, s_1} \in f^{-1} \land \tuple {t, s_2} \in f^{-1} \implies s_1 = s_2$
and so by definition, $f^{-1}$ is a many-to-one relation.
{{qed}}
Category:Injections
Category:Inverse Relations
ixecpmse2fy6f1ur9mnk60mdnw8boe6
Theorem: Bijection iff Left and Right Cancellable

Let $f$ be a mapping.
Then $f$ is a bijection {{iff}} $f$ is both left cancellable and right cancellable.

Proof:
Follows directly from:
:Injection iff Left Cancellable: $f$ is an injection {{iff}} $f$ is left cancellable
:Surjection iff Right Cancellable: $f$ is a surjection {{iff}} $f$ is right cancellable.
{{qed}}
Theorem: Relation Induced by Mapping is Equivalence Relation

Let $f: S \to T$ be a mapping.
Let $\RR_f \subseteq S \times S$ be the relation induced by $f$:
:$\tuple {s_1, s_2} \in \RR_f \iff \map f {s_1} = \map f {s_2}$
Then $\RR_f$ is an equivalence relation.

Proof:
We need to show that $\RR_f$ is an equivalence relation.
Checking in turn each of the criteria for equivalence:
Theorem: Canonical Injection is Monomorphism

Let $\struct {S_1, \circ_1}$ and $\struct {S_2, \circ_2}$ be algebraic structures with identities $e_1, e_2$ respectively.
The canonical injections:
:$\inj_1: \struct {S_1, \circ_1} \to \struct {S_1, \circ_1} \times \struct {S_2, \circ_2}: \forall x \in S_1: \map {\inj_1} x = \tuple {x, e_2}$
:$\inj_2: \struct {S_2, \circ_2} \to \struct {S_1, \circ_1} \times \struct {S_2, \circ_2}: \forall x \in S_2: \map {\inj_2} x = \tuple {e_1, x}$
are monomorphisms.

Proof:
From Canonical Injection is Injection we have that the canonical injections are in fact injective.
It remains to prove the morphism property.
Let $x, y \in \struct {S_1, \circ_1}$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\inj_1} {x \circ_1 y}
      | r = \tuple {x \circ_1 y, e_2}
}}
{{eqn | r = \tuple {x \circ_1 y, e_2 \circ_2 e_2}
}}
{{eqn | r = \tuple {x, e_2} \circ \tuple {y, e_2}
}}
{{eqn | r = \map {\inj_1} x \circ \map {\inj_1} y
}}
{{end-eqn}}
and the morphism property has been demonstrated to hold for $\inj_1$.
Thus $\inj_1: \struct {S_1, \circ_1} \to \struct {S_1, \circ_1} \times \struct {S_2, \circ_2}$ has been shown to be an injective homomorphism and therefore a monomorphism.
The same argument applies to $\inj_2$.
{{Qed}}
Theorem: Order Embedding is Injection

Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be ordered sets.
Let $\phi: S \to T$ be an order embedding.
That is:
:$\forall x, y \in S: x \preceq_1 y \iff \map \phi x \preceq_2 \map \phi y$
Then $\phi$ is an injection.

Proof:
Suppose $\phi: S \to T$ is a mapping such that:
:$\forall x, y \in S: x \preceq_1 y \iff \map \phi x \preceq_2 \map \phi y$
Then, for all $x, y \in S$:
{{begin-eqn}}
{{eqn | l = \map \phi x
      | r = \map \phi y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \phi x \preceq_2 \map \phi y
      | o = \land
      | r = \map \phi y \preceq_2 \map \phi x
      | c = Ordering $\preceq_2$ is Reflexive
}}
{{eqn | ll= \leadsto
      | l = x \preceq_1 y
      | o = \land
      | r = y \preceq_1 x
      | c = {{Defof|Order Embedding}}
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = Ordering $\preceq_1$ is Antisymmetric
}}
{{end-eqn}}
So $\phi$ is an injection.
{{qed}}
Theorem: Order Isomorphism is Surjective Order Embedding

Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be ordered sets.
Let $f: S \to T$ be a mapping.
Then $f$ is an order isomorphism {{iff}}:
:$(1): \quad f$ is a surjection
:$(2): \quad \forall x, y \in S: x \preceq_1 y \iff \map f x \preceq_2 \map f y$
That is, {{iff}} $f$ is an order embedding which is also a surjection.

Proof:
=== Necessary Condition ===
Suppose $f$ is an order isomorphism.
Then by definition $f$ is a bijection and so a surjection.
Also by definition, $f$ is increasing, and so:
:$\forall x, y \in S: x \preceq_1 y \implies \map f x \preceq_2 \map f y$
Also by definition $f^{-1}$ is also a bijection which is increasing, and so:
:$\forall x, y \in S: \map f x \preceq_2 \map f y \implies x = \map {f^{-1} } {\map f x} \preceq_1 \map {f^{-1} } {\map f y} = y$
and so:
:$\forall x, y \in S: x \preceq_1 y \iff \map f x \preceq_2 \map f y$
{{qed|lemma}}
Theorem: Infimum of Power Set

Let $S$ be a set.
Let $\powerset S$ be the power set of $S$.
Let $\struct {\powerset S, \subseteq}$ be the relational structure defined on $\powerset S$ by the relation $\subseteq$.
(From Subset Relation on Power Set is Partial Ordering, this is an ordered set.)
Then the infimum of $\struct {\powerset S, \subseteq}$ is the empty set $\O$.

Proof:
Follows directly from Empty Set is Subset of All Sets and the definition of infimum.
{{qed}}
Category:Power Set
Category:Empty Set
Category:Order Theory
mxzl51u3522bax9ahoq1hxuit81hyvj
Theorem: Supremum of Power Set

Let $S$ be a set.
Let $\powerset S$ be the power set of $S$.
Let $\struct {\powerset S, \subseteq}$ be the relational structure defined on $\powerset S$ by the relation $\subseteq$.
(From Subset Relation on Power Set is Partial Ordering, this is an ordered set.)
Then the supremum of $\struct {\powerset S, \subseteq}$ is the set $S$.

Proof:
By the definition of the power set:
:$\forall X \in \powerset S: X \subseteq S$
The result then follows from the definition of supremum.
{{qed}}
Category:Power Set
Category:Order Theory
n7tk2sqicrbpkrz6e4rw2pl32muxe4c
Theorem: Diagonal Relation is Ordering and Equivalence

Let $\struct {S, \Delta_S}$ be a relational structure where $\Delta_S$ is the diagonal relation, defined as:
:$\forall x, y \in S: \paren {x, y} \in \Delta_S \iff x = y$
Then $\Delta_S$ is the '''only''' relation on $S$ which is both an equivalence and an ordering.

Proof:
From Trivial Ordering is Universally Compatible and Diagonal Relation is Equivalence we know that the diagonal relation possesses these properties.
We now need to show that it is the '''only''' relation on $S$ which possesses these properties.
Both an equivalence and an ordering are reflexive and transitive.
Also:
:An equivalence relation is symmetric
:An ordering is antisymmetric.
The result follows from Relation is Symmetric and Antisymmetric iff Coreflexive.
{{qed}}
Theorem: Dominance Relation is Ordering

Let $S$ and $T$ be cardinals.
Let $S \preccurlyeq T$ denote that $S$ is dominated by $T$.
Let $\mathbb S$ be any set of cardinals.
Then the relational structure $\struct {\mathbb S, \preccurlyeq}$ is an ordered set.
That is, $\preccurlyeq$ is an ordering (at least partial) on $\mathbb S$.

Proof:
From the definition, a cardinal is a set, so standard set theoretic results apply.
So, checking in turn each of the criteria for an ordering: