avewright/proofwiki-math huggingface dataset:
Theorem: Square Number Less than One

Let $x$ be a real number such that $x^2 < 1$.
Then:
:$x \in \openint {-1} 1$
where $\openint {-1} 1$ is the open interval $\left\{{x \in \R: -1 < x < 1}\right\}$.

Proof:
First note that from Square of Real Number is Non-Negative:
:$x^2 \ge 0$
From Ordering of Squares in Reals:
:$(1): \quad x > 1 \implies x^2 > 1$
:$(2): \quad x < 1 \implies x^2 < 1$
From Identity Element of Multiplication on Numbers:
:$1^2 = 1$
so it is clear that the strict inequalities apply above.
For clarity, therefore, the case where $x = \pm 1$ can be ignored.
Suppose $x \notin \openint {-1} 1$.
Then either:
:$x < -1$
or:
:$x > 1$
If $x > 1$ then:
:$x^2 > 1$
If $x < -1$ then:
:$-x > 1$
From Square of Real Number is Non-Negative:
:$\paren {-x}^2 = x^2$
So again $x^2 > 1$.
Thus:
:$x \notin \openint {-1} 1 \implies x^2 > 1$
So by the Rule of Transposition:
:$x^2 < 1 \implies x \in \openint {-1} 1$
{{qed}}
Category:Real Analysis
ng4q181lfb3d96oods9e0vvprk2kyox
Theorem: Uniform Limit Theorem

Let $\struct {M, d_M}$ and $\struct {N, d_N}$ be metric spaces.
Let $\sequence {f_n}$ be a sequence of mappings from $M$ to $N$ such that:
:$(1): \quad \forall n \in \N: f_n$ is continuous at every point of $M$
:$(2): \quad \sequence {f_n}$ converges uniformly to $f$
Then:
:$f$ is continuous at every point of $M$.

