avewright/proofwiki-math huggingface dataset:
Theorem: Abel's Test

Let $\ds \sum b_n$ be a convergent real series.
Let $\sequence {a_n}$ be a decreasing sequence of positive real numbers.
Then the series $\ds \sum a_n b_n$ is also convergent.

Proof:
{{MissingLinks|throughout}}
Let $b_0 = 0$.
Let $B_N = \ds \sum_{k \mathop = 0}^N b_k$.
Then: 
:$\forall n \ge 1: b_n = B_n − B_{n − 1}$
From Abel's Lemma:
$\ds \sum_{k \mathop = 1}^N a_k b_k = \sum_{k \mathop = 1}^{N - 1} B_k \paren {a_k - a_{k + 1} } + a_N B_N$
By the Monotone Convergence Theorem:
:$\sequence {a_n}$ converges
:$\sequence {B_N}$ converges since $\ds \sum b_n$ converges.
Hence the second addend $a_N B_N$ converges.
It remains to prove the first addend $\ds \sum B_k \paren {a_k − a_{k + 1} }$ converges.
Since $\sequence {B_N}$ converges, $\size {B_N} \le M$ for some $M \in \N$.
{{begin-eqn}}
{{eqn | l = \sum_1^N \size {B_k \paren {a_k -a_{k + 1} } }
      | o = \le
      | r = M \sum_1^N \size {a_k - a_{k + 1} }
}}
{{eqn | r =  M \size {a_1 - a_{N + 1} }
      | c = as $\sequence {a_n}$ is decreasing
}}
{{eqn | o = \to
      | r = M \size {a_1 - a}
      | c = as $a_k \to a$
}}
{{end-eqn}}
Hence $\ds \sum B_k \paren {a_k − a_{k + 1} }$ converges absolutely.
Hence $\ds \sum a_n b_n$ converges.
{{qed}}
{{Namedfor|Niels Henrik Abel|cat = Abel}}
Theorem: Abel's Test for Uniform Convergence

Let $\sequence {\map {a_n} z}$ and $\sequence {\map {b_n} z}$ be sequences of complex functions on a compact set $K$.
Let $\sequence {\map {a_n} z}$ be such that:
:$\sequence {\map {a_n} z}$ is bounded in $K$
:$\ds \sum \size {\map {a_n} z - \map {a_{n + 1} } z}$ is convergent with a sum which is bounded in $K$
:$\ds \sum \map {b_n} z$ is uniformly convergent in $K$.
Then $\ds \sum \map {a_n} z \map {b_n} z$ is uniformly convergent on $K$.

Proof:
{{tidy|Use {{ProofWiki}} templates in order to make this page readable}}
{{MissingLinks|throughout}}
{{ProofWanted}}
First we modify the statement of Abel's Lemma
Theorem: Equivalence of Definitions of Topology Generated by Synthetic Basis/Definition 1 iff Definition 2

Let $S$ be a set.
Let $\BB$ be a synthetic basis on $S$.
Let $\tau$ be the topology on $S$ generated by the synthetic basis $\BB$:
:$\ds \tau = \set {\bigcup \AA: \AA \subseteq \BB}$
Then:
:$\ds \forall U \subseteq S: U \in \tau \iff U = \bigcup \set {B \in \BB: B \subseteq U}$

Proof:
Trivially, the reverse implication holds, as $\set {B \in \BB: B \subseteq U} \subseteq \BB$.
We now show that the forward implication holds.
Suppose $U \in \tau$.
Then, by definition:
:$\ds \exists \AA \subseteq \BB: U = \bigcup \AA$
By Union is Smallest Superset: General Result:
:$\forall B \in \AA: B \subseteq U$
By definition of subset, it follows that:
:$\AA \subseteq \set {B \in \BB: B \subseteq U}$
From Union of Subset of Family is Subset of Union of Family:
:$\ds U = \bigcup \AA \subseteq \bigcup \set {B \in \BB: B \subseteq U}$
By Union is Smallest Superset: General Result:
:$\ds \bigcup \set {B \in \BB: B \subseteq U} \subseteq U$
By definition of set equality:
:$\ds U = \bigcup \set {B \in \BB: B \subseteq U}$
Theorem: Equivalence of Definitions of Topology Generated by Synthetic Basis/Definition 1 iff Definition 3

