avewright/proofwiki-math huggingface dataset:
Theorem: Element of Ordinal is Ordinal

Let $n$ be an ordinal.
Let $m \in n$.
Then $m$ is also an ordinal.
That is, the class of all ordinals $\On$ is a transitive class.

Proof:
Let $\On$ denote the class of all ordinals.
From Class of All Ordinals is Minimally Superinductive over Successor Mapping, $\On$ is superinductive.
By Zero is Smallest Ordinal, $0$ is the smallest element of $\On$.
We identify the natural number $0$ via the von Neumann construction of the natural numbers as:
:$0 := \O$
Vacuously, every element of $\O$ is an ordinal.
{{qed|lemma}}
Let $\alpha \in \On$ be an ordinal.
Let us assume that every element of $\alpha$ is an ordinal.
Let $\alpha^+$ denote the successor to $\alpha$.
Because $\On$ is superinductive:
:$\alpha \in \On \implies \alpha^+ \in \On$
By definition of successor mapping:
:$\alpha^+ = \alpha \cup \set \alpha$
Then every element of $\alpha^+$ is either an element of $\alpha$ or $\alpha$ itself.
We have {{hypothesis}} that:
:$\alpha$ is an ordinal
:every element of $\alpha$ is an ordinal.
That is, $\alpha^+$ is an ordinal.
{{qed|lemma}}
Let $C$ be a chain of ordinals such that:
:each element $\alpha$ of $C$ has the property that each element of $\alpha$ is itself an ordinal.
Let $\beta \in \bigcup C$.
Then $\beta \in \alpha$ for some $\alpha \in C$.
Hence, by definition of $C$, $\beta$ is an ordinal which has the property that each element of $\beta$ is itself an ordinal.
It follows by the Principle of Superinduction that every element of an ordinal is an ordinal.
{{qed|lemma}}
Let $\alpha \in \On$ be an arbitrary ordinal.
Let $\beta \subseteq \alpha$.
From Class of All Ordinals is Well-Ordered by Subset Relation, $\beta$ is an ordinal
Hence from the above:
:$\beta \in \alpha$
As $\alpha$ is arbitrary:
:$\forall \alpha \in \On: \beta \subseteq \alpha \implies \beta \in \alpha$
proving that $\On$ is transitive.
{{qed}}
Theorem: Element of Ordinal is Ordinal

Let $n$ be an ordinal.
Let $m \in n$.
Then $m$ is also an ordinal.
That is, the class of all ordinals $\On$ is a transitive class.

Proof:
By the definition of ordinal, $n$ is transitive.
Thus $m \subseteq n$.
By Restriction of Strict Well-Ordering is Strict Well-Ordering, it follows that $m$ is strictly well-ordered by the epsilon restriction $\Epsilon {\restriction_m}$.
It is now to be shown that $m$ is transitive.
If $m = \O$ then the result follows by Empty Class is Transitive.
If $m \ne \O$, then let $x \in m$.
If $x = \O$, then $x \subseteq m$ by Empty Set is Subset of All Sets.
If $x \ne \O$, then let $y \in x$.
It suffices to show that $y \in m$.
Since $m \subseteq n$, it follows that $x \in n$.
Also, $y \in x \land x \in n \implies y \in n$ because $n$ is transitive.
And so $x \in n$, $y \in n$, and $m \in n$.
A strict well-ordering is transitive by definition.
Therefore:
:$y \in x \land x \in m \implies y \in m$
Hence the result.
{{qed}}
Theorem: Modulus of Exponential of Imaginary Number is One

Let $\cmod z$ denote the modulus of a complex number $z$.
Let $e^z$ be the complex exponential of $z$.
Let $x$ be wholly real.
Then:
:$\cmod {e^{i x} } = 1$

