avewright/proofwiki-math huggingface dataset:
Theorem: Simple Function is Measurable

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f: X \to \R$ be a simple function.
Then $f$ is $\Sigma$-measurable.

Proof:
Let $f$ be written in the following form:
:$f = \ds \sum_{i \mathop = 1}^n a_i \chi_{S_i}$
where $a_i \in \R$ and the $S_i$ are $\Sigma$-measurable.
Next, for each ordered $n$-tuple $b$ of zeroes and ones define:
:<nowiki>$\map {T_b} i := \begin{cases}
S_i & : \text {if $\map b i = 0$}\\
X \setminus S_i & : \text {if $\map b i = 1$}
\end{cases}$</nowiki>
and subsequently:
:$T_b := \ds \bigcap_{i \mathop = 1}^n \map {T_b} i$
From Sigma-Algebra Closed under Intersection, $T_b \in \Sigma$ for all $b$.
Also, the $T_b$ are pairwise disjoint, and furthermore:
:$f = \ds \sum_b a_b \chi_{T_b}$
where:
:$a_b := \ds \sum_{i \mathop = 1}^n \map b i a_i$
{{finish|prove it, it's a messy business}}
Now we have, for all $\lambda \in \R$:
:$\set {x \in X: \map f x > \lambda} = \ds \bigcup \set {T_b: a_b > \lambda}$
which by Sigma-Algebra Closed under Union is a $\Sigma$-measurable set.
From Characterization of Measurable Functions: $(5)$ it follows that $f$ is measurable.
{{qed}}
Theorem: Identity Mapping is Relation Isomorphism

Let $\struct {S, \RR}$ be a relational structure.
Then the identity mapping $I_S: S \to S$ is a relation isomorphism from $\struct {S, \RR}$ to itself.

Proof:
By definition of identity mapping:
:$\forall x \in S: \map {I_S} x = x$
So:
:$x \mathrel \RR y \implies \map {I_S} x \mathrel \RR \map {I_S} y$
From Identity Mapping is Bijection, $I_S$ is a bijection.
Hence:
:$\map {I_S^{-1} } x = x$
So:
:$x \mathrel \RR y \implies \map {I_S^{-1} } x \mathrel \RR \map {I_S^{-1} } y$
{{qed}}
Theorem: Inverse of Relation Isomorphism is Relation Isomorphism

Let $\struct {S, \RR_1}$ and $\struct {T, \RR_2}$ be relational structures.
Let $\phi: \struct {S, \RR_1} \to \struct {T, \RR_2}$ be a bijection.
Then:
:$\phi: \struct {S, \RR_1} \to \struct {T, \RR_2}$
is a relation isomorphism
{{iff}}:
:$\phi^{-1}: \struct {T, \RR_2} \to \struct {S, \RR_1}$
is also a relation isomorphism.

Proof:
Follows directly from the definition of relation isomorphism.
{{Qed}}
Theorem: Measurable Function is Simple Function iff Finite Image Set

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f: X \to \R$ be a measurable function.
Then $f$ is a simple function {{iff}} its image is finite:
:$\card {\Img f} < \infty$

Proof:
=== Necessary Condition ===
Suppose that $f$ is a simple function, and that:
:$\ds \forall x \in X: \map f x = \sum_{i \mathop = 1}^n a_i \map {\chi_{S_i} } x$
Since each of the $\chi_{S_i}$ is a characteristic function, it can take only the values $0$ and $1$.
Thus each summand can take two values.
It follows immediately that $f$ can take at most $2^n$ different values.
The conclusion follows from Simple Function is Measurable.
{{qed|lemma}}
Theorem: Composite of Relation Isomorphisms is Relation Isomorphism

Let $\struct {S_1, \RR_1}$, $\struct {S_2, \RR_2}$ and $\struct {S_3, \RR_3}$ be relational structures.
Let:
:$\phi: \struct {S_1, \RR_1} \to \struct {S_2, \RR_2}$
and:
:$\psi: \struct {S_2, \RR_2} \to \struct {S_3, \RR_3}$
be relation isomorphisms.
Then $\psi \circ \phi: \struct {S_1, \RR_1} \to \struct {S_3, \RR_3}$ is also a relation isomorphism.

Proof:
From Composite of Bijections is Bijection, $\psi \circ \phi$ is a bijection, as, by definition, an relation isomorphism is also a bijection.
By definition of composition of mappings:
:$\map {\psi \circ \phi} x = \map \psi {\map \phi x}$
As $\phi$ is a relation isomorphism, we have:
:$\forall x_1, y_1 \in S_1: x_1 \mathrel {\RR_1} y_1 \implies \map \phi {x_1} \mathrel {\RR_2} \map \phi {y_1}$
As $\psi$ is a relation isomorphism, we have:
:$\forall x_2, y_2 \in S_2: x_2 \mathrel {\RR_2} y_2 \implies \map \psi {x_2} \mathrel {\RR_3} \map \psi {y_2}$
By setting $x_2 = \map \phi {x_1}, y_2 = \map \phi {y_1}$, it follows that:
:$\forall x_1, y_1 \in S_1: x_1 \mathrel {\RR_1} y_1 \implies \map \psi {\map \phi {x_1} } \mathrel {\RR_3} \map \psi {\map \phi {y_1} }$
Similarly we can show that:
:$\forall x_3, y_3 \in S_3: x_3 \mathrel {\RR_3} y_3 \implies \map {\phi^{-1} } {\map {\psi^{-1} } {x_3} } \mathrel {\RR_1} \map {\phi^{-1} } {\map {\psi^{-1} } {y_3} }$
Hence the result, by definition of a relation isomorphism.
{{qed}}
Theorem: Pointwise Sum of Simple Functions is Simple Function

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f, g : X \to \R$ be simple functions.
Then the pointwise sum $f + g: X \to \R$ of $f$ and $g$:
:$\forall x, y \in X: \map {\paren {f + g} } x := \map f x + \map g x$
is also a simple function.

Proof:
We have $f + g = + \circ \innerprod f g \circ \Delta_X$, where:
:$\Delta_X: X \to X \times X$ is the diagonal mapping on $X$
:$\innerprod f g: X \times X \to \R \times \R, \map {\innerprod f g} {x, y} := \tuple {\map f x, \map g y}$
:$+: \R \times \R \to \R$ is real addition.
{{explain|What is the meaning of the notation $\innerprod f g$? Inner product? And what exactly does the notation in $+ \circ \innerprod f g \circ \Delta_X$?}}
From this, we see that $+$ may be restricted to $\Img {\innerprod f g}$, the image of $\sequence {f, g}$.
It is immediate that this image equals $\Img f \times \Img g$.
By Measurable Function is Simple Function iff Finite Image Set, $\Img f$ and $\Img g$ are finite.
Therefore, by Cardinality of Cartesian Product of Finite Sets, $\Img {\sequence {f, g} }$ is also finite.
Next, from {{Corollary|Image of Composite Mapping}}:
:$\Img {\innerprod f g \circ \Delta_X} \subseteq \Img {\innerprod f g}$
whence the former is finite.
Now $+$ is a surjection:
:$+: \Img {\innerprod f g \circ \Delta_X} \to \Img {f + g}$
by Restriction of Mapping to Image is Surjection.
By Cardinality of Codomain of Surjection, this implies that $\Img {f + g}$ is finite.
Whence Measurable Function is Simple Function iff Finite Image Set grants that $f + g$ is a simple function.
{{qed}}
Theorem: Pointwise Product of Simple Functions is Simple Function

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f, g : X \to \R$ be simple functions.
Then $f \cdot g: X \to \R, \map {\paren {f \cdot g} } x := \map f x \cdot \map g x$ is also a simple function.

Proof:
From Measurable Function is Simple Function iff Finite Image Set, it follows that there exist $x_1, \ldots, x_n$ and $y_1, \ldots y_m$ comprising the image of $f$ and $g$, respectively.
But then it immediately follows that any value attained by $f \cdot g$ is of the form $x_i \cdot y_j$.
Hence, there are at most $n \times m$ distinct values $f \cdot g$ can take.
From Pointwise Product of Measurable Functions is Measurable, $f \cdot g$ is also measurable.
{{CircularStructure}}
Hence by Measurable Function is Simple Function iff Finite Image Set, $f \cdot g$ is a simple function.
{{qed}}
Theorem: Positive Part of Simple Function is Simple Function

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f: X \to \R$ be a simple function.
Then $f^+: X \to \R$, the positive part of $f$, is also a simple function.

Proof:
Let $f$ have the following standard representation:
:$f = \ds \sum_{i \mathop = 0}^n a_i \chi_{E_i}$
Then we see that $f^+$ must satisfy:
:$f^+ = \ds \sum_{i \mathop = 0}^n \max \set {a_i, 0} \chi_{E_i}$
as the $E_i$ are disjoint, and $\chi_{E_i} \ge 0$ pointwise.
Since all of the $E_i$ are measurable, it follows that $f^+$ is a simple function.
{{qed}}
Theorem: Negative Part of Simple Function is Simple Function

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f: X \to \R$ be a simple function.
Then $f^-: X \to \R$, the negative part of $f$ is also a simple function.

Proof:
Let $f$ have the following standard representation:
:$f = \ds \sum_{i \mathop = 0}^n a_i \chi_{E_i}$
Then we see that $f^-$ must satisfy:
:$f^- = \ds \sum_{i \mathop = 0}^n \min \set {a_i, 0} \chi_{E_i}$
as the $E_i$ are disjoint, and $\chi_{E_i} \ge 0$ pointwise.
Since all of the $E_i$ are measurable, it follows that $f^+$ is a simple function.
{{qed}}
Theorem: Difference of Positive and Negative Parts

Let $X$ be a set, and let $f: X \to \overline{\R}$ be an extended real-valued function.
Let $f^+$, $f^-: X \to \overline{\R}$ be the positive and negative parts of $f$, respectively.
Then $f = f^+ - f^-$.

Proof:
Let $x \in X$. 
Consider the following four cases for the value of $\map f x$ in $\overline{\R}$:
$(1): \quad \map f x = -\infty$
: By ordering on extended reals:
::$\map {f^+} x = \map \max {0, \map f x} = \map \max {0, -\infty} = 0$
::$\map {f^-} x = - \map \min {0, \map f x} = - \map \min {0, -\infty} = +\infty$
: By extended real subtraction, it thus follows that:
::$\map {f^+} x - \map {f^-} x = 0 - \paren {+\infty} = - \infty = \map f x$
$(2): \quad \map f x \in \openint {-\infty} 0$
: Since $\map f x < 0$, it follows that:
::$\map {f^+} x = \map \max {0, \map f x} = 0$
::$\map {f^-} x = - \map \min {0, \map f x} = - \map f x$
: Thence it immediately follows that:
::$\map {f^+} x - \map {f^-} x = 0 - \paren {- \map f x} = \map f x$
$(3): \quad \map f x \in \hointr 0 {+\infty}$
: Since $\map f x \ge 0$, we obtain:
::$\map {f^+} x = \map \max {0, \map f x} = \map f x$
::$\map {f^-} x = - \min {0, \map f x} = 0$
: Then, these immediately imply:
::$\map {f^+} x - \map {f^-} x = \map f x - 0 = \map f x$
$(4): \quad \map f x = +\infty$
: By ordering on extended reals:
::$\map {f^+} x = \map \max {0, \map f x} = \map \max {0, +\infty} = +\infty$
::$\map {f^-} x = - \map \min {0, \map f x} = - \map \min {0, +\infty} = 0$
: By extended real subtraction, it now follows that:
::$\map {f^+} x - \map {f^-} x = +\infty - 0 = +\infty = \map f x$
In all cases, $\map {f^+} x - \map {f^-} x = \map f x$.
As $x \in X$ was arbitrary, we may conclude that:
:$\forall x \in X: \map {f^+} x - \map {f^-} x = \map f x$
That is, we have shown:
:$f = f^+ - f^-$
{{qed}}
Theorem: Sum of Positive and Negative Parts

Let $X$ be a set, and let $f: X \to \overline \R$ be an extended real-valued function.
Let $f^+, f^-: X \to \overline \R$ be the positive and negative parts of $f$, respectively.
Then $\size {f} = f^+ + f^-$, where $\size {f}$ is the absolute value of $f$.

Proof:
Let $x \in X$.
Suppose that $\map f x \ge 0$, where $\ge$ signifies the extended real ordering.
Then $\size {\map f x} = \map f x$, and:
:$\map {f^+} x = \map \max {\map f x, 0} = \map f x$
:$\map {f^-} x = - \map \min {\map f x, 0} = 0$
Hence $\map {f^+} x + \map {f^-} x = \map f x = \size {\map f x}$.
Next, suppose that $\map f x < 0$, again in the extended real ordering.
Then $\size {\map f x} = - \map f x$, and:
:$\map {f^+} x = \map \max {\map f x, 0} = 0$
:$\map {f^-} x = - \map \min {\map f x, 0} = - \map f x$
Hence $\map {f^+} x + \map {f^-} x = - \map f x = \size {\map f x}$.
Thus, for all $x \in X$:
:$\map {f^+} x + \map {f^-} x = \size {\map f x}$
That is, $f^+ + f^- = \size {f}$.
{{qed}}
Theorem: Absolute Value of Simple Function is Simple Function

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f: X \to \R$ be a simple function.
Then $\size f: X \to \R$, the absolute value of $f$, is also a simple function.

Proof:
By Sum of Positive and Negative Parts, we have:
:$\size f = f^+ + f^-$
We also have that Positive Part of Simple Function is Simple Function and Negative Part of Simple Function is Simple Function.
Hence $\size f$ is a pointwise sum of simple functions.
The result follows from Pointwise Sum of Simple Functions is Simple Function.
{{qed}}
Theorem: Absolute Value of Simple Function is Simple Function

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f: X \to \R$ be a simple function.
Then $\size f: X \to \R$, the absolute value of $f$, is also a simple function.

Proof:
By Simple Function has Standard Representation, $f$ has a standard representation, say:
:$(1): \quad f = \ds \sum_{k \mathop = 0}^n a_k \chi_{E_k}$
Then, for all $x \in X$:
:$\map {\size f} x = \ds \size {\sum_{k \mathop = 0}^n a_k \map {\chi_{E_k} } x}$
by definition of pointwise absolute value.
The fact that $(1)$ forms a standard representation ensures that for every $x \in X$, precisely one $k$ has $x \in E_k$.
Now suppose that $x \in E_l$. 
Then $\map {\chi_{E_l} } x = 0$ {{iff}} $k \ne l$ by definition of characteristic function.
It follows that $\map {\size f} x = \size {a_l \cdot 1} = \size {a_l}$.
Now define $g: X \to \R$ by:
:$\map g x := \ds \sum_{k \mathop = 0}^n \size {a_k} \map {\chi_{E_k} } x$
By construction, $g$ is a simple function, and for $x \in E_l$:
:$\map g x = \size {a_l}$
Thus, since every $x$ is in $E_l$ for precisely one $l$, it has been shown that $g = \size f$.
As $g$ was a simple function, it follows that $\size f$ is also a simple function.
{{qed}}
Theorem: Finite Cartesian Product of Non-Empty Sets is Non-Empty

Let $S_1, S_2, \ldots, S_n$ be non-empty sets.
Then their cartesian product $S_1 \times S_2 \times \cdots \times S_n$ is non-empty.

Proof:
We use mathematical induction.
The base case $n = 2$ is proved in Kuratowski Formalization of Ordered Pair, and the induction step follows directly from the definition of an ordered tuple.
{{qed}}
{{finish}}
Category:Cartesian Product
dmytyq44dk054dtplnkbkhl67vh1by6
Theorem: Equivalent Conditions for Dedekind-Infinite Set

For a set $S$, the following conditions are equivalent:
:$(1): \quad$ $S$ is Dedekind-infinite.
:$(2): \quad$ $S$ has a countably infinite subset.
The above equivalence can be proven in Zermelo-Fraenkel set theory.
If the axiom of countable choice is accepted, then it can be proven that the following condition is also equivalent to the above two:
:$(3): \quad$ $S$ is infinite.

Proof:
{{Tidy}}
{{MissingLinks}}
Theorem: Relation Isomorphism Preserves Reflexivity

Let $\struct {S, \RR_1}$ and $\struct {T, \RR_2}$ be relational structures.
Let $\struct {S, \RR_1}$ and $\struct {T, \RR_2}$ be (relationally) isomorphic.
Then $\RR_1$ is a reflexive relation {{iff}} $\RR_2$ is also a reflexive relation.

Proof:
{{WLOG}} it is necessary to prove only that if $\RR_1$ is reflexive then $\RR_2$ is reflexive.
Let $\phi: S \to T$ be a relation isomorphism.
Let $y \in T$.
Let $x = \map {\phi^{-1} } y$.
As $\phi$ is a bijection it follows from Inverse Element of Bijection that:
:$y = \map \phi x$
As $\RR_1$ is a reflexive relation it follows that:
:$x \mathrel {\RR_1} x$
As $\phi$ is a relation isomorphism it follows that:
:$\map \phi x \mathrel {\RR_2} \map \phi x$
Hence the result.
{{qed}}
Theorem: Preimage of Subset under Composite Mapping

Let $S_1, S_2, S_3$ be sets.
Let $f: S_1 \to S_2$ and $g: S_2 \to S_3$ be mappings.
Denote with $g \circ f: S_1 \to S_3$ the composition of $g$ and $f$.
Let $S_3' \subseteq S_3$ be a subset of $S_3$.
Then:
:$\paren {g \circ f}^{-1} \sqbrk {S_3'} = \paren {f^{-1} \circ g^{-1} } \sqbrk {S_3'}$
where $g^{-1} \sqbrk {S_3'}$ denotes the preimage of $S_3'$ under $g$.

Proof:
A mapping is a specific kind of relation.
Hence, Inverse of Composite Relation applies, and it follows that:
:$\paren {g \circ f}^{-1} \sqbrk {S_3'} = \paren {f^{-1} \circ g^{-1} } \sqbrk {S_3'}$
{{qed}}
Theorem: Preimage of Subset under Composite Mapping

Let $S_1, S_2, S_3$ be sets.
Let $f: S_1 \to S_2$ and $g: S_2 \to S_3$ be mappings.
Denote with $g \circ f: S_1 \to S_3$ the composition of $g$ and $f$.
Let $S_3' \subseteq S_3$ be a subset of $S_3$.
Then:
:$\paren {g \circ f}^{-1} \sqbrk {S_3'} = \paren {f^{-1} \circ g^{-1} } \sqbrk {S_3'}$
where $g^{-1} \sqbrk {S_3'}$ denotes the preimage of $S_3'$ under $g$.

Proof:
Let $x \in S_1$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \paren {g \circ f}^{-1} \sqbrk {S_3'}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \map {\paren {g \circ f} } x
      | o = \in
      | r = S_3'
      | c = {{Defof|Preimage of Subset under Mapping}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \map g {\map f x}
      | o = \in
      | r = S_3'
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \map f x
      | o = \in
      | r = g^{-1} \sqbrk {S_3'}
      | c = {{Defof|Preimage of Subset under Mapping}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = f^{-1} \sqbrk {g^{-1} \sqbrk {S_3'} }
      | c = {{Defof|Preimage of Subset under Mapping}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \paren {f^{-1} \circ g^{-1} } \sqbrk {S_3'}
      | c = {{Defof|Composition of Mappings}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Infinite Set has Countably Infinite Subset/Proof 4

If the axiom of countable choice is accepted, then it can be proven that every infinite set has a countably infinite subset.

Proof:
Let $S$ be an infinite set.
For all $n \in \N$, let:
:$\FF_n = \set {T \subseteq S: \size T = n}$
where $\size T$ denotes the cardinality of $T$.
From Set is Infinite iff exist Subsets of all Finite Cardinalities:
:$\FF_n$ is non-empty.
Using the axiom of countable choice, we can obtain a sequence $\sequence {S_n}_{n \mathop \in \N}$ such that $S_n \in \FF_n$ for all $n \in \N$.
Define:
:$\ds T = \bigcup_{n \mathop \in \N} S_n \subseteq S$
For all $n \in \N$, $S_n$ is a subset of $T$ whose cardinality is $n$.
From Set is Infinite iff exist Subsets of all Finite Cardinalities:
:$T$ is infinite.
From Countable Union of Countable Sets is Countable, $T$ is countable.
{{qed}}
Theorem: Set is Infinite iff exist Subsets of all Finite Cardinalities

A set $S$ is infinite {{iff}} for all $n \in \N$, there exists a subset of $S$ whose cardinality is $n$.

Proof:
Let the cardinality of a set $S$ be denoted $\card S$.
Theorem: Relation Isomorphism Preserves Symmetry

Let $\struct {S, \RR_1}$ and $\struct {T, \RR_2}$ be relational structures.
Let $\struct {S, \RR_1}$ and $\struct {T, \RR_2}$ be (relationally) isomorphic.
Then $\RR_1$ is a symmetric relation {{iff}} $\RR_2$ is also a symmetric relation.

Proof:
Let $\phi: S \to T$ be a relation isomorphism.
By Inverse of Relation Isomorphism is Relation Isomorphism it follows that $\phi^{-1}: T \to S$ is also a relation isomorphism.
{{WLOG}}, it suffices to prove only that if $\RR_1$ is symmetric, then also $\RR_2$ is symmetric.
So, suppose $\RR_1$ is a symmetric relation.
Let $y_1, y_2 \in T$ such that $y_1 \mathrel {\RR_2} y_2$.
Let $x_1 = \map {\phi^{-1} } {y_1}$ and $x_2 = \map {\phi^{-1} } {y_2}$.
As $\phi$ is a bijection it follows from Inverse Element of Bijection that $y_1 = \map \phi {x_1}$ and $y_2 = \map \phi {x_2}$.
As $\phi^{-1}$ is a relation isomorphism it follows that:
:$x_1 = \map {\phi^{-1} } {y_1} \mathrel {\RR_1} \map {\phi^{-1} } {y_2} = x_2$
As $\RR_1$ is a symmetric relation it follows that:
:$x_2 \mathrel {\RR_1} x_1$
As $\phi$ is a relation isomorphism it follows that:
:$y_2 = \map \phi {x_2} \mathrel {\RR_2} \map \phi {x_1} = y_1$
So:
:$y_1 \mathrel {\RR_2} y_2 \implies y_2 \mathrel {\RR_2} y_1$
and so by definition $\RR_2$ is a symmetric relation.
Hence the result.
{{qed}}
Theorem: Set Difference with Proper Subset

Let $S$ be a set.
Let $T \subsetneq S$ be a proper subset of $S$.
Let $S \setminus T$ denote the set difference between $S$ and $T$.
Then:
:$S \setminus T \ne \O$
where $\O$ denotes the empty set.

Proof:
{{AimForCont}} $S \setminus T = \O$.
Then:
:$\not \exists x \in S: x \notin T$
By De Morgan's laws:
:$\forall x \in S: x \in T$
By definition of subset:
:$S \subseteq T$
By definition of proper subset, we have that $T \subseteq S$ such that $T \ne S$.
But we have $T \subseteq S$ and $S \subseteq T$.
So by definition of set equality:
:$S = T$
From this contradiction it follows that:
:$S \setminus T \ne \O$
{{qed}}
Category:Set Difference
Category:Proper Subsets
h1fl0uijajl0e3472yoj0hv188r7n8a
Theorem: Order Isomorphism iff Strictly Increasing Surjection

Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be totally ordered sets.
A mapping $\phi: \struct {S, \preceq_1} \to \struct {T, \preceq_2}$ is an order isomorphism {{iff}}:
:$(1): \quad \phi$ is a surjection
:$(2): \quad \forall x, y \in S: x \mathop {\prec_1} y \implies \map \phi x \mathop {\prec_2} \map \phi y$

Proof:
=== Necessary Condition ===
Let $\phi: \struct {S, \preceq_1} \to \struct {T, \preceq_2}$ be an order isomorphism.
Then by definition $\phi$ is a bijection and so a surjection.
Suppose $x \mathop {\prec_1} y$.
That is:
:$x \mathop {\preceq_1} y$
:$x \ne y$
Then:
:$x \mathop {\prec_1} y \implies \map \phi x \mathop {\preceq_2} \map \phi y$
as $\phi$ is an order isomorphism.
But as $\phi$ is a bijection it is also an injection.
Thus:
:$\map \phi x = \map \phi y \implies x = y$
and so it follows that:
:$x \mathop {\prec_1} y \implies \map \phi x \mathop {\prec_2} \map \phi y$
{{qed|lemma}}
Theorem: Relation Isomorphism Preserves Transitivity

Let $\struct {S, \RR_1}$ and $\struct {T, \RR_2}$ be relational structures.
Let $\struct {S, \RR_1}$ and $\struct {T, \RR_2}$ be (relationally) isomorphic.
Then $\RR_1$ is a transitive relation {{iff}} $\RR_2$ is a transitive relation.

Proof:
Let $\phi: S \to T$ be a relation isomorphism.
By Inverse of Relation Isomorphism is Relation Isomorphism it follows that $\phi^{-1}: T \to S$ is also a relation isomorphism.
{{WLOG}}, it is therefore sufficient to prove only that if $\RR_1$ is transitive, then $\RR_2$ is also transitive.
So, suppose $\RR_1$ is a transitive relation.
Let $y_1, y_2, y_3 \in T$ such that $y_1 \mathrel {\RR_2} y_2$ and $y_2 \mathrel {\RR_2} y_3$.
Let $x_1 = \map {\phi^{-1} } {y_1}$, $x_2 = \map {\phi^{-1} } {y_2}$ and $x_3 = \map {\phi^{-1} } {y_3}$.
As $\phi$ is a bijection it follows from Inverse Element of Bijection that:
:$y_1 = \map \phi {x_1}$
:$y_2 = \map \phi {x_2}$
:$y_3 = \map \phi {x_3}$
As $\phi^{-1}$ is a relation isomorphism it follows that:
:$x_1 = \map {\phi^{-1} } {y_1} \mathrel {\RR_1} \map {\phi^{-1} } {y_2} = x_2$
:$x_2 = \map {\phi^{-1} } {y_2} \mathrel {\RR_1} \map {\phi^{-1} } {y_3} = x_3$
As $\RR_1$ is a transitive relation it follows that:
:$x_1 \mathrel {\RR_1} x_3$
As $\phi$ is a relation isomorphism it follows that:
:$y_1 = \map \phi {x_1} \mathrel {\RR_2} \map \phi {x_3} = y_3$
Hence if $y_1 \mathrel {\RR_2} y_2$ and $y_2 \mathrel {\RR_2} y_3$, then also:
:$y_1 \mathrel {\RR_2} y_3$
Hence, $\RR_2$ is a transitive relation, by definition.
Hence the result.
{{qed}}
Theorem: Relation Isomorphism Preserves Antisymmetry

Let $\struct {S, \RR_1}$ and $\struct {T, \RR_2}$ be relational structures.
Let $\struct {S, \RR_1}$ and $\struct {T, \RR_2}$ be (relationally) isomorphic.
Then $\RR_1$ is an antisymmetric relation {{iff}} $\RR_2$ is also an antisymmetric relation.

Proof:
Let $\phi: S \to T$ be a relation isomorphism.
By Inverse of Relation Isomorphism is Relation Isomorphism it follows that $\phi^{-1}: T \to S$ is also a relation isomorphism.
{{WLOG}}, it therefore suffices to prove only that if $\RR_1$ is antisymmetric, then also $\RR_2$ is antisymmetric.
So, suppose $\RR_1$ is an antisymmetric relation.
Let $y_1, y_2 \in T$ such that both $y_1 \mathrel {\RR_2}, y_2$ and $y_2 \mathrel {\RR_2} y_1$.
Let $x_1 = \map {\phi^{-1} } {y_1}$ and $x_2 = \map {\phi^{-1} } {y_2}$.
As $\phi$ is a bijection it follows from Inverse Element of Bijection that $y_1 = \map \phi {x_1}$ and $y_2 = \map \phi {x_2}$.
As $\phi^{-1}$ is a relation isomorphism it follows that:
:$x_1 = \map {\phi^{-1} } {y_1} \mathrel {\RR_1} \map {\phi^{-1} } {y_2} = x_2$
:$x_2 = \map {\phi^{-1} } {y_2} \mathrel {\RR_1} \map {\phi^{-1} } {y_1} = x_1$
As $\RR_1$ is an antisymmetric relation it follows that $x_1 = x_2$.
As $\phi$ is a bijection it follows that:
:$y_1 = \map \phi {x_1} = \map \phi {x_2} = y_2$
Hence $y_1 = y_2$ and so by definition, $\RR_2$ is an antisymmetric relation.
Hence the result.
{{qed}}