Let $S$ be a set.
Let $\BB$ be a synthetic basis on $S$.
Let $\tau$ be the topology on $S$ generated by the synthetic basis $\BB$:
:$\ds \tau = \set {\bigcup \AA: \AA \subseteq \BB}$
Then:
:$\forall U \subseteq S: U \in \tau \iff \forall x \in U: \exists B \in \BB: x \in B \subseteq U$

Proof:
From Set is Subset of Union: General Result, the forward implication directly follows.
We now show that the reverse implication holds.
By hypothesis, we have that:
:$\ds U \subseteq \bigcup \set {B \in \BB: B \subseteq U}$
By Union is Smallest Superset: General Result:
:$\ds \bigcup \set {B \in \BB: B \subseteq U} \subseteq U$
By definition of set equality:
:$\ds U = \bigcup \set {B \in \BB: B \subseteq U}$
The result follows.
Theorem: Projection from Product Topology is Open and Continuous

Let $T_1 = \struct {S_1, \tau_1}$ and $T_2 = \struct {S_2, \tau_2}$ be topological spaces.
Let $T = \struct {T_1 \times T_2, \tau}$ be the product space of $T_1$ and $T_2$, where $\tau$ is the product topology on $S$.
Let $\pr_1: T \to T_1$ and $\pr_2: T \to T_2$ be the first and second projections from $T$ onto its factors.
Then both $\pr_1$ and $\pr_2$ are open and continuous.

Proof:
=== Projection is Continuous ===
{{:Projection from Product Topology is Continuous}}{{qed|lemma}}
Theorem: Projection from Product Topology is Open and Continuous/General Result

Let $\family {T_i}_{i \mathop \in I} = \family {\struct {S_i, \tau_i} }_{i \mathop \in I}$ be an indexed family of topological spaces where $I$ is an arbitrary index set.
Let $\ds S = \prod_{i \mathop \in I} S_i$ be the corresponding product space.
Let $\tau$ denote the product topology on $S$.
Let $\pr_i: S \to S_i$ be the corresponding projection from $S$ onto $S_i$.
Then $\pr_i$ is open and continuous for all $i \in I$.

Proof:
=== Projection is Continuous ===
{{:Projection from Product Topology is Continuous/General Result/Proof}}{{qed|lemma}}
Theorem: Projection from Product Topology is Continuous/General Result

Let $\family {T_i}_{i \mathop \in I} = \family {\struct{S_i, \tau_i} }_{i \mathop \in I}$ be an indexed family of topological spaces where $I$ is an arbitrary index set.
Let $\ds S = \prod_{i \mathop \in I} S_i$ be the corresponding product space.
Let $\tau$ denote the Tychonoff topology on $S$.
Let $\pr_i: S \to S_i$ be the corresponding projection from $S$ onto $S_i$.
Then $\pr_i$ is continuous for all $i \in I$.

Proof:
By definition of the product topology on $S$:
:$\tau$ is the initial topology on $S$ with respect to $\family {\pr_i}_{i \mathop \in I}$
By definition of the Initial Topoplogy: Definition 2:
:$\tau$ is the coarsest topology on $S$ such that each $\pr_i: S \to S_i$ is a $\struct{\tau, \tau_i}$-continuous.
Theorem: Projection from Product Topology is Open/General Result