Proof:
{{begin-eqn}}
{{eqn | l = e^{i x}
      | r = \cos x + i \sin x
      | c = Euler's Formula
}}
{{eqn | ll= \leadsto
      | l = \cmod {e^{i x} }
      | r = \cmod {\cos x + i \sin x}
}}
{{eqn | r = \sqrt {\paren {\map \Re {\cos x + i \sin x} }^2 + \paren {\map \Im {\cos x + i \sin x} }^2}
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | r = \sqrt {\cos^2 x + \sin^2 x}
      | c = as $x$ is wholly real
}}
{{eqn | r = 1
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
{{qed}}
Category:Complex Modulus
Category:Modulus of Exponential of Imaginary Number is One
4e54obxfjkhpr31zu5htm7dromjp3mj
Theorem: Absolute Value of Power

Let $x$, $y$ be real numbers.
Let $x^y$, $x$ to the power of $y$, be real.
Then:
:$\size {x^y} = \size x^y$

Proof:
If $x = 0$, the theorem clearly holds, by the definition of powers of zero.
Suppose $x \ne 0$.
We use the interpretation of real numbers as wholly real complex numbers.
Likewise we interpret the absolute value of $x$ as the modulus of $x$.
Then $x$ can be expressed in polar form:
:$x = r e^{i\theta}$
where $r = \size x$ and $\theta$ is an argument of $x$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = r e^{i\theta}
}}
{{eqn | ll= \leadsto
      | l = x^y
      | r = \left(r{e^{i\theta} }\right)^y
}}
{{eqn | r = r^y e^{i \theta y}
}}
{{eqn | ll= \leadsto
      | l = \size {x^y}
      | r = \size {r^y e^{i \theta y} }
}}
{{eqn | r = \size {r^y} \size {e^{i \theta y} }
      | c = Modulus of Product
}}
{{eqn | r = \size {r^y}
      | c = Modulus of Exponential of Imaginary Number is One
}}
{{eqn | r = \size {\size x^y}
      | c = by definition of $r$
}}
{{eqn | r = \size x^y
      | c = as $\size x^y \ge 0$
}}
{{end-eqn}}
{{qed}}
{{MissingLinks|exponential properties for $\C$ and that $\size x^y \ge 0$}}
Category:Absolute Value Function
g0rl07jenlyqentmmvi3q5l1rpraizk
Theorem: Count of Rows of Truth Table

Let $P$ be a WFF of propositional logic.
Suppose $\PP$ is of finite size such that it contains $n$ different letters.
Then a truth table constructed to express $P$ will contain $2^n$ rows.

Proof:
In a truth table, one row is needed for each boolean interpretation of $P$.
Let $S$ be the set of different letters used in $P$.
The result then follows from applying Number of Boolean Interpretations for Finite Set of Variables to $S$.
{{qed}}
Theorem: Equivalence of Definitions of Transitive Closure of Set

Let $x$ and $y$ be sets.
{{TFAE|def = Transitive Closure of Set}}

Proof:
Let $x^t$ be the transitive closure of $x$ by Definition 2.
Let the mapping $G$ be defined as on that definition page.
Theorem: Denumerable Class is Set

Let $A$ be a class.
Let $\N$ be the natural numbers.
Suppose that $F: \N \to A$ is a bijection.
Then $A$ is a set.

Proof:
By the Axiom of Infinity, $\N$ is a set.
Thus by the Axiom of Replacement, $A$ is also a set.
{{qed}}
Category:Set Theory
5hmyb1p303uf7bgmuq7hv5xmn9nuw12
Theorem: Relative Complement inverts Subsets

Let $S$ be a set.
Let $A \subseteq S, B \subseteq S$ be subsets of $S$.
Then:
:$A \subseteq B \iff \relcomp S B \subseteq \relcomp S A$
where $\complement_S$ denotes the complement relative to $S$.

Proof:
{{begin-eqn}}
{{eqn | l = A
      | o = \subseteq
      | r = B
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = A \cap B
      | r = A
      | c = Intersection with Subset is Subset
}}
{{eqn | ll= \leadstoandfrom
      | l = \relcomp S {A \cap B}
      | r = \relcomp S A
      | c = Relative Complement of Relative Complement
}}
{{eqn | ll= \leadstoandfrom
      | l = \relcomp S A \cup \relcomp S B
      | r = \relcomp S A
      | c = De Morgan's Laws: Relative Complement of Intersection
}}
{{eqn | ll= \leadstoandfrom
      | l = \relcomp S B
      | o = \subseteq
      | r = \relcomp S A
      | c = Union with Superset is Superset
}}
{{end-eqn}}
{{qed}}
Theorem: Union of Subsets is Subset/Family of Sets