Proof:
Let $a \in M$.
We are given that $d_N$ is a metric on $N$.
By applying {{Metric-space-axiom|2}} twice:
{{begin-eqn}}
{{eqn | n = 3
      | q = \forall n \in \N, \forall x \in M
      | l = \map {d_N} {\map f x, \map f a}
      | o = \le
      | r = \map {d_N} {\map f x, \map {f_n} x} + \map {d_N} {\map {f_n} x, \map {f_n} a} + \map {d_N} {\map {f_n} a, \map f a}
}}
{{end-eqn}}
Let $\epsilon \in \R_{>0}$.
Since $\sequence {f_n}$ converges uniformly to $f$:
{{begin-eqn}}
{{eqn | n = 4 a
      | q = \exists \NN \in \R_{>0}: \forall n \in \N_{>\NN}: \forall x \in M
      | l = \map {d_N} {\map f x, \map {f_n} x}
      | o = <
      | r = \frac \epsilon 3
}}
{{eqn | n = 4 b
      | ll= \leadsto
      | q = \exists \NN \in \R_{>0}: \forall n \in \N_{>\NN}
      | l = \map {d_N} {\map f a, \map {f_n} a}
      | o = <
      | r = \frac \epsilon 3
      | c = Universal Instantiation of $x$
}}
{{end-eqn}}
We are given that $\forall n \in \N: f_n$ is continuous.
Hence:
{{begin-eqn}}
{{eqn | n = 5
      | q = \forall n \in \N: \exists \delta \in \R_{>0}: \forall x \in M
      | l = \map {d_M} {x, a}
      | o = <
      | r = \delta
}}
{{eqn | ll= \implies
      | l = \map {d_N} {\map {f_n} x, \map {f_n} a}
      | o = <
      | r = \frac \epsilon 3
}}
{{end-eqn}}
Combining $(3)$, $\text {(4 a)}$, $\text {(4 b)}$ and $(5)$:
{{begin-eqn}}
{{eqn | q = \exists \NN \in \R_{>0}: \forall n \in \N_{>\NN}: \exists \delta \in \R_{>0}: \forall x \in M
      | l = \map {d_M} {x, a}
      | o = <
      | r = \delta
}}
{{eqn | ll= \implies
      | l = \map {d_N} {\map f x, \map f a}
      | o = <
      | r = \frac \epsilon 3 + \frac \epsilon 3 + \frac \epsilon 3
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}
As $a$ and $\epsilon$ are arbitrary, it follows by Universal Instantiation of $n$ that:
{{begin-eqn}}
{{eqn | q = \forall a \in M: \forall \epsilon \in \R_{>0}: \exists \delta \in \R_{>0}: \forall x \in M
      | l = \map {d_M} {x, a}
      | o = <
      | r = \delta
}}
{{eqn | ll= \implies
      | l = \map {d_N} {\map f x, \map f a}
      | o = <
      | r = \epsilon
}}
{{end-eqn}}
Hence, $f$ is continuous at every point of $M$.
{{qed}}
Theorem: Equality is Transitive

:$\forall a, b, c: \paren {a = b} \land \paren {b = c} \implies a = c$

Proof:
{{begin-eqn}}
{{eqn | l = a
      | r = b
      | c = 
}}
{{eqn | ll= \vdash
      | l = \map P a
      | o = \iff
      | r = \map P b
      | c = Leibniz's law
}}
{{eqn | l = b
      | r = c
      | c = 
}}
{{eqn | ll= \vdash
      | l = \map P b
      | o = \iff
      | r = \map P c
      | c = Leibniz's law
}}
{{eqn | ll= \vdash
      | l = \map P a
      | o = \iff
      | r = \map P c
      | c = Biconditional is Transitive
}}
{{eqn | ll= \vdash
      | l = a
      | r = c
      | c = Leibniz's law
}}
{{end-eqn}}
{{qed}}
Theorem: Axiom of Pairing from Infinity and Replacement

The Axiom of Pairing is a consequence of:
:the Axiom of Infinity
and
:the Axiom of Replacement.

Proof:
The set $2 = \set {\O, \set \O}$ is used with the Axiom of Replacement as the domain for a mapping whose image is $\set {A, B}$.
A suitable mapping would be:
:$\paren {y = \O \land z = A} \lor \paren {y = \set \O \land z = B}$
The set $2$ is shown to exist as a member of the infinite set whose existence is asserted by the axiom of infinity.
{{qed}}
Category:Axiom of Pairing
Category:Doubletons
cnmivoukhqhrjdynhgrzl3kcs3ajaf7
Theorem: Axiom of Pairing from Powers and Replacement

The {{axiom-link|Pairing|Set Theory}} is a consequence of:
:the {{axiom-link|the Empty Set|Set Theory}}
and
:the {{axiom-link|Powers|Set Theory}}
and also
:the {{axiom-link|Replacement}}.

Proof:
It is to be shown that $2 = \set {\O, \set \O}$ is a set.
By the {{axiom-link|the Empty Set|Set Theory}}, it is seen that $\O$ is a set.
By the {{axiom-link|Powers|Set Theory}}, it is seen that $\powerset \O$ is also a set.
It is to be shown that $\powerset \O = \set \O$.
To determine the elements of $\powerset \O$, we must find all of the sets $z$ such that:
:$\forall x: x \in z \implies x \in \O$
From the definition of the empty set, the {{RHS}} of this expression is invariably false.
So by Rule of Transposition, we deduce that:
:$\forall x: x \notin z$
But this is the definition of the empty set.
So by Empty Set is Unique, it follows that $\powerset \O = \set \O$.
{{qed|lemma}}
It is now to be shown that $\powerset {\set \O} = \set {\O, \set \O}$.
By Empty Set is Subset of All Sets, $\O \in \powerset {\set \O}$.
By Set is Subset of Itself, $\set \O \in \powerset {\set \O}$.
And so:
:$(1) \quad \set {\O, \set \O} \subseteq \powerset {\set \O}$
It is now to be shown that $\set {\O, \set \O} \supseteq \powerset {\set \O}$.
{{AimForCont}} that there exists a set $S \in \powerset {\set \O}$ such that $S \ne \O$ and $S \ne \set \O$.
But then $\exists x \ne \O: x \in \set \O$, which is false.
Therefore by contradiction:
:$(2) \quad \powerset {\set \O} \subseteq \set {\O, \set \O}$.
Putting $(1)$ and $(2)$ together yields:
:$\powerset {\set \O} = \set {\O, \set \O}$
{{qed|lemma}}
The set $2 = \set {\O, \set \O}$ is used with the {{axiom-link|Replacement}} as the domain for a mapping whose image is $\set {A, B}$.
A suitable mapping would be:
:$\paren {y = \O \land z = A} \lor \paren {y = \set \O \land z = B}$
Usually this mapping would be written as:
:$\map f x = \begin{cases}
A & : x = \O \\
B & : x = \set \O
\end{cases}$
{{qed}}
Category:Axiom of Pairing
Category:Doubletons
pgqe4219kkktcyjqzwwt0iank1nk2ke
Theorem: Axiom of Pairing from Axiom of Specification

Let it be supposed that there exists a set which contains at least two elements.
Then the Axiom of Pairing is a consequence of the Axiom of Specification.

Proof:
Let $A$ be a set which contains at least two elements.
Let $a$ and $b$ be any two elements of $A$.
Let $\map P x$ be the propositional function:
:$\map P x := \paren {x = a \lor x = b}$
Then we may use the Axiom of Specification to define $B$ as:
:$x \in B \iff \set {x \in A: \map P x}$
Hence we can define:
:$B := \set {a, b}$
for any two $a, b \in A$.
{{qed}}
Theorem: Existence of Singleton Set

Let $a$ be a set.
Then the singleton set $\set a$ may be constructed such that:
:$a \in \set a$

Proof:
Let $a$ be a set.
From the Axiom of Pairing the set $\set {a, a}$ may be formed.
From the Axiom of Extension it follows that:
:$\set {a, a} = \set a$
{{qed}}
Theorem: Intersection is Subset of Union of Intersections with Complements

Let $R, S, T$ be sets.
Then:
:$S \cap T \subseteq \paren {R \cap S} \cup \paren {\overline R \cap T}$
where $\overline R$ denotes the complement of $R$.

Proof:
Let $x \in S \cap T$.
Then by definition of set intersection, $x \in S \land x \in T$.
From Conjunction implies Disjunction of Conjunctions with Complements, it follows that:
:$\paren {x \in S \land \psi} \lor \paren {x \in T \land \neg \psi}$
where $\psi$ is any arbitrary statement.
Let $\psi$ be the statement $x \in R$.
Thus:
:$\paren {x \in S \land x \in T} \implies \paren {x \in S \land x \in R} \lor \paren {x \in T \land x \notin R}$
By definition of subset, set intersection, set union and set complement, it follows that:
:$S \cap T \subseteq \paren {R \cap S} \cup \paren {\overline R \cap T}$
{{qed}}
Theorem: Intersection of Unions with Complements is Subset of Union

Let $R, S, T$ be sets.
Then:
:$\left({R \cup S}\right) \cap \left({\overline R \cup T}\right) \subseteq S \cup T$

Proof:
Let $x \in \left({R \cup S}\right) \cap \left({\overline R \cup T}\right)$.
Then by definition of set intersection, set union and set complement, we have:
:$\left({x \in R \lor x \in S}\right) \land \left({x \notin R \lor x \in T}\right)$
From Conjunction of Disjunctions with Complements implies Disjunction it follows that:
:$x \in S \lor x \in T$
By definition of set union, it follows that:
:$x \in S \cup T$
By definition of subset it follows that:
:$\left({R \cup S}\right) \cap \left({\overline R \cup T}\right) \subseteq S \cup T$
{{qed}}
Theorem: Conjunction implies Disjunction of Conjunctions with Complements

:$p \land q \vdash \paren {p \land r} \lor \paren {q \land \neg r}$

Proof:
{{BeginTableau|p \land q \vdash \paren {p \land r} \lor \paren {q \land \neg r} }}
{{Premise|1|p \land q}}
{{ExcludedMiddle|2|r \lor \neg r}}
{{Simplification|3|1|p|1|1}}
{{Simplification|4|1|q|1|2}}
{{Assumption|5|r}}
{{Conjunction|6|1, 5|p \land r|1|5}}
{{Addition|7|1, 5|\paren {p \land r} \lor \paren {q \land \neg r}|6|1}}
{{Assumption|8|\neg r}}
{{Conjunction|9|1, 8|q \land \neg r|4|8}}
{{Addition|10|1, 8|\paren {p \land r} \lor \paren {q \land \neg r}|9|2}}
{{ProofByCases|11|1|\paren {p \land r} \lor \paren {q \land \neg r}|2|5|7|8|10}}
{{EndTableau|qed}}
{{LEM||3}}
Category:Conjunction
Category:Disjunction
oqhq5eseiy7xvt7xjd5wa6pl20e9qv4
Theorem: Conjunction of Disjunctions with Complements implies Disjunction

:$\paren {p \lor r} \land \paren {q \lor \neg r} \vdash p \lor q$

Proof:
{{BeginTableau|\paren {p \lor r} \land \paren {q \lor \neg r} \vdash p \lor q}}
{{Premise|1|\paren {p \lor r} \land \paren {q \lor \neg r} }}
{{Simplification|2|1|p \lor r|1|1|The aim is to use Proof by Cases on this ...}}
{{Assumption|3|p|Assume the first of the disjuncts ...}}
{{Addition|4|3|p \lor q|3|1|... and demonstrate the conclusion}}
{{Simplification|5|1|q \lor \neg r|1|2}}
{{Commutation|6|1|\neg r \lor q|5|Disjunction}}
{{SequentIntro|7|1|r \implies q|6|Rule of Material Implication}}
{{Assumption|8|r| then assume the second of the disjuncts ...}}
{{ModusPonens|9|1, 8|q|7|8}}
{{Addition|10|1, 8|p \lor q|9|2|... and demonstrate the conclusion}}
{{ProofByCases|11|1|p \lor q|2|3|4|8|10}}
{{EndTableau|qed}}
Category:Conjunction
Category:Disjunction
h1it43fjat3r0s3jo9va85i82aqh799
Theorem: Intersection of Elements of Power Set

Let $S$ be a set.
Let:
:$\ds \mathbb S = \bigcap_{X \mathop \in \powerset S} X$
where $\powerset S$ is the power set of $S$.
Then $\mathbb S = \O$.

Proof:
By Intersection is Subset:
:$\ds \forall X \in \powerset S: \bigcap_{X \mathop \in \powerset S} X \subseteq X$
From Empty Set is Element of Power Set:
:$\O \in \powerset S$
So:
:$\ds \bigcap_{X \mathop \in \powerset S} X \subseteq \O$
From Empty Set is Subset of All Sets:
:$\ds \O \subseteq \bigcap_{X \mathop \in \powerset S} X$
So by definition of set equality:
:$\ds \bigcap_{X \mathop \in \powerset S} X = \O$
{{qed}}
Theorem: Power Set of Subset

Let $S \subseteq T$ where $S$ and $T$ are both sets.
Then:
:$\powerset S \subseteq \powerset T$
where $\powerset S$ denotes the power set of $S$.

Proof:
{{begin-eqn}}
{{eqn | l = X
      | o = \in
      | r = \powerset S
      | c =
}}
{{eqn | ll= \leadsto
      | l = X
      | o = \subseteq
      | r = S
      | c = {{Defof|Power Set}}
}}
{{eqn | ll= \leadsto
      | l = X
      | o = \subseteq
      | r = T
      | c = as $S \subseteq T$: Subset Relation is Transitive
}}
{{eqn | l = X
      | o = \in
      | r = \powerset T
      | c = {{Defof|Power Set}}
}}
{{end-eqn}}
{{qed}}
Theorem: Union of Elements of Power Set

Let $S$ be a set.
Then:
:$\ds S = \bigcup_{X \mathop \in \powerset S} X$
where $\powerset S$ denotes the power set of $S$.

Proof:
By Subset of Union:
:$\ds \forall X \in \powerset S: X \subseteq \bigcup_{X \mathop \in \powerset S} X$
From Set is Subset of Itself, $S \subseteq S$ and so $S \in \powerset S$.
So:
:$\ds S \subseteq \bigcup_{X \mathop \in \powerset S} X$
From Union is Smallest Superset:
:$\ds \paren {\forall X \in \mathbb S: X \subseteq T} \iff \bigcup \mathbb S \subseteq T$
where $\mathbb S \subseteq \powerset S$.
But as $\powerset S \subseteq \powerset S$ from Set is Subset of Itself:
:$\ds \paren {\forall X \in \powerset S: X \subseteq S} \iff \bigcup \powerset S \subseteq S$
The {{LHS}} is no more than the definition of the power set, making it a tautological statement, and so:
:$\ds \bigcup \powerset S \subseteq S$
The result follows by definition of set equality.
{{qed}}
Theorem: Subset of Cartesian Product

Let $S$ be a set of ordered pairs.
Then $S$ is the subset of the cartesian product of two sets.

Proof:
Let $S$ be a set of ordered pairs.
Let $x \in S$ such that $x = \set {\set a, \set {a, b} }$ as defined in Kuratowski Formalization of Ordered Pair.
Since the elements of $S$ are sets, we can form the union $\mathbb S = \bigcup S$ of the sets in $S$.
Since $x \in S$ it follows that the elements of $x$ are elements of $\mathbb S$.
Since $\set {a, b} \in x$ it follows that $\set {a, b} \in \mathbb S$.
Now we can form the union $\mathbb S' = \bigcup \mathbb S$ of the sets in $\mathbb S$.
Since $\set {a, b} \in \mathbb S$ it follows that both $a$ and $b$ are elements of $\mathbb S' = \bigcup \bigcup S$.
Thus from the Kuratowski Formalization of Ordered Pair we have that $S$ is a subset of some $A \times B$.
We can at this stage take both $A$ and $B$ as being equal to $\bigcup \bigcup S$.
Finally, the axiom of specification is applied to construct the sets:
:$A = \set {a: \exists b: \tuple {a, b} \in S}$
and
:$B = \set {b: \exists a: \tuple {a, b} \in S}$
$A$ and $B$ are seen to be the first and second projections respectively of $S$.
{{qed}}
Theorem: Diagonal Relation is Smallest Equivalence Relation

The diagonal relation $\Delta_S$ on $S$ is the smallest equivalence in $S$, in the sense that:
:$\forall \EE \subseteq S \times S: \Delta_S \subseteq \EE$
where $\EE$ denotes a general equivalence relation.

Proof:
It is confirmed that, from Diagonal Relation is Equivalence, $\Delta_S$ is an equivalence relation.
Let $\EE$ be an arbitrary equivalence relation.
By definition, $\EE$ is reflexive.
From Relation Contains Diagonal Relation iff Reflexive it follows that as $\Delta_S \subseteq \EE$.
{{qed}}
Theorem: Trivial Relation is Largest Equivalence Relation

The trivial relation $\TT$ on $S$ is the largest equivalence in $S$, in the sense that:
:$\forall \EE \subseteq S \times S: \EE \subseteq \TT$
where $\EE$ denotes a general equivalence relation.

Proof:
The trivial relation $\TT$ on $S$ is defined as:
:$\TT = S \times S$
It is confirmed from Trivial Relation is Equivalence that the trivial relation is in fact an equivalence relation.
Let $\EE$ be an arbitrary equivalence relation on $S$.
By definition of relation, $\EE \subseteq S \times S$ and so (trivially) $\EE \subseteq \TT$.
{{qed}}
Theorem: Continuously Differentiable Curve has Finite Arc Length

Let $y = \map f x$ be a real function which is continuous on the closed interval $\closedint a b$ and continuously differentiable on the open interval $\openint a b$.
The definite integral: 
:$s = \ds \int_{x \mathop = a}^{x \mathop = b} \sqrt {1 + \paren {\frac {\d y} {\d x} }^2} \rd x$
exists, and is called the '''arc length''' of $f$ between $a$ and $b$.

Proof:
It intuitively makes sense to define the length of a line segment to be the distance between the two end points, as given by the Distance Formula:
:$\sqrt {\paren {x_1 - x_2}^2 + \paren {y_1 - y_2}^2}$
Similarly, it is reasonable to assume that the actual length of the curve would be approximately equal to the sum of the lengths of each of the line segments, as shown:
400px
{{handwaving|The intuitive arguments need to be replaced with something more rigorous, which would probably happen on another page and be linked.}}
To calculate the sum of the length of these line segments, divide $\closedint a b$ into any number of closed subintervals of the form $\closedint {x_{i - 1} } {x_i}$ where:
:$a = x_0 < x_1 < \dotsb < x_{k - 1} < x_k = b$
Define:
:$\Delta x_i = x_i - x_{i - 1}$
:$\Delta y_i = y_i - y_{i - 1}$
As the length of the $i$th line segment is $\sqrt {\paren {\Delta x_i}^2 + \paren {\Delta y_i}^2}$, the sum of all these line segments is given by:
:$\ds \sum_{i \mathop = 1}^k \ \sqrt {\paren {\Delta x_i}^2 + \paren {\Delta y_i}^2}$
{{begin-eqn}}
{{eqn | r = \sum_{i \mathop = 1}^k \ \sqrt {\paren {\Delta x_i}^2 + \paren {\frac {\Delta y_i} {\Delta x_i} {\Delta x_i} }^2}
      | c = multiply the second term in the radicand by $1 = \dfrac {\Delta x_i} {\Delta x_i}$
}}
{{eqn | r = \sum_{i \mathop = 1}^k \ \sqrt {1 + \paren {\frac {\Delta y_i} {\Delta x_i} }^2} \Delta x_i
      | c = factor $\Delta x_i$ out of the radicand
}}
{{end-eqn}}
Thus the approximate arc length is given by the sum:
:$\ds s \approx \sum_{i \mathop = 1}^k \sqrt {1 + \paren {\frac {\Delta y_i} {\Delta x_i} }^2}\Delta x_i$
Recall that by hypothesis:
:$f$ is continuous on $\closedint a b$
:$f$ is differentiable on $\openint a b$.
Thus the Mean Value Theorem can be applied.
In every open interval $\openint {x_i} {x_{i - 1} }$ there exists some $c_i$ such that:
:$D_x \, \map f {c_i} = \dfrac {\Delta y_i} {\Delta x_i}$
Plugging this into the above sum we have:
:$\ds s \approx \sum_{i \mathop = 1}^k \ \sqrt {1 + \paren {\frac {\d y} {\d x} }^2} \Delta x_i$
By hypothesis, $D_x f$ is continuous.
As Square of Real Number is Non-Negative the radicand is always positive.
From Continuity of Root Function and Limit of Composite Function, $\sqrt {1 + \paren {\dfrac {\d y} {\d x} }^2}$ is continuous as well.
Because Continuous Real Function is Darboux Integrable, there exists a definite integral that confirms the intuitive notion that there is a value that represents the exact length of the curve as the limit of the above Riemann sum.
This definite integral is:
:$\ds s = \int_{x \mathop = a}^{x \mathop = b} \sqrt {1 + \paren {\frac {\d y} {\d x} }^2} \rd x$
{{qed}}
Theorem: Arc Length for Parametric Equations

Let $x = \map f t$ and $y = \map g t$ be real functions of a parameter $t$. 
Let these equations describe a curve $\CC$ that is continuous for all $t \in \closedint a b$ and continuously differentiable for all $t \in \openint a b$.
Suppose that the graph of the curve does not intersect itself for any $t \in \openint a b$.
Then the arc length of $\CC$ between $a$ and $b$ is given by:
:$\ds s = \int_a^b \sqrt {\paren {\frac {\d x} {\d t} }^2 + \paren {\frac {\d y} {\d t} }^2} \rd t$
for $\dfrac {\d x} {\d t} \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = s
      | r = \int_a^b \sqrt {1 + \paren {\frac {\d y} {\d x} }^2} \rd x
      | c = {{Defof|Arc Length}}
}}
{{eqn | r = \int_a^b \sqrt {\paren {\frac {\frac {\d x} {\d t} } {\frac {\d x} {\d t} } }^2 + \paren {\frac {\frac {\d y}{\d t} } {\frac {\d x} {\d t} } }^2} \rd x
      | c = because $\paren {\dfrac {\frac {\d x} {\d t} } {\frac {\d x}{\d t} } }^2 = 1$, and from {{Corollary|Derivative of Composite Function}}
}}
{{eqn | r = \int_a^b \sqrt {\paren {\frac {\d x} {\d t} }^2 + \paren {\frac {\d y} {\d t} }^2} \paren {\frac 1 {\frac {\d x} {\d t} } } \rd x
      | c = factoring $\dfrac {\d x} {\d t}$ out of the radicand. No absolute value is needed as length cannot be negative.
}}
{{eqn | r = \int_a^b \sqrt {\paren {\frac {\d x} {\d t} }^2 + \paren {\frac {\d y} {\d t} }^2} \frac {\d t} {\d x} \rd x
      | c = Derivative of Inverse Function
}}
{{eqn | r = \int_a^b \sqrt {\paren {\frac {\d x} {\d t} }^2 + \paren {\frac {\d y} {\d t} }^2} \rd t
      | c = Integration by Substitution
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Element of Injection

Let $S$ and $T$ be sets.
Let $f: S \to T$ be an injection.
Then:
:$\map {f^{-1} } y = x \iff \map f x = y$

Proof:
=== Necessary Condition ===
Let $y = \map f x$.
From the definition of the preimage of an element:
:$\map {f^{-1} } y = \set {x \in S: \tuple {y, x} \in f}$
Thus:
:$x \in \map {f^{-1} } y$
By definition of injection, $\map {f^{-1} } y$ is a singleton:
:$\map {f^{-1} } y = \set x$
which can be expressed as:
:$\map {f^{-1} } y = x$
{{qed|lemma}}
Theorem: Intersection of Inductive Sets

Let $\mathbb S$ be a non-empty indexed family of inductive sets.
Then $\bigcap \mathbb S$ is an inductive set.

Proof:
From definition, a set $X$ is an inductive set {{iff}} both the following holds:
:$\O \in X$
:$x \in X \implies x^+ \in X$
For all $S \in \mathbb S$, $S$ is an inductive set.
From definition of an inductive set, $\O \in S$.
By definition of set intersection, $\O \in \bigcap \mathbb S$.
Now suppose $x \in \bigcap \mathbb S$.
By definition of set intersection:
:$\forall S \in \mathbb S: x \in S$
Hence from definition of an inductive set, $x^+ \in S$.
By definition of set intersection, $x^+ \in \bigcap \mathbb S$.
Therefore $\bigcap \mathbb S$ is an inductive set.
{{qed}}
Theorem: Minimally Inductive Set Exists

There exists a minimally inductive set $\omega$ that is a subset of every other inductive set.

Proof:
From the Axiom of Infinity, there is a set $S$ such that:
:$\O \in S$
:$x \in S \implies x^+ \in S$
where $\O$ denotes the empty set and $x^+$ is the successor set of $x$.
That is, there exists an inductive set.
Next, by the Axiom of Specification, the minimally inductive set $\omega$:
:$\omega := \ds \bigcap \set {S' \subseteq S: \text{$S'$ is an inductive set} }$
exists.
It remains to be shown that if $T$ is an inductive set, then $\omega \subseteq T$.
By Intersection of Inductive Sets, $S \cap T$ is an inductive set.
Moreover, by Intersection is Subset, $S \cap T$, so that:
:$S \cap T \in \set {S' \subseteq S: \text{$S'$ is an inductive set} }$
from which we conclude by definition of $\omega$ and Intersection is Subset: General Result that:
:$\omega \subseteq S \cap T \subseteq T$
as desired.
{{qed}}
Theorem: Minimally Inductive Set forms Peano Structure