Let $\family {T_i}_{i \mathop \in I} = \family {\struct {S_i, \tau_i} }_{i \mathop \in I}$ be an indexed family of topological spaces where $I$ is an arbitrary index set.
Let $\ds S = \prod_{i \mathop \in I} S_i$ be the corresponding product space.
Let $\tau$ denote the product topology on $S$.
Let $\pr_i: S \to S_i$ be the corresponding projection from $S$ onto $S_i$.
Then $\pr_i$ is open for all $i \in I$.

Proof:
Let $U \in \tau$.
It follows from the definition of product topology that $U$ can be expressed as:
:$\ds U = \bigcup_{j \mathop \in J} \bigcap_{k \mathop = 1}^{n_j} \map {\pr_{i_{k, j} }^{-1} } {U_{k, j} }$
where:
:$J$ is an arbitrary index set
:$n_j \in \N$
:$i_{k, j} \in I$
:$U_{k, j} \in \tau_{i_{k, j} }$.
For all $i' \in I$, define $V_{i', k, j} \in \tau_{i'}$ by:
:$V_{i', k, j} = \begin {cases} U_{k, j} & : i' = i_{k, j} \\ S_{i'} & : i' \ne i_{k, j} \end {cases}$
For all $i \in I$, we have:
{{begin-eqn}}
{{eqn | l = \map {\pr_i} U
      | r = \bigcup_{j \mathop \in J} \map {\pr_i} {\bigcap_{k \mathop = 1}^{n_j} \map {\pr_{i_{k,j} }^{-1} } { U_{k,j} } }
      | c = Image of Union under Relation: Family of Sets
}}
{{eqn | r = \bigcup_{j \mathop \in J} \map {\pr_i} {\bigcap_{k \mathop = 1}^{n_j} \prod_{i' \mathop \in I} V_{i', k, j} }
      | c = {{Defof|Projection (Mapping Theory)|Projection}}
}}
{{eqn | r = \bigcup_{j \mathop \in J} \map {\pr_i} {\prod_{i' \mathop \in I} \bigcap_{k \mathop = 1}^{n_j} V_{i', k, j} }
      | c = Cartesian Product of Intersections: General Case
}}
{{eqn | r = \bigcup_{j \mathop \in J} \bigcap_{k \mathop = 1}^{n_j} V_{i,k,j}
      | c = {{Defof|Projection (Mapping Theory)|Projection}}
}}
{{end-eqn}}
As:
:$\ds \bigcup_{j \mathop \in J} \bigcap_{k \mathop = 1}^{n_j} V_{i, k, j} \in \tau_i$
it follows that $\pr_i$ is open.
Theorem: Product Space Basis Induced from Factor Space Bases

Let $\family {\struct{S_\alpha, \tau_\alpha} }_{\alpha \mathop \in I}$ be an indexed family of topological spaces for $\alpha$ in some indexing set $I$.
Let $\BB_\alpha$ be a basis for the topology $\tau_\alpha$ for each $\alpha \in I$.
Let $\struct {S, \tau} = \ds \prod_{\alpha \mathop \in I} \struct {S_\alpha, \tau_\alpha}$ be the product space of $\family {\struct {S_\alpha, \tau_\alpha} }_{\alpha \mathop \in I}$.
Let $\BB$ be the set of all cartesian products of the form $\ds \prod_{\alpha \mathop \in I} U_\alpha$ where:
:for all but finitely many indices $\alpha : U_\alpha = S_\alpha$
:for all $\alpha \in I : U_\alpha \ne S_\alpha \implies U_\alpha \in \BB_\alpha$
Then $\BB$ is a basis for the topology on the product space $\struct{S, \tau}$.

Proof:
Let $x = \family {x_\alpha}_{\alpha \mathop \in I} \in S$.
Let $W \in \tau$ such that $x \in W$.
From Natural Basis of Product Topology, the set $\BB'$ of cartesian products of the form $\ds \prod_{\alpha \mathop \in I} V_\alpha$ where:
:for all $\alpha \in I : V_\alpha \in \tau_\alpha$
:for all but finitely many indices $\alpha : V_\alpha = X_\alpha$
is a basis for $\tau$.
Therefore, there exists $V = \ds \prod_{\alpha \mathop \in I} V_\alpha \in \BB'$:
:$x \in V \subseteq W$
Let $J = \set{\alpha \in I : V_\alpha \ne S_\alpha}$.
By definition of $\BB'$, $J$ is finite.
Now for all $\alpha \in J$, $x_\alpha \in V_\alpha$ and $V_\alpha \in \tau_\alpha$.
Since $\BB_\alpha$ is a basis for $\tau_\alpha$ then for all $\alpha \in J$ there exists $N_\alpha \in \BB_\alpha$:
:$x_\alpha \in N_\alpha \subseteq V_\alpha$
For all $\alpha \in I$, let:
:$U_\alpha = \begin {cases} N_\alpha & : \alpha \in J \\ S_\alpha & : \alpha \notin J \end {cases}$
Let $U = \ds \prod_{\alpha \mathop \in I} U_\alpha$.
For $\alpha \in J$:
:$U_\alpha = N_\alpha \subseteq V_\alpha$
:$x_\alpha \in N_\alpha = U_\alpha$
:$U_\alpha = N_\alpha \in \BB_\alpha$
For $\alpha \notin J$:
:$U_\alpha = S_\alpha = V_\alpha$
:$x_\alpha \in S_\alpha = U_\alpha$
Thus:
:$x \in U$
:$U \subseteq V \subseteq W$
By the definition of $\BB$ and because $J$ is finite:
:$U \in \BB$.
The result follows.
{{qed}}
Category:Topological Bases
Category:Product Topology
49h99pcsodgtf341jdequgo8c5idfyv
Theorem: Existence and Uniqueness of Domain of Relation

Let $V$ be a basic universe.
Let $\RR \subseteq V \times V$ be a relation.
Then the domain $\Dom \RR$ of $\RR$ exists and is unique.

Proof:
By the Axiom of Specification we can create the subclass of $V$:
:$\Dom \RR = \set {x \in V: \exists y \in V: \tuple {x, y} \in \RR}$
Hence $\Dom \RR$ exists.
Suppose $\QQ \subseteq V$ such that $\QQ$ and $\Dom \RR$ are both the domain of $\RR$.
Then:
:$\QQ = \set {x \in V: \exists y \in V: \tuple {x, y} \in \RR}$
Thus:
:$x \in \QQ \implies x \in \Dom \RR$
and:
:$x \in \Dom \RR \implies x \in \QQ$
Hence by the Axiom of Extension:
:$\QQ = \Dom \RR$
and uniqueness has been demonstrated.
{{qed}}
Theorem: Existence and Uniqueness of Image of Relation

Let $V$ be a basic universe.
Let $\RR \subseteq V \times V$ be a relation.
Then the image $\Img \RR$ of $\RR$ exists and is unique.

Proof:
By the Axiom of Specification we can create the subclass of $V$:
:$\Img \RR = \set {y \in V: \exists x \in V: \tuple {x, y} \in \RR}$
Hence $\Img \RR$ exists.
Suppose $\QQ \subseteq V$ such that $\QQ$ and $\Img \RR$ are both the image of $\RR$.
Then:
:$\QQ = \set {y \in V: \exists x \in V: \tuple {x, y} \in \RR}$
Thus:
:$x \in \QQ \implies x \in \Img \RR$
and:
:$x \in \Img \RR \implies x \in \QQ$
Hence by the Axiom of Extension:
:$\QQ = \Img \RR$
and uniqueness has been demonstrated.
{{qed}}
Theorem: Union of Union of Relation is Union of Domain with Image

Let $V$ be a basic universe.
Let $\RR \subseteq V \times V$ be a relation.
Let $\Dom \RR$ denote the domain of $\RR$.
Then:
:$\map \bigcup {\bigcup \RR} = \Dom \RR \cup \Img \RR$
where:
:$\bigcup \RR$ denotes the union of $\RR$
:$\Dom \RR$ denotes the domain of $\RR$
:$\Img \RR$ denotes the image of $\RR$.

Proof:
{{begin-eqn}}
{{eqn | l = \bigcup \RR
      | r = \set {z: \exists \tuple {x, y} \in \RR: z \in \tuple {x, y} }
      | c = {{Defof|Union of Class}}
}}
{{eqn | r = \set {z: \exists \set {\set x, \set {x, y} } \in \RR: z \in \tuple {x, y} }
      | c = {{Defof|Kuratowski Formalization of Ordered Pair}}
}}
{{eqn | r = \set {\set x, \set {x, y}: x \in \Dom \RR, \tuple {x, y} \in \RR}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \bigcup {\bigcup \RR}
      | r = \set {z: \exists X \in \bigcup \RR: z \in X}
      | c = {{Defof|Union of Class}}
}}
{{eqn | r = \set {x, y: x \in \Dom \RR, \tuple {x, y} \in \RR}
      | c = Definition of $\bigcup \RR$
}}
{{eqn | r = \set {x, y: x \in \Dom \RR, y \in \Img \RR}
      | c = {{Defof|Image of Relation}}
}}
{{eqn | r = \set {x: x \in \Dom \RR} \cup \set {y: y \in \Img \RR}
      | c = {{Defof|Class Union}}
}}
{{eqn | r = \Dom \RR \cup \Img \RR
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Class Union
Category:Relation Theory
ht3wr000kevsfi7987bqphpb37wq05x
Theorem: Domain of Relation is Subclass of Union of Union of Relation

Let $V$ be a basic universe.
Let $\RR \subseteq V \times V$ be a relation.
Let $\Dom \RR$ denote the domain of $\RR$.
Then:
:$\Dom \RR \subseteq \map \bigcup {\bigcup \RR}$
where $\bigcup \RR$ denotes the union of $\RR$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \Dom \RR
      | c = {{Defof|Domain of Relation (Class Theory)}}
}}
{{eqn | ll= \leadsto
      | q = \exists x
      | l = \tuple {x, y}
      | o = \in
      | r = \RR
      | c = {{Defof|Domain of Relation (Class Theory)}}
}}
{{eqn | ll= \leadsto
      | l = \set {\set x, \set {x, y} }
      | o = \in
      | r = \RR
      | c = {{Defof|Ordered Pair}}
}}
{{end-eqn}}
But then:
{{begin-eqn}}
{{eqn | l = \set x
      | o = \in
      | r = \set {\set x, \set {x, y} }
      | c = 
}}
{{eqn | ll= \leadsto
     || l = \set x
      | o = \in
      | r = \bigcup \RR
      | c = {{Defof|Union of Class}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \map \bigcup {\bigcup \RR}
      | c = {{Defof|Union of Class}}
}}
{{eqn | ll= \leadsto
      | l = \Dom \RR
      | o = \subseteq
      | r = \map \bigcup {\bigcup \RR}
      | c = {{Defof|Subclass}}
}}
{{end-eqn}}
{{qed}}
Theorem: Image of Relation is Subclass of Union of Union of Relation

Let $V$ be a basic universe.
Let $\RR \subseteq V \times V$ be a relation.
Let $\Img \RR$ denote the image of $\RR$.
Then:
:$\Img \RR \subseteq \map \bigcup {\bigcup \RR}$
where $\bigcup \RR$ denotes the union of $\RR$.

Proof:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = \Img \RR
      | c = {{Defof|Image of Relation (Class Theory)}}
}}
{{eqn | ll= \leadsto
      | q = \exists x
      | l = \tuple {x, y}
      | o = \in
      | r = \RR
      | c = {{Defof|Image of Relation (Class Theory)}}
}}
{{eqn | ll= \leadsto
      | l = \set {\set x, \set {x, y} }
      | o = \in
      | r = \RR
      | c = {{Defof|Ordered Pair}}
}}
{{end-eqn}}
But then:
{{begin-eqn}}
{{eqn | l = \set {x, y}
      | o = \in
      | r = \set {\set x, \set {x, y} }
      | c = 
}}
{{eqn | ll= \leadsto
     || l = \set {x, y}
      | o = \in
      | r = \bigcup \RR
      | c = {{Defof|Union of Class}}
}}
{{end-eqn}}
Also:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = \set {x, y}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = \map \bigcup {\bigcup \RR}
      | c = {{Defof|Union of Class}}
}}
{{eqn | ll= \leadsto
      | l = \Img \RR
      | o = \subseteq
      | r = \map \bigcup {\bigcup \RR}
      | c = {{Defof|Subclass}}
}}
{{end-eqn}}
{{qed}}
Theorem: Relation is Set implies Domain and Image are Sets