Let $\family {S_i}_{i \mathop \in I}$ be a family of sets indexed by $I$.
Then for all sets $X$:
:$\ds \paren {\forall i \in I: S_i \subseteq X} \implies \bigcup_{i \mathop \in I} S_i \subseteq X$
where $\ds \bigcup_{i \mathop \in I} S_i$ is the union of $\family {S_i}$.

Proof:
Suppose that $\forall i \in I: S_i \subseteq X$.
Consider any $\ds x \in \bigcup_{i \mathop \in I} S_i$.
By definition of set union:
:$\exists i \in I: x \in S_i$
But as $S_i \subseteq X$ it follows that $x \in X$.
Thus it follows that:
:$\ds \bigcup_{i \mathop \in I} S_i \subseteq X$
So:
:$\ds \paren {\forall i \in I: S_i \subseteq X} \implies \bigcup_{i \mathop \in I} S_i \subseteq X$
{{qed}}
Theorem: Set Union is Self-Distributive/Sets of Sets

Let $A$ and $B$ denote sets of sets.
Then:
:$\ds \bigcup \paren {A \cup B} = \paren {\bigcup A} \cup \paren {\bigcup B}$
where $\ds \bigcup A$ denotes the union of $A$.

Proof:
Let $\ds s \in \bigcup \paren {A \cup B}$.
Then by definition of union of set of sets:
:$\exists X \in A \cup B: s \in X$
By definition of set union, either:
:$X \in A$
or:
:$X \in B$
If $X \in A$, then:
:$s \in \set {x: \exists X \in A: x \in X}$
If $X \in B$, then:
:$s \in \set {x: \exists X \in B: x \in X}$
Thus by definition of union of set of sets, either:
:$\ds s \in \bigcup A$
or:
:$\ds s \in \bigcup B$
So by definition of set union:
:$\ds s \in \paren {\bigcup A} \cup \paren {\bigcup B}$
So by definition of subset:
:$\ds \bigcup \paren {A \cup B} \subseteq \paren {\bigcup A} \cup \paren {\bigcup B}$
Now let $\ds s \in \paren {\bigcup A} \cup \paren {\bigcup B}$.
By definition of set union, either:
:$\ds s \in \bigcup A$
or:
:$\ds s \in \bigcup B$
That is, by definition of union of set of sets, either:
:$s \in \set {x: \exists X \in A: x \in X}$
or:
:$s \in \set {x: \exists X \in B: x \in X}$
{{WLOG}}, let $s \in X$ such that $X \in A$.
Then by Set is Subset of Union:
:$s \in X$ such that $X \in A \cup B$
That is:
:$\ds s \in \bigcup \paren {A \cup B}$
Similarly if $x \in X$ such that $X \in B$.
So by definition of subset:
:$\ds \paren {\bigcup A} \cup \paren {\bigcup B} \subseteq \bigcup \paren {A \cup B}$
Hence by definition of equality of sets:
:$\ds \bigcup \paren {A \cup B} = \paren {\bigcup A} \cup \paren {\bigcup B}$
{{qed}}
Category:Set Union is Self-Distributive
o34przogjvuqtzn52esyn1qn9jtt7iu
Theorem: Set Union is Self-Distributive/Families of Sets

