avewright/proofwiki-math huggingface dataset:
Theorem: Order of Real Numbers is Dual of Order of their Negatives

:$\forall x, y \in \R: x > y \iff \paren {-x}< \paren {-y}$

Proof:
Let $x > y$.
{{begin-eqn}}
{{eqn | l = x
      | o = >
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + \paren {-x}
      | o = >
      | r = y + \paren {-x}
      | c = {{Real-number-axiom|O1}}
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = >
      | r = y + \paren {-x}
      | c = {{Real-number-axiom|A4}}
}}
{{eqn | ll= \leadsto
      | l = 0 + \paren {-y}
      | o = >
      | r = y + \paren {-x} + \paren {-y}
      | c = {{Real-number-axiom|O1}}
}}
{{eqn | ll= \leadsto
      | l = 0 + \paren {-y}
      | o = >
      | r = \paren {y + \paren {-y} } + \paren {-x}
      | c = {{Real-number-axiom|A1}} and {{Real-number-axiom|A2}}
}}
{{eqn | ll= \leadsto
      | l = 0 + \paren {-y}
      | o = >
      | r = 0 + \paren {-x}
      | c = {{Real-number-axiom|A4}}
}}
{{eqn | ll= \leadsto
      | l = \paren {-y}
      | o = >
      | r = \paren {-x}
      | c = {{Real-number-axiom|A3}}
}}
{{eqn | ll= \leadsto
      | l = \paren {-x}
      | o = <
      | r = \paren {-y}
      | c = {{Defof|Dual Ordering}}
}}
{{end-eqn}}
{{qed|lemma}}
Let $\paren {-x} < \paren {-y}$.
{{begin-eqn}}
{{eqn | l = \paren {-x}
      | o = <
      | r = \paren {-y}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {-x} + x
      | o = <
      | r = \paren {-y} + x
      | c = {{Real-number-axiom|O1}}
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | r = \paren {-y} + x
      | c = {{Real-number-axiom|A4}}
}}
{{eqn | ll= \leadsto
      | l = 0 + y
      | o = <
      | r = \paren {-y} + x + y
      | c = {{Real-number-axiom|O1}}
}}
{{eqn | ll= \leadsto
      | l = 0 + y
      | o = <
      | r = \paren {\paren {-y} + y} + x
      | c = {{Real-number-axiom|A1}} and {{Real-number-axiom|A2}}
}}
{{eqn | ll= \leadsto
      | l = 0 + y
      | o = <
      | r = 0 + x
      | c = {{Real-number-axiom|A4}}
}}
{{eqn | ll= \leadsto
      | l = y
      | o = <
      | r = x
      | c = {{Real-number-axiom|A3}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = >
      | r = y
      | c = {{Defof|Dual Ordering}}
}}
{{end-eqn}}
{{qed}}
Theorem: Order of Real Numbers is Dual of Order of their Negatives

:$\forall x, y \in \R: x > y \iff \paren {-x}< \paren {-y}$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = >
      | r = y
}}
{{eqn | ll= \leadstoandfrom
      | l = y - x
      | o = <
      | r = 0
      | c = Inequality iff Difference is Positive
}}
{{eqn | ll= \leadstoandfrom
      | lr = -x + y
      | o = <
      | r = 0
      | c = {{Real-number-axiom|A2}}
}}
{{eqn | ll= \leadstoandfrom
      | l = -x + -\paren {-y}
      | o = <
      | r = 0
      | c = Negative of Negative Real Number
}}
{{eqn | ll= \leadstoandfrom
      | l = -x - \paren {-y}
      | o = <
      | r = 0
      | c = {{Defof|Real Subtraction}}
}}
{{eqn | ll= \leadstoandfrom
      | l = -y
      | o = >
      | r = -x
      | c = Inequality iff Difference is Positive
}}
{{end-eqn}}
{{qed}}
Theorem: Square of Non-Zero Real Number is Strictly Positive

:$\forall x \in \R: x \ne 0 \implies x^2 > 0$

Proof:
There are two cases to consider:
:$(1): \quad x > 0$
:$(2): \quad x < 0$
Let $x > 0$.
Then:
{{begin-eqn}}
{{eqn | l = x \times x
      | o = >
      | r = 0
      | c = Strictly Positive Real Numbers are Closed under Multiplication
}}
{{end-eqn}}
Let $x < 0$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = <
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \times x
      | o = >
      | r = x \times 0
      | c = Real Number Ordering is Compatible with Multiplication: Negative Factor
}}
{{eqn | r = 0
      | c = Real Zero is Zero Element
}}
{{end-eqn}}
{{qed}}
Theorem: Minus One is Less than Zero