Let $V$ be a basic universe.
Let $\RR \subseteq V \times V$ be a relation.
Let $\RR$ be a set.
Then $\Dom \RR$ and $\Img \RR$ are also sets.

Proof:
From Domain of Relation is Subclass of Union of Union of Relation:
:$\Dom \RR \subseteq \map \bigcup {\bigcup \RR}$
From Image of Relation is Subclass of Union of Union of Relation:
:$\Img \RR \subseteq \map \bigcup {\bigcup \RR}$
We are given that $\RR$ is a set.
From the {{axiom-link|Unions|Class Theory}}:
:$\bigcup \RR$ is a set.
Applying the {{axiom-link|Unions|Class Theory}} a second time:
:$\map \bigcup {\bigcup \RR}$ is a set.
We have that $\RR \subseteq V$, by definition of basic universe
From the {{axiom-link|Swelledness}}, it follows that every subclass of $V$ is a set.
The result follows.
{{qed}}
Theorem: Set is Transitive iff Subset of Power Set

A set $a$ is transitive {{iff}}:
:$a \subseteq \powerset a$
where $\powerset a$ denotes the power set of $a$.

Proof:
=== Necessary Condition ===
Let $a$ be transitive.
Let $x \in a$.
By definition of transitive set:
:$x \subseteq a$
Then by definition of power set:
:$x \in \powerset a$
Hence, by definition of subset:
:$a \subseteq \powerset a$
{{qed|lemma}}
Theorem: Power Set of Transitive Set is Transitive