Let $I$ be an indexing set.
Let $\family {A_\alpha}_{\alpha \mathop \in I}$ and $\family {B_\alpha}_{\alpha \mathop \in I}$ be indexed families of subsets of a set $S$.
Then:
:$\ds \map {\bigcup_{\alpha \mathop \in I} } {A_\alpha \cup B_\alpha} = \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cup \paren {\bigcup_{\alpha \mathop \in I} B_\alpha}$
where $\ds \bigcup_{\alpha \mathop \in I} A_\alpha$ denotes the union of $\family {A_\alpha}_{\alpha \mathop \in I}$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \map {\bigcup_{\alpha \mathop \in I} } {A_\alpha \cup B_\alpha}
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists \beta \in I
      | l = x
      | o = \in
      | r = A_\beta \cup B_\beta
      | c = {{Defof|Union of Family}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = A_\beta
      | c = {{Defof|Set Union}}
}}
{{eqn | lo= \lor
      | l = x
      | o = \in
      | r = B_\beta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \bigcup_{\alpha \mathop \in I} A_\alpha
      | c = Set is Subset of Union of Family
}}
{{eqn | lo= \lor
      | l = x
      | o = \in
      | r = \bigcup_{\alpha \mathop \in I} B_\alpha
      | c = Set is Subset of Union of Family
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cup \paren {\bigcup_{\alpha \mathop \in I} B_\alpha}
      | c = {{Defof|Set Union}}
}}
{{end-eqn}}
Thus by definition of subset:
:$\ds \map {\bigcup_{\alpha \mathop \in I} } {A_\alpha \cup B_\alpha} \subseteq \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cup \paren {\bigcup_{\alpha \mathop \in I} B_\alpha}$
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cup \paren {\bigcup_{\alpha \mathop \in I} B_\alpha}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \bigcup_{\alpha \mathop \in I} A_\alpha
      | c = {{Defof|Set Union}}
}}
{{eqn | lo= \lor
      | l = x
      | o = \in
      | r = \bigcup_{\alpha \mathop \in I} B_\alpha
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists \beta \in I
      | l = x
      | o = \in
      | r = A_\beta
      | c = {{Defof|Union of Family}}
}}
{{eqn | lo= \lor
      | q = \exists \beta \in I
      | l = x
      | o = \in
      | r = B_\beta
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists \beta \in I
      | l = x
      | o = \in
      | r = A_\beta \cup B_\beta
      | c = {{Defof|Union of Family}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \map {\bigcup_{\alpha \mathop \in I} } {A_\alpha \cup B_\alpha}
      | c = 
}}
{{end-eqn}}
Thus by definition of subset:
:$\ds \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cup \paren {\bigcup_{\alpha \mathop \in I} B_\alpha} \subseteq \map {\bigcup_{\alpha \mathop \in I} } {A_\alpha \cup B_\alpha}$
{{qed|lemma}}
By definition of set equality:
:$\ds \map {\bigcup_{\alpha \mathop \in I} } {A_\alpha \cup B_\alpha} = \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cup \paren {\bigcup_{\alpha \mathop \in I} B_\alpha}$
{{qed}}
Theorem: Set Intersection is Self-Distributive/General Result

Let $\family {\mathbb S_i} _{i \mathop \in I}$ be an $I$-indexed family of sets of sets.
Then:
:$\ds \bigcap_{i \mathop \in I} \bigcap \mathbb S_i = \bigcap \bigcap_{i \mathop \in I} \mathbb S_i$

Proof:
{{proof wanted}}
Category:Set Intersection is Self-Distributive
f94t9xyxs3xx1tcjhcxqv6dbdajy8fj
Theorem: Intersection Distributes over Union/Family of Sets

Let $I$ be an indexing set.
Let $\family {A_\alpha}_{\alpha \mathop \in I}$ be a indexed family of subsets of a set $S$.
Let $B \subseteq S$.
Then:
:$\ds \map {\bigcup_{\alpha \mathop \in I} } {A_\alpha \cap B} = \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cap B$
where $\ds \bigcup_{\alpha \mathop \in I} A_\alpha$ denotes the union of $\family {A_\alpha}_{\alpha \mathop \in I}$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \bigcup_{\alpha \mathop \in I} \paren {A_\alpha \cap B}
      | c =
}}
{{eqn | ll= \leadsto
      | q = \exists \alpha \in I
      | l = x
      | o = \in
      | r = A_\alpha \cap B
      | c = {{Defof|Union of Family}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = A_\alpha
      | c = {{Defof|Set Intersection}}
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \paren {\bigcup_{\alpha \mathop \in I} A_\alpha}
      | c = Set is Subset of Union of Family
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cap B
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
By definition of subset:
:$\ds \bigcup_{\alpha \mathop \in I} \paren {A_\alpha \cap B} \subseteq \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cap B$
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cap B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \paren {\bigcup_{\alpha \mathop \in I} A_\alpha}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = B
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists \alpha \in I
      | l = x
      | o = \in
      | r = A_\alpha
      | c = {{Defof|Union of Family}}
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = B
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists \alpha \in I
      | l = x
      | o = \in
      | r = A_\alpha \cap B
      | c = {{Defof|Set Intersection}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \bigcup_{\alpha \mathop \in I} \paren {A_\alpha \cap B}
      | c = Set is Subset of Union of Family
}}
{{end-eqn}}
By definition of subset:
:$\ds \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cap B \subseteq \map {\bigcup_{\alpha \mathop \in I} } {A_\alpha \cap B}$
{{qed|lemma}}
By definition of set equality:
:$\ds\map {\bigcup_{\alpha \mathop \in I} } {A_\alpha \cap B} = \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cap B$
{{qed}}
Theorem: Union Distributes over Intersection/Family of Sets

Let $I$ be an indexing set.
Let $\family {A_\alpha}_{\alpha \mathop \in I}$ be an indexed family of subsets of a set $S$.
Let $B \subseteq S$.
Then:
:$\ds \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cup B} = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cup B$
where $\ds \bigcap_{\alpha \mathop \in I} A_\alpha$ denotes the intersection of $\family {A_\alpha}_{\alpha \mathop \in I}$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cup B}
      | c =
}}
{{eqn | ll= \leadsto
      | q = \forall \alpha \in I
      | l = x
      | o = \in
      | r = A_\alpha \cup B
      | c = Intersection is Subset
}}
{{eqn | ll= \leadsto
      | q = \forall \alpha \in I
      | l = x
      | o = \in
      | r = A_\alpha
      | c = {{Defof|Set Union}}
}}
{{eqn | lo= \lor
      | l = x
      | o = \in
      | r = B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha}
      | c = {{Defof|Intersection of Family}}
}}
{{eqn | lo= \lor
      | l = x
      | o = \in
      | r = B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cup B
      | c = {{Defof|Set Union}}
}}
{{end-eqn}}
By definition of subset:
:$\ds \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cup B} \subseteq \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cup B$
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cup B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha}
      | c = {{Defof|Set Union}}
}}
{{eqn | lo= \lor
      | l = x
      | o = \in
      | r = B
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall \alpha \in I
      | l = x
      | o = \in
      | r = A_\alpha
      | c = Intersection is Subset
}}
{{eqn | lo= \lor
      | l = x
      | o = \in
      | r = B
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall \alpha \in I
      | l = x
      | o = \in
      | r = A_\alpha \cup B
      | c = {{Defof|Set Union}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cup B}
      | c = {{Defof|Intersection of Family}}
}}
{{end-eqn}}
By definition of subset:
:$\ds \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cup B \subseteq \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cup B}$
{{qed|lemma}}
By definition of set equality:
:$\ds \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cup B} = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cup B$
{{qed}}
Theorem: Equivalence of Definitions of Well-Ordering