:$-1 < 0$

Proof:
{{begin-eqn}}
{{eqn | l = 0
      | o = <
      | r = 1
      | c = Real Zero is Less than Real One
}}
{{eqn | ll= \leadsto
      | l = -0
      | o = >
      | r = -1
      | c = Order of Real Numbers is Dual of Order of their Negatives
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = >
      | r = -1
      | c = Negative of Real Zero equals Zero
}}
{{eqn | ll= \leadsto
      | l = -1
      | o = <
      | r = 0
      | c = {{Defof|Dual Ordering}}
}}
{{end-eqn}}
{{qed}}
Theorem: Real Zero is Less than Real One

The real number $0$ is less than the real number $1$:
:$0 < 1$

Proof:
{{begin-eqn}}
{{eqn | l = 1 \times 1
      | o = >
      | r = 0
      | c = Square of Non-Zero Real Number is Strictly Positive
}}
{{eqn | ll= \leadsto
      | l = 1
      | o = >
      | r = 0
      | c = {{Real-number-axiom|M3}}
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | r = 1
      | c = {{Defof|Dual Ordering}}
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Real Numbers is Positive iff Numbers have Same Sign

The product of two real numbers is greater than $0$ {{iff}} either both are greater than $0$ or both are less than $0$.
:$\forall x, y \in \R: x \times y > 0 \iff \paren {x, y \in \R_{>0} } \lor \paren {x, y \in \R_{<0} }$

Proof:
=== Sufficient Condition ===
Let $x \times y > 0$.
{{AimForCont}} either $x = 0$ or $y = 0$.
Then from Real Zero is Zero Element:
:$x \times y = 0$
Therefore by Proof by Contradiction:
:$y \ne 0$ and $x \ne 0$
{{qed|lemma}}
Let $x > 0$.
{{AimForCont}} $y < 0$.
{{begin-eqn}}
{{eqn | l = x
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \times y
      | o = <
      | r = 0 \times 0
      | c = Real Number Ordering is Compatible with Multiplication: Negative Factor
}}
{{eqn | ll= \leadsto
      | l = x \times y
      | o = <
      | r = 0
      | c = {{Defof|Dual Ordering}}
}}
{{end-eqn}}
But {{hypothesis}}, $x \times y > 0$.
Therefore by Proof by Contradiction:
:$y > 0$
{{qed|lemma}}
Let $x < 0$.
{{AimForCont}} $y > 0$.
{{begin-eqn}}
{{eqn | l = x
      | o = <
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \times y
      | o = <
      | r = 0 \times 0
      | c = {{Real-number-axiom|O2}}
}}
{{eqn | ll= \leadsto
      | l = x \times y
      | o = <
      | r = 0
      | c = {{Defof|Dual Ordering}}
}}
{{end-eqn}}
But {{hypothesis}}, $x \times y > 0$.
Therefore by Proof by Contradiction:
:$y > 0$
{{qed|lemma}}
Thus:
:$x \times y > 0 \implies \paren {x > 0 \land y > 0} \lor \paren {x < 0 \land y < 0}$
{{qed|lemma}}
Theorem: Reciprocal of Strictly Positive Real Number is Strictly Positive

:$\forall x \in \R: x > 0 \implies \dfrac 1 x > 0$

Proof:
Let $x > 0$.
{{AimForCont}} $\dfrac 1 x < 0$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \times \dfrac 1 x
      | o = <
      | r = 0 \times 0
      | c = Real Number Ordering is Compatible with Multiplication: Negative Factor
}}
{{eqn | ll= \leadsto
      | l = 1
      | o = <
      | r = 0
      | c = {{Real-number-axiom|A4}}
}}
{{end-eqn}}
But from Real Zero is Less than Real One:
:$1 > 0$
Therefore by Proof by Contradiction:
:$\dfrac 1 x > 0$
{{qed}}
Theorem: Order of Strictly Positive Real Numbers is Dual of Order of their Reciprocals

:$\forall x, y \in \R: x > y > 0 \implies \dfrac 1 x < \dfrac 1 y$