Let $x$ be a transitive set.
Then its power set $\powerset x$ is also a transitive set.

Proof:
Let $x$ be transitive.
By Set is Transitive iff Subset of Power Set:
:$x \subseteq \powerset x$
Then by Power Set of Subset:
:$\powerset x \subseteq \powerset {\powerset x}$
Thus by Set is Transitive iff Subset of Power Set:
:$\powerset x$ is a transitive set.
{{qed}}
Theorem: Universal Class less Set is not Transitive

Let $V$ be a basic universe.
Let $a \in V$ be a set.
Then:
:$V \setminus \set a$ is not a transitive class
where $\setminus$ denotes class difference.

Proof:
By definition, $V$ is the class of all sets.
As $a \in V$, by definition of $V$ it follows that $a$ is a set.
Consider the power set $\powerset a$ of $a$.
From the axiom of powers:
:$\powerset a$ is also a set
and:
:$\powerset {\powerset a}$ is also a set.
By definition:
:$a \in \powerset a$
and so:
:$\set a \in \powerset {\powerset a}$
as $\powerset {\powerset a}$ is a set, it follows that:
:$\powerset {\powerset a} \in V$
But we have by definition of class difference that $\set a \notin V$.
Hence we have an element of an element of $V$ which is not itself in $V$.
Hence, by definition, $V \setminus \set a$ is not a transitive class.
{{qed}}
Theorem: Basic Universe is Inductive