{{TFAE|def = Well-Ordering}}
Let $\struct {S, \preceq}$ be a ordered set.

Proof:
=== Definition 1 implies Definition 2 ===
{{:Equivalence of Definitions of Well-Ordering/Definition 1 implies Definition 2}}
By hypothesis, every subset of $S$ has a smallest element.
By Smallest Element is Minimal it follows that every subset of $S$ has a minimal element.
Thus it follows that $\preceq$ is a well-ordering on $S$ by definition 2.
{{qed|lemma}}
Theorem: Equivalence of Definitions of Transitive Closure of Relation/Finite Chain is Smallest

Let $S$ be a set or class.
Let $\RR$ be a relation on $S$.
Let $\RR^+$ be the transitive closure of $\RR$ by the finite chain definition.
That is, for $x, y \in S$ let $x \mathrel {\RR^+} y$ {{iff}} for some natural number $n > 0$ there exist $s_0, s_1, \dots, s_n \in S$ such that $s_0 = x$, $s_n = y$, and:
:$\forall k \in \N_n: s_k \mathrel \RR s_{k + 1}$
Then $\RR^+$ is transitive and if $\QQ$ is a transitive relation on $S$ such that $\RR \subseteq \QQ$ then $\RR \subseteq \QQ$.

Proof:
==== $\RR^+$ is transitive ====
Let $x, y, z \in S$.
Let $x \mathrel {\RR^+} y$ and $y \mathrel {\RR^+} z$.
Then for some $m, n \in \N_{>0}$ there are $s_0, s_1, \dots, s_m$ and $t_0, t_1, \dots, t_n$ such that $s_0 = x$, $s_m = y$, $t_0 = y$, $t_n = z$, and the following hold:
:$\forall k \in \N_m: s_k \mathrel {\RR^+} s_{k + 1}$
:$\forall k \in \N_n: t_k \mathrel {\RR^+} t_{k + 1}$
Let $\sequence {u_k}_{k \mathop \in \N_{m + n} }$ be defined thus:
:$u_k = \cases {s_k & \text {if $k \le m$} \\ t_{k - m} & \text {if $k > m$} }$
Then clearly $u_k \mathrel {\RR^+} u_{k + 1}$ whenever $k < m$ and whenever $k > m$.
But $u_m = s_m = y = t_0 \mathrel {\RR^+} t_1 = u_{m + 1}$, so this holds also for $k = m$.
Furthermore, $u_0 = s_0 = x$ and $u_{m + n} = t_n = z$.
Therefore $x \mathrel {\RR^+} z$.
As this holds for all such $x$ and $z$, $\RR^+$ is transitive.
{{qed|lemma}}
Theorem: Order-Preserving Bijection on Wosets is Order Isomorphism

Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be well-ordered sets.
Let $\phi: S \to T$ be a bijection such that $\phi: S \to T$ is order-preserving:
:$\forall x, y \in S: x \preceq_1 y \implies \map \phi x \preceq_2 \map \phi y$
Then:
:$\forall x, y \in S: \map \phi x \preceq_2 \map \phi y \implies x \preceq_1 y$
That is, $\phi: S \to T$ is an order isomorphism.