Proof:
From Reciprocal of Strictly Positive Real Number is Strictly Positive:
:$(1): \quad x > 0 \implies \dfrac 1 x > 0$
:$(2): \quad y > 0 \implies \dfrac 1 y > 0$
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = >
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \times \frac 1 x
      | o = >
      | r = y \times \frac 1 x
      | c = {{Real-number-axiom|O2}} and from $(1)$
}}
{{eqn | ll= \leadsto
      | l = x \times \frac 1 x \times \frac 1 y
      | o = >
      | r = y \times \frac 1 x \times \frac 1 y
      | c = {{Real-number-axiom|O2}} and from $(2)$
}}
{{eqn | ll= \leadsto
      | l = \paren {x \times \frac 1 x} \times \frac 1 y
      | o = >
      | r = \paren {y \times \frac 1 y} \times \frac 1 x
      | c = {{Real-number-axiom|M1}} and {{Real-number-axiom|M2}}
}}
{{eqn | ll= \leadsto
      | l = 1 \times \frac 1 y
      | o = >
      | r = 1 \times \frac 1 x
      | c = {{Real-number-axiom|A4}}
}}
{{eqn | ll= \leadsto
      | l = \frac 1 y
      | o = >
      | r = \frac 1 x
      | c = {{Real-number-axiom|M3}}
}}
{{eqn | ll= \leadsto
      | l = \frac 1 x
      | o = <
      | r = \frac 1 y
      | c = {{Defof|Dual Ordering}}
}}
{{end-eqn}}
{{qed}}
Theorem: Mean of Unequal Real Numbers is Between them

:$\forall x, y \in \R: x < y \implies x < \dfrac {x + y} 2 < y$

Proof:
First note that:
{{begin-eqn}}
{{eqn | l = 0
      | o = <
      | r = 1
      | c = Real Zero is Less than Real One
}}
{{eqn | ll= \leadsto
      | l = 0 + 0
      | o = <
      | r = 1 + 1
      | c = Real Number Inequalities can be Added
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | r = \frac 1 {1 + 1}
      | c = Reciprocal of Strictly Positive Real Number is Strictly Positive
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = 0
      | o = <
      | r = \frac 1 2
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = <
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + x
      | o = <
      | r = x + y
      | c = {{Real-number-axiom|O1}}
}}
{{eqn | ll= \leadsto
      | l = \paren {x + x} \times \frac 1 2
      | o = <
      | r = \paren {x + y} \times \frac 1 2
      | c = {{Real-number-axiom|O2}} and from $(1)$
}}
{{eqn | ll= \leadsto
      | l = x
      | o = <
      | r = \frac {x + y} 2
      | c = {{Defof|Real Division}}
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn | l = x
      | o = <
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + y
      | o = <
      | r = y + y
      | c = {{Real-number-axiom|O1}}
}}
{{eqn | ll= \leadsto
      | l = \paren {x + y} \times \frac 1 2
      | o = <
      | r = \paren {y + y} \times \frac 1 2
      | c = {{Real-number-axiom|O2}} and from $(1)$
}}
{{eqn | ll= \leadsto
      | l = \frac {x + y} 2
      | o = <
      | r = y
      | c = {{Defof|Real Division}}
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection of Inductive Set as Subset of Real Numbers is Inductive Set

Let $\AA$ be a set of inductive sets defined as subsets of real numbers.
Then their intersection is an inductive set.

Proof:
By definition of inductive set:
:$\forall S \in \AA: 1 \in S$
Thus by definition of set intersection:
:$\ds 1 \in \bigcap_{S \mathop \in \AA} S$
Also by definition of inductive set:
:$\forall S \in \AA: x \in S \implies x + 1 \in S$
So:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \bigcap_{S \mathop \in \AA} S
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall S \in \AA
      | l = x
      | o = \in
      | r = S
      | c = {{Defof|Intersection of Set of Sets}}
}}
{{eqn | ll= \leadsto
      | q = \forall S \in \AA
      | l = x + 1
      | o = \in
      | r = S
      | c = {{Defof|Inductive Set as Subset of Real Numbers}}
}}
{{eqn | ll= \leadsto
      | l = x + 1
      | o = \in
      | r = \bigcap_{S \mathop \in \AA} S
      | c = {{Defof|Intersection of Set of Sets}}
}}
{{end-eqn}}
Hence the result, by definition of inductive set.
{{qed}}
Theorem: Non-Empty Subset of Initial Segment of Natural Numbers has Greatest Element