Let $V$ be a basic universe.
Then $V$ is an inductive class.

Proof:
By definition of basic universe, $V$ is a class containing all sets as elements.
By the {{axiom-link|the Empty Set|Class Theory}}:
:the empty class $\O$ is a set.
Hence $\O$ is an element of $V$.
By the {{axiom-link|Powers|Class Theory}}, if $x$ is a set, then $\powerset x$ is a set.
By definition of power set:
:$\set x \subseteq \powerset x$
By the {{axiom-link|Swelledness}}, $\set x$ is a set.
By the {{axiom-link|Unions|Class Theory}}, if $x$ is a set, then $\bigcup x$ is a set.
Thus $x \cup \set x$ is a set.
The result follows.
{{qed}}
Theorem: Equivalence of Formulations of Axiom of Infinity for Zermelo Universe

The following formulations of the '''{{axiom-link|Infinity|Class Theory}}''' in the context of a '''Zermelo universe''' are equivalent:

Proof:
Let the {{axiom-link|Infinity|Class Theory}}, in each of its formulations, be applied to a basic universe $V$ separately, as follows.
Theorem: Inductive Construction of Natural Numbers fulfils Peano's Axioms

Let $P$ denote the set of natural numbers by definition as an inductive set.
Then $P$ fulfils Peano's axioms.