Let $\omega$ be the minimally inductive set.
Let $\cdot^+: \omega \to \omega$ be the mapping assigning to a set its successor set:
:$n^+ := n \cup \set n$
Let $\O \in \omega$ be the empty set.
Then $\struct {\omega, \cdot^+, \O}$ is a Peano structure.

Proof:
We need to check that all of Peano's axioms hold for $\struct {\omega, \cdot^+, \O}$.
Suppose first that for $m, n \in \omega$, we have $m^+ = n^+$.
Since $n \in n^+$ it follows that $n \in m^+$.
Hence, either $n \in m$ or $n = m$.
Similarly, either $m \in n$ or $m = n$.
Now if $n \ne m$, both $m \in n$ and $n \in m$.
By Element of Minimally Inductive Set is Transitive Set, it follows that $n \subseteq m$.
As $m \in n$, this contradicts Finite Ordinal is not Subset of one of its Elements.
Hence it must be that $n = m$, and {{PeanoAxiom|3}} holds.
Next, since $n \in n^+$ for all $n \in \omega$, it follows that $n^+ \ne \O$.
Hence, {{PeanoAxiom|4}} holds as well.
Finally, let $S \subseteq \omega$ satisfy:
:$\O \in S$
:$\forall n \in S: n^+ \in S$
Then by definition, $S$ is an inductive set.
Therefore, by definition of $\omega$ as the minimally inductive set:
:$\omega \subseteq S$
Consequently $S = \omega$ by the definition of set equality.
Thus {{PeanoAxiom|5}} is seen to hold.
That is, $\struct {\omega, \cdot^+, \O}$ is a Peano structure.
{{qed}}