Let $n \in \N_{>0}$ be a non-zero natural number.
Let $\N^*_n$ denote the Initial segment $\set {1, 2, \ldots, n}$ of the non-zero natural numbers.
Then every non-empty subset of $\N^*_n$ has a greatest element.

Proof:
The proof will proceed by the Principle of Mathematical Induction on $\N_{>0}$.
Let $S$ be the set defined as:
:$S := \leftset {n \in \N:}$ Every non-empty subset of $\N^*_n$ has a greatest element$\rightset{}$
Theorem: Not every Non-Empty Subset of Natural Numbers has Greatest Element

Let $S \subseteq \N_{>0}$.
Then, despite Non-Empty Subset of Initial Segment of Natural Numbers has Greatest Element, it is not necessarily the case that $S$ has a greatest element.

Proof:
Let:
:$S = \set {x \in \N_{>0}: x > 1}$
Then $S \subseteq \N_{>0}$.
{{AimForCont}} $S$ has a greatest element.
Let the greatest element of $S$ be $k$.
But $\N_{>0}$ is an inductive set.
Therefore $k + 1 \in \N_{>0}$.
By definition of $S$:
:$k + 1 \in S$
Therefore $k$ cannot be the greatest element of $S$.
By Proof by Contradiction it follows that $S$ has no greatest element.
It is not possible to apply Non-Empty Subset of Initial Segment of Natural Numbers has Greatest Element, because $S$ is not a subset of an initial segment of $\N_{>0}$.
{{qed}}
Theorem: Existence of Integral on Union of Adjacent Intervals

Let $f$ be a real function defined on a closed interval $\closedint a b$ where $a < b$.
Let $c$ be a point in $\openint a b$.
Then:
:$f$ is Darboux integrable on $\closedint a c$ and $\closedint c b$
{{iff}}:
:$f$ is Darboux integrable on $\closedint a b$.