Proof:
By definition of inductive set:
:$\O \in P$
By definition of the natural numbers, $\O$ is identified with $0$ (zero).
Thus {{PeanoAxiom|1}} holds.
{{qed|lemma}}
Let $x$ be a natural number.
By definition, $x$ is an element of every inductive set.
Thus if $x \in P$ it follows that $x^+ \in P$.
Thus {{PeanoAxiom|2}} holds.
{{qed|lemma}}
By Inductive Construction of Natural Numbers fulfils Peano's Axiom of Injectivity, {{PeanoAxiom|3}} holds.
{{qed|lemma}}
For all $n$, $n$ is an element of $n^+$.
But $0$ is identified with the empty set $\O$.
By definition, $\O$ has no elements.
Therefore it is not possible for $\O$ to equal $n^+$ for any $n$.
Thus {{PeanoAxiom|4}} holds.
{{qed|lemma}}
{{PeanoAxiom|5}} holds immediately by definition of inductive set.
{{qed}}
Theorem: Natural Number is Transitive Set

Let $n$ be a natural number.
Then $n$ is a transitive set.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$n$ is a transitive set.
Theorem: Natural Number is Ordinary Set

Let $n$ be a natural number.
Then $n$ is an ordinary set.
That is:
:$n \notin n$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$n$ is an ordinary set.
Theorem: Product Space Local Basis Induced from Factor Spaces Local Bases

Let $\family {\struct {S_\alpha, \tau_\alpha} }_{\alpha \mathop \in I}$ be an indexed family of topological spaces for $\alpha$ in some indexing set $I$.
Let $\struct {S, \tau} = \ds\prod_{\alpha \mathop \in I} \struct {S_\alpha, \tau_\alpha}$ be the product space of $\family {\struct {S_\alpha, \tau_\alpha} }_{\alpha \mathop \in I}$.
Let $x = \family {x_\alpha} \in S$.
Let $\BB_\alpha$ be a local basis for $x_\alpha$ in the topological space $\struct {S_\alpha, \tau_\alpha}$ for each $\alpha \in I$.
Let $\BB_x$ be the set of all cartesian products of the form $\ds \prod_{\alpha \mathop \in I} U_\alpha$ where:
:for all but finitely many indices $\alpha : U_\alpha = S_\alpha$
:for all $\alpha \in I : U_\alpha \ne S_\alpha \implies U_\alpha \in \BB_\alpha$
Then $\BB_x$ is a local basis for $x$ in the product space $\struct{S, \tau}$.