Proof:
A well-ordered set is a totally ordered set by definition.
A bijection is a surjection by definition.
The result follows from Order Isomorphism iff Strictly Increasing Surjection.
{{qed}}
Category:Well-Orderings
Category:Order Isomorphisms
bd9m2xcftcxo5aowtn8z62ncldgdsm8
Theorem: Inverse Image of Set under Set-Like Relation is Set

Let $A$ be a class.
Let $\RR$ be a set-like endorelation on $A$.
Let $B \subseteq A$ be a set.
Then $\map {\RR^{-1} } B$, the inverse image of $B$ under $\RR$, is also a set.

Proof:
Since $\RR$ is set-like, $\map {\RR^{-1} } {\set x}$ is a set for each $x$ in $A$.
As $B \subseteq A$, this holds also for each $x \in B$.
{{explain|Explain better.}}
But then $\ds \map {\RR^{-1} } B = \bigcup_{x \mathop \in B} \map {\RR^{-1} } {\set x}$, which is a set by the Axiom of Unions.
{{qed}}
Category:Set Theory
mhc0n5hvhy7ydj1m5rlh03fdo6oo4k8
Theorem: Reciprocal of Holomorphic Function

Let $f: \C \to \C$ be a complex function.
Let $U \subseteq \C$ be an open set such that $f$ has no zeros in $U$.
Suppose further that $f$ is holomorphic in $U$.
Then the complex function
:$\dfrac 1 {f_{\restriction U} } : U \to \C$
is holomorphic.

Proof:
Let $g: U \to \C$ be such that $\map g x = 1 / \map f x$.
Since $\map f x$ is nonzero for $x \in U$, $g$ is well-defined.
By Quotient Rule for Continuous Complex Functions, $g$ is continuous.
Let $z_0 \in U$.
As $g$ is continuous:
:$\ds \lim_{h \mathop \to 0} \frac 1 {\map f {z_0 + h} } = \frac 1 {\map f {z_0} }$
As $f$ is holomorphic:
:$\ds \lim_{h \mathop \to 0} \frac {\map f {z_0 + h} - \map f {z_0} } h = \map {f'} {z_0}$
By the Combination Theorem for Limits of Complex Functions:
{{begin-eqn}}
{{eqn | l = \lim_{h \mathop \to 0} \frac {\map g {z_0 + h} - \map g {z_0} } h
      | r = \lim_{h \mathop \to 0} \frac {\frac 1 {\map f {z_0 + h} } - \frac 1 {\map f {z_0} } } h
}}
{{eqn | r = -\frac 1 {\map f {z_0} } \lim_{h \mathop \to 0} \paren {\paren {\frac 1 {\map f {z_0 + h} } } \paren {\frac {\map f {z_0 + h} - \map f {z_0} } h} }
}}
{{eqn | r = -\frac 1 {\map f {z_0}^2} \cdot \map {f'} {z_0}
}}	
{{end-eqn}}
It follows that $g$ is holomorphic.
{{qed}}
Category:Holomorphic Functions
Category:Reciprocals
7vtylob45oscyg2qu3jkpnphyqf0yqr