Proof:
=== Necessary Condition ===
We need to prove that $f$ is Darboux integrable on $\closedint a b$.
To do this it suffices to show that for all $\epsilon > 0$, there exists a subdivision $S$ of $\closedint a b$ such that $\map U S – \map L S < \epsilon$.
Here, $\map U S$ and $\map L S$ are, respectively, the upper Darboux sum and lower Darboux sum of $f$ on $\closedint a b$ with respect to the subdivision $S$.
Let a strictly positive $\epsilon$ be given.
Since $f$ is Darboux integrable on $\closedint a c$, we know that a subdivision $S_1$ of $\closedint a c$ exists such that $\map U {S_1} – \map L {S_1} < \dfrac \epsilon 2$.
Since $f$ is Darboux integrable on $\closedint c b$, we know that a subdivision $S_2$ of $\closedint c b$ exists such that $\map U {S_2} – \map L {S_2} < \dfrac \epsilon 2$.
Define the subdivision $S = S_1 \cup S_2$.
We observe that $S$ is a subdivision of $\closedint a b$.
By the definition of upper Darboux sum:
{{begin-eqn}}
{{eqn | l = \map U S
      | r = \map U {S_1} + \map U {S_2}
      | c = since $S = S_1 \cup S_2$ and $S_1$ and $S_2$ are adjacent
}}
{{end-eqn}}
Also, by the definition of lower Darboux sum:
{{begin-eqn}}
{{eqn | l = \map L S
      | r = \map L {S_1} + \map L {S_2}
      | c = since $S = S_1 \cup S_2$ and $S_1$ and $S_2$ are adjacent
}}
{{end-eqn}}
These two equations give:
{{begin-eqn}}
{{eqn | l = \map U S – \map L S
      | r = \map U {S_1} + \map U {S_2} – \paren {\map L {S_1} + \map L {S_2} }
}}
{{eqn | r = \map U {S_1} – \map L {S_1} + \map U {S_2} – \map L {S_2}
}}
{{eqn | o = <
      | r = \dfrac \epsilon 2 + \dfrac \epsilon 2
      | c = since $\map U {S_1} – \map L {S_1} < \dfrac \epsilon 2$ and $\map U {S_2} – \map L {S_2} < \dfrac \epsilon 2$
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}
This shows that $S$ satisfies $\map U S – \map L S < \epsilon$.
We conclude from this that $f$ is Darboux integrable on $\closedint a b$ since $S$ is a subdivision of $\closedint a b$.
{{qed|lemma}}
Theorem: Cartesian Product of Bijections is Bijection

Let $S_1 \times S_2$ be the Cartesian product of two sets $S_1$ and $S_2$.
Let $T_1 \times T_2$ be the Cartesian product of two sets $T_1$ and $T_2$.
Let $f_1: S_1 \to T_1$ and $f_2: S_2 \to T_2$ be bijections.
Let $f_1 \times f_2: S_1 \times S_2 \to T_1 \times T_2$ be the Cartesian product of $f_1$ and $f_2$ defined as:
:$\forall \left({s_1, s_2}\right) \in S_1 \times S_2: f_1 \times f_2 \left({s_1, s_2}\right) := \left({f_1 \left({s_1}\right), f_2 \left({s_2}\right)}\right)$
Then $f_1 \times f_2$ is a bijection.

Proof:
Because $f_1$ and $f_2$ are both bijections, it follows by definition that they are both surjections.
Let $\left({t_1, t_2}\right) \in T_1 \times T_2$.
Then:
:as $f_1$ is a surjection, $\exists s_1 \in S_1: f_1 \left({s_1}\right) = t_1$
:as $f_2$ is a surjection, $\exists s_2 \in S_2: f_2 \left({s_2}\right) = t_2$
Thus:
:$\exists \left({s_1, s_2}\right) \in S_1 \times S_2: f_1 \times f_2 \left({s_1, s_2}\right) = \left({t_1, t_2}\right)$
So $f_1 \times f_2$ is a surjection.
Because $f_1$ and $f_2$ are both bijections, it follows by definition that they are both injections.
Let:
: $f_1 \times f_2 \left({a_1, a_2}\right) = \left({c_1, c_2}\right), f_1 \times f_2 \left({b_1, b_2}\right) = \left({d_1, d_2}\right)$
for some $\left({a_1, a_2}\right), \left({b_1, b_2}\right) \in S_1 \times S_2$.
Suppose $\left({c_1, c_2}\right) = \left({d_1, d_2}\right)$.
Then by Equality of Ordered Pairs:
:$c_1 = d_1$
:$c_2 = d_2$
By definition of $f_1 \times f_2$:
:$f_1 \left({a_1}\right) = c_1$
:$f_1 \left({b_1}\right) = d_1$
and:
:$f_2 \left({a_2}\right) = c_2$
:$f_2 \left({b_2}\right) = d_2$
As $f_1$ is an injection:
:$c_1 = d_1 \implies a_1 = b_1$
and as $f_2$ is an injection:
:$c_2 = d_2 \implies a_2 = b_2$
Thus it follows that:
:$\left({c_1, c_2}\right) = \left({d_1, d_2}\right) \implies \left({a_1, a_2}\right) = \left({b_1, b_2}\right)$
and so $f_1 \times f_2$ is an injection.
So $f_1 \times f_2$ is a surjection and also an injection.
Hence by definition, $f_1 \times f_2$ is a bijection.
{{qed}}
Category:Bijections
Category:Cartesian Product
a5gd6052hnmbkcqn4kezns4qy9nt7ci
Theorem: Cartesian Product of Bijections is Bijection/General Result

Let $I$ be an indexing set.
Let $\family {S_i}_{i \mathop \in I}$ and $\family {T_i}_{i \mathop \in I}$ be families of sets indexed by $I$.
Let $\ds \SS := \prod_{i \mathop \in I} S_i$ and $\ds \TT := \prod_{i \mathop \in I} T_i$ be the Cartesian products of $\family {S_i}_{i \mathop \in I}$ and $\family {T_i}_{i \mathop \in I}$ respectively.
For all $i \in I$, let $f_i: S_i \to T_i$ be a bijection.
Let $\ds \FF: \SS \to \TT := \prod_{i \mathop \in I} \paren {f_i: S_i \to T_i}$ be the Cartesian product of $\family {f_i}_{i \mathop \in I}$ defined as:
:$\ds \forall \mathbf s \in \SS: \map \FF {\mathbf s} := \prod_{i \mathop \in I} \paren {\map {f_i} {s_i} }$
where $\mathbf s := \family {S_i}_{i \mathop \in I}$ is an arbitrary element of $\family {S_i}_{i \mathop \in I}$.
Then $\FF$ is a bijection.

Proof:
Because $f_i$ are bijections, it follows by definition that they are surjections.
Let $\mathbf t := \family {t_i}_{i \mathop \in I} \in \TT$.
Then as $f_i$ is a surjection:
:$\forall i \in I: \exists s_i \in S_i: \map {f_i} {s_i} = t_i$
Thus:
:$\exists \mathbf s \in \SS: \map \FF {\mathbf s} = \mathbf t$
So $\FF$ is a surjection.
Because $f_i$ are bijections, it follows by definition that they are injections.
Let:
:$\mathbf t_1 := \family {t_{i 1} }_{i \mathop \in I} \in \TT$
:$\mathbf t_2 := \family {t_{i 2} }_{i \mathop \in I} \in \TT$
Let:
:$\map \FF {\mathbf s_1} = \paren {\mathbf t_1}, \map \FF {\mathbf s_2} = \mathbf t_2$
for some $\mathbf s_1, \mathbf s_2 \in \SS$ where:
:$\mathbf s_1 := \family {s_{i 1} }_{i \mathop \in I}$
:$\mathbf s_2 := \family {s_{i 2} }_{i \mathop \in I}$
Suppose $\mathbf t_1 = \mathbf t_2$.
Then:
:$\forall i \in I: t_{i 1} = t_{i 2}$
By definition of $\FF$:
:$\forall i \in I: \map {f_i} {s_{i 1} } = t_{i 1}$
:$\forall i \in I: \map {f_i} {s_{i 2} } = t_{i 2}$
As $f_i$ is an injection for all $i \in I$:
:$\forall i \in I: t_{i 1} = t_{i 2} \implies s_{i 1} = s_{i 2}$
Thus it follows that:
:$\mathbf t_1 = \mathbf t_2 \implies \mathbf s_1 = \mathbf s_2$
and so $\FF$ is an injection.
So $\FF$ is a surjection and also an injection.
Hence by definition, $\FF$ is a bijection.
{{qed}}
Theorem: First Order ODE/y' - f (y) phi' (x) over f' (y) = phi (x) phi' (x) over f' (y)

Let $\map f y$ and $\map \phi x$ be known real functions of $y$ and $x$ respectively.
The general solution of:
:$(1): \quad \dfrac {\d y} {\d x} - \dfrac {\map f y} {\map {f'} y} \map {\phi'} x = \dfrac {\map \phi x \map {\phi'} x} {\map {f'} y}$
is:
:$\map f y = C e^{\map \phi x} - \map \phi x - 1$

Proof:
Let $u = \map f y$
Then by the Chain Rule for Derivatives:
:$\dfrac {\d u} {\d x} = \map {f'} y \dfrac {\d y} {\d x}$
Then:
{{begin-eqn}}
{{eqn | l = \dfrac {\d y} {\d x} - \dfrac {\map f y} {\map {f'} y} \map {\phi'} x
      | r = \dfrac {\map \phi x \map {\phi'} x} {\map {f'} y}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {f'} y \dfrac {\d y} {\d x} - \map f y \map {\phi'} x
      | r = \map \phi x \map {\phi'} x
      | c = multiplying $(1)$ by $\map {f'} y$
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d u} {\d x} - u \map {\phi'} x
      | r = \map \phi x \map {\phi'} x
      | c = substituting $u$ for $\map f y$
}}
{{end-eqn}}
This is a linear first order ordinary differential equation in the form:
:$\dfrac {\d u} {\d x} + \map P x u = \map Q x$
whose general solution from Solution to Linear First Order Ordinary Differential Equation is:
:$\ds u e^{\int P \rd x} = \int Q e^{\int P \rd x} \rd x + C$
In this instance:
:$\map P x = -\map {\phi'} x$
and:
:$\map Q x = \map \phi x \map {\phi'} x$
Thus:
{{begin-eqn}}
{{eqn | l = \int P \rd x
      | r = -\int \map {\phi'} x \rd x
      | c = 
}}
{{eqn | r = -\map \phi x + A
      | c = 
}}
{{end-eqn}}
Hence:
:$\ds u e^{-\map \phi x + A} = \int \map \phi x \map {\phi'} x e^{-\map \phi x + A} \rd x + C$
Let $v = \map \phi x$.
Then by Integration by Substitution:
{{begin-eqn}}
{{eqn | l = \int \map \phi x \map {\phi'} x e^{-\map \phi x + A} \rd x
      | r = \int v e^{-v + A} \rd v
      | c = Integration by Substitution
}}
{{eqn | r = \int v e^{-v} e^A \rd v
      | c = 
}}
{{eqn | r = e^A \int v e^{-v} \rd v
      | c = 
}}
{{eqn | r = - e^A e^{-v} \paren {v + 1} + C'
      | c = Primitive of $x e^{a x}$
}}
{{end-eqn}}
This leaves us with:
:$u e^{-\map \phi x + A} = - e^A e^{-v} \paren {v + 1} + C$
subsuming $C'$ into $C$.
Substituting back in, the general solution is seen to be:
:$\map f y e^{-\map \phi x + A} = - e^{-\map \phi x + A} \paren {\map \phi x + 1} + C$
and so multiplying both sides by $e^{\map \phi x - A}$:
{{begin-eqn}}
{{eqn | l = \map f y 
      | r = \paren {-\map \phi x - 1} + C e^{\map \phi x - A}
}}
{{eqn | r = C e^{-A} e^{\map \phi x} - \map \phi x - 1 
}}
{{eqn | r = C e^{\map \phi x} - \map \phi x - 1 
      | c = by absorbing the constant factor $e^{-A}$ into $C$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Cardinality of Set of All Mappings/Finite Sets

Let $S$ and $T$ be finite sets.
The cardinality of the set of all mappings from $S$ to $T$ (that is, the total number of mappings from $S$ to $T$) is:
:$\card {T^S} = \card T^{\card S}$

Proof:
Let $\card S = n$ and $\card T = m$.
First suppose that $n = 0$, that is, that $S = \O$.
From Cardinality of Set of All Mappings from Empty Set:
:$\card {T^\O} = 1 = m^0$
and the result is seen to hold for $n = 0$.
Next, suppose that $m = 0$, that is, that $T = \O$.
From Cardinality of Set of All Mappings to Empty Set:
:$\card {\O^S} = \begin {cases}
1 & : S = \O \\ 
0 & : S \ne \O
\end {cases}$
So if $n > 0$:
:$\card {\O^S} = 0 = 0^n$
and if $n = 0$:
:$\card {T^S} = 1 = 0^0 = m^n$
and the result holds.
This fits in with the preferred definition of the value of $0^0$.
Finally, suppose $m > 0$ and $n > 0$.
Let $\sigma: \N_n \to S$ and $\tau: T \to \N_n$ be bijections.
Then the mapping $\Phi: T^S \to \paren {\N_m}^{\paren {\N_n} }$ defined as:
:$\forall f \in T^S: \map \Phi f = \tau \circ f \circ \sigma$
(where $\paren {\N_m}^{\paren {\N_n} }$ is the set of all mappings from $\N_n$ to $\N_m$) is also a bijection.
So we need only consider the case where $S = \N_n$ and $T = \N_m$.
Let $m \in \N_{>0}$.
For each $n \in \N$, let $\Bbb T \paren {n, m}$ be the set of all mappings from $\N_n$ to $\N_m$.
Let:
:$\Bbb S = \set {n \in \N: \card {\Bbb T \tuple {n, m} } = m^n}$
We have seen that $0 \in \Bbb S$.
Let $n \in \Bbb S$.
Let $\rho: \Bbb T \tuple {n + 1, m} \to \Bbb T \paren {n, m}$ defined by:
:$\forall f \in \Bbb T \tuple {n + 1, m}: \rho \paren f =$ the restriction of $f$ to $\N_n$
Given that $g \in \Bbb T \tuple {n, m}$, and $k \in \N_m$, let $g_k: \N_{n + 1} \to \N_m$ be defined by:
:$\forall x \in \N_{n + 1}: \map {g_k} x = \begin {cases}
\map g x & : x \in \N_n \\
k & : x = n
\end {cases}$
Then:
:$\rho^{-1} \sqbrk {\set g} = \set {g_0, \ldots, g_{m - 1} }$
Thus $\rho^{-1} \sqbrk {\set g}$ has $m$ elements.
So clearly:
:$\set {\rho^{-1} \sqbrk {\set g}: g \in \Bbb T \tuple {n, m} }$
is a partition of $\Bbb T \tuple {n + 1, m}$.
Hence, as $n \in \Bbb S$, the set $\Bbb T \tuple {n + 1, m}$ has $m \cdot m^n = m^{n + 1}$ elements by Number of Elements in Partition.
Thus $n + 1 \in \Bbb S$.
By the Principle of Mathematical Induction:
:$\Bbb S = \N$
and the proof is complete.
{{qed}}