Proof:
Let $W \in \tau$ such that $x \in W$.
From Natural Basis of Product Topology, the set $\BB$ of cartesian products of the form $\ds \prod_{\alpha \mathop \in I} V_\alpha$ where:
:for all $\alpha \in I : V_\alpha \in \tau_\alpha$
:for all but finitely many indices $\alpha : V_\alpha = X_\alpha$
is a basis for $\tau$.
Therefore, there exists $V = \ds \prod_{\alpha \mathop \in I} V_\alpha \in \BB$:
:$x \in V \subseteq W$
Let $J = \set {\alpha \in I : V_\alpha \ne S_\alpha}$.
By definition of $\BB$, $J$ is finite.
Now for all $\alpha \in J$, $x_\alpha \in V_\alpha$ and $V_\alpha \in \tau_\alpha$.
Since $\BB_\alpha$ is a local basis for $\tau_\alpha$ then for all $\alpha \in J$ there exists $N_\alpha \in \BB_\alpha$:
:$x_\alpha \in N_\alpha \subseteq V_\alpha$
For all $\alpha \in I$, let:
:$U_\alpha = \begin {cases} N_\alpha & : \alpha \in J \\ S_\alpha & : \alpha \notin J \end {cases}$
Let $U = \ds \prod_{\alpha \mathop \in I} U_\alpha$.
For $\alpha \in J$:
:$U_\alpha = N_\alpha \subseteq V_\alpha$
:$x_\alpha \in N_\alpha = U_\alpha$
:$U_\alpha = N_\alpha \in \BB_\alpha$
For $\alpha \notin J$:
:$U_\alpha = S_\alpha = V_\alpha$
:$x_\alpha \in S_\alpha = U_\alpha$
Thus:
:$x \in U$
:$U \subseteq V \subseteq W$
By definition of $\BB_x$ and since $J$ is finite:
:$U \in \BB_x$.
The result follows.
{{qed}}
Category:Topological Bases
Category:Product Spaces
Category:Local Bases
pi9pmkntm088ph2atwp9rjo31k7s8lq
Theorem: Natural Numbers cannot be Elements of Each Other

Let $m$ and $n$ be natural numbers.
Then it cannot be the case that both $m \in n$ and $n \in m$.

Proof:
{{AimForCont}} both $m \in n$ and $n \in m$.
We have $m \in n$
From Natural Number is Transitive Set:
:$m \subseteq n$
by definition of transitive.
Thus:
:$n \in m \subseteq n$
and so:
:$n \in n$
But from Natural Number is Ordinary Set:
:$n \notin n$
The result follows by Proof by Contradiction.
{{qed}}
Theorem: Inductive Construction of Natural Numbers fulfils Peano's Axiom of Injectivity

Let $P$ denote the set of natural numbers by definition as an inductive set.
Then $P$ fulfils:
:{{PeanoAxiom|3}}
where $s$ denotes the successor mapping.

Proof:
Let $m$ and $n$ be natural numbers such that $n^+ = m^+$.
By construction:
:$n \in n^+$
and:
:$m \in m^+$
Thus as $n^+ = m^+$ we have:
:$n \in m^+$
and:
:$m \in n^+$
This gives us:
:$n \in m \lor n = m$
and:
:$m \in n \lor m = n$
{{AimForCont}} that $n \ne m$.
Then from $n \in m \lor n = m$ we have:
:$n \in m$
and from $m \in n \lor m = n$ we have:
:$m \in n$
In summary, if $n \ne m$ we have 
:$n \in m$ and $m \in n$
But from Natural Numbers cannot be Elements of Each Other, this is not possible.
Hence by Proof by Contradiction:
:$n^+ = m^+ \implies n = m$
and the result follows by definition of injection.
{{qed}}
Theorem: Element of Natural Number is Natural Number

Let $n$ be a natural number.
Let $m \in n$.
Then $m$ is also a natural number.

Proof:
The proof proceeds by induction.
For all $n \in \N$, let $\map P n$ be the proposition:
:for all $m \in n$: $m$ is a natural number.