avewright/proofwiki-math huggingface dataset:
Theorem: Closed Interval of Naturally Ordered Semigroup with Successor equals Union with Successor

Let $\struct {S, \circ, \preceq}$ be a naturally ordered semigroup.
Then:
:$\forall m, n \in \struct {S, \circ, \preceq}: m \preceq n \implies \closedint m {n \circ 1} = \closedint m n \cup \set {n \circ 1}$
where $\closedint m n$ is the closed interval between $m$ and $n$.

Proof:
Let $m \preceq n$. Then:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \closedint m {n \circ 1}
      | c = 
}}
{{eqn | o = \leadstoandfrom
      | r = m \preceq x \land x \preceq \paren {n \circ 1}
      | c = {{Defof|Closed Interval}}
}}
{{eqn | o = \leadstoandfrom
      | r = m \preceq x \land \paren {x \prec n \circ 1 \lor x = n \circ 1}
      | c = {{Defof|Strictly Precede}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \closedint m n \cup \set {n \circ 1}
      | c = 
}}
{{eqn | o = \leadstoandfrom
      | r = m \preceq x \land \paren {x \preceq n \lor x = n \circ 1}
      | c = {{Defof|Closed Interval}} and {{Defof|Set Union}}
}}
{{eqn | o = \leadstoandfrom
      | r = m \preceq x \land \paren {x \prec n \lor x = n \lor x = n \circ 1}
      | c = {{Defof|Strictly Precede}}
}}
{{eqn | o = \leadstoandfrom
      | r = m \preceq x \land \paren {x \prec n \circ 1 \lor x = n \circ 1}
      | c = {{Defof|Strictly Precede}}
}}
{{end-eqn}}
Thus:
:$\closedint m {n \circ 1} = \closedint m n \cup \set {n \circ 1}$
{{qed}}
Theorem: Principle of Induction applied to Interval of Naturally Ordered Semigroup

Let $\struct {S, \circ, \preceq}$ be a naturally ordered semigroup.
Let $\closedint p q$ be a closed interval of $\struct {S, \circ, \preceq}$.
Let $T \subseteq \closedint p q$ such that the minimal element of $\closedint p q$ is in $T$.
Let:
:$x \in T: x \prec q \implies x \circ 1 \in T$
Then:
:$T = \closedint p q$

Proof:
Let $T' = T \cup \set {x \in S: q \prec x}$.
Then $T'$ satisfies the conditions of the Principle of Mathematical Induction.
Therefore:
:$T' = \set {x \in S: p \preceq x}$
Therefore:
:$T = \closedint p q$
{{Qed}}
Theorem: Naturally Ordered Semigroup is Unique

Let $\struct {S, \circ, \preceq}$ and $\struct {S', \circ', \preceq'}$ be naturally ordered semigroups.
Let:
:$0'$ be the smallest element of $S'$
:$1'$ be the smallest element of $S' \setminus \set {0'} = S'^*$.
Then the mapping $g: S \to S'$ defined as:
:$\forall a \in S: \map g a = \circ'^a 1'$
is an isomorphism from $\struct {S, \circ, \preceq}$ to $\struct {S', \circ', \preceq'}$.
This isomorphism is unique.
Thus, up to isomorphism, there is only one naturally ordered semigroup.

Proof:
=== Proof that Mapping is Isomorphism ===
{{:Naturally Ordered Semigroup is Unique/Existence of Isomorphism}}{{Qed|lemma}}
Theorem: Consecutive Subsets of N

Let $\N_k$ denote the initial segment of the natural numbers determined by $k$:
:$\N_k = \left\{{0, 1, 2, 3, \ldots, k - 1}\right\}$
Then:
:$\N_k = \N_{k + 1} \setminus \left\{{k}\right\}$
In particular:
:$\N_{k - 1} = \N_k \setminus \left\{{k - 1}\right\}$

Proof:
The result follows as a direct application of Strict Lower Closure of Sum with One.
{{qed}}
Category:Natural Numbers
ebnlj9h3zjmkiqhic6nj6grj7lm6oxj
Theorem: Well-Ordering Principle

Every non-empty subset of $\N$ has a smallest (or '''first''') element.
That is, the relational structure $\struct {\N, \le}$ on the set of natural numbers $\N$ under the usual ordering $\le$ forms a well-ordered set.
This is called the '''well-ordering principle'''.

Proof:
Let $S$ be a non-empty subset of the set of natural numbers $\N$.
We take as axiomatic that $\N$ is itself a subset of the set of real numbers $\R$.
Thus $S \subseteq \R$.
By definition:
:$\forall n \in \N: n \ge 0$
and so:
:$\forall n \in S: n \ge 0$
Hence $0$ is a lower bound of $S$.
This establishes the fact that $S$ is bounded below.
By the Continuum Property, we have that $S$ admits an infimum.
Hence let $b = \inf S$.
Because $b$ is the infimum of $S$, it follows that $b + 1$ is not a lower bound of $S$.
So, for some $n \in S$:
:$n < b + 1$
{{AimForCont}} $n$ is not the smallest element of $S$.
Then there exists $m \in S$ such that:
:$b \le m < n < b + 1$
from which it follows that:
:$0 < n - m < 1$
But there exist no natural numbers $k$ such that $0 < k < 1$.
Hence $n = b$ is the smallest element of $S$.
{{qed}}
Theorem: Well-Ordering Principle

Every non-empty subset of $\N$ has a smallest (or '''first''') element.
That is, the relational structure $\struct {\N, \le}$ on the set of natural numbers $\N$ under the usual ordering $\le$ forms a well-ordered set.
This is called the '''well-ordering principle'''.

Proof:
Consider the natural numbers $\N$ defined as the naturally ordered semigroup $\struct {S, \circ, \preceq}$.
From its definition, $\struct {S, \circ, \preceq}$ is well-ordered by $\preceq$.
The result follows.
As $\N_{\ne 0} = \N \setminus \set 0$, by Set Difference is Subset $\N_{\ne 0} \subseteq \N$.
As $\N$ is well-ordered, by definition, every subset of $\N$ has a smallest element.
{{qed}}
Theorem: Well-Ordering Principle

Every non-empty subset of $\N$ has a smallest (or '''first''') element.
That is, the relational structure $\struct {\N, \le}$ on the set of natural numbers $\N$ under the usual ordering $\le$ forms a well-ordered set.
This is called the '''well-ordering principle'''.

Proof:
From Von Neumann Construction of Natural Numbers is Minimally Inductive, $\omega$ is a minimally inductive class under the successor mapping.
From Successor Mapping on Natural Numbers is Progressing, this successor mapping is a progressing mapping.
The result is a direct application of Minimally Inductive Class under Progressing Mapping is Well-Ordered under Subset Relation.
{{qed}}
Theorem: Equality of Natural Numbers

Let $m, n \in \N$.
Then:
:$\N_m \sim \N_n \iff m = n$
where $\sim$ denotes set equivalence and $\N_n$ denotes the set of all natural numbers less than $n$.

Proof:
By Set Equivalence behaves like Equivalence Relation, we have that:
:$m = n \implies \N_m \sim \N_n$
It remains to show that:
:$m \ne n \implies \N_m \nsim \N_n$.
Since the naturals are totally ordered, it will be sufficient to show that:
:$m \in \N_n \implies \N_m \nsim \N_n$
Let $S = \set {n \in \N: \forall m \in \N_n: \N_m \nsim \N_n}$.
That is, $S$ is the set of all the natural numbers $n$ such that $\N_m \nsim \N_n$ for all $m \in \N_n$.
We use mathematical induction to prove that $S = \N$.
From Initial Segment of Natural Numbers determined by Zero is Empty:
:$\N_0 = \O$
Thus $0 \in S$.
This is the basis for the induction.
Now, assume the induction hypothesis that $n \in S$.
We now complete the induction step, that is, to show that $n + 1 \in S$.
Let $m \in \N_{n + 1}$.
If $m = 0$, then $\N_m \nsim \N_{n + 1}$ because $\N_0 = \O$ and $\N_{n + 1} \ne \O$.
{{AimForCont}} that $m \ge 1$ and $\N_m \sim \N_{n + 1}$.
Then, by Set Equivalence Less One Element, that means $\N_{m - 1} \sim \N_n$.
But then $m - 1 \in \N_n$ which contradicts the induction hypothesis that $n \in S$.
Thus $n + 1 \in S$.
The result follows from the fact that Set Equivalence behaves like Equivalence Relation, in particular the symmetry clause.
{{qed}}
Theorem: Principle of Counting

Let $T$ be a set such that $T \sim \N_n$.
Then:
:$\forall m \in \N: n \ne m \implies T \nsim \N_m$

Proof:
The result follows directly from Equality of Natural Numbers and the fact that set equivalence is transitive.
{{qed}}
Theorem: Cardinality Less One

Let $S$ be a finite set.
Let:
:$\card S = n + 1$
where $\card S$ is the cardinality of $S$.
Let $a \in S$.
Then:
:$\card {S \setminus \set a} = n$
where $\setminus$ denotes set difference.

Proof:
This follows as an immediate consequence of Set Equivalence Less One Element.
{{qed}}
Theorem: Cardinality of Empty Set

:$\card S = 0 \iff S = \O$
That is, the empty set is finite, and has a cardinality of zero.

Proof:
Zero is defined as the cardinal of the empty set.
The result follows from Finite Cardinals and Ordinals are Equivalent.
Theorem: Cardinality of Subset of Finite Set

Let $A$ and $B$ be finite sets such that $A \subseteq B$.
Let
:$\card B = n$
where $\card {\, \cdot \,}$ denotes cardinality.
Then $\card A \le n$.

Proof:
Let $A \subseteq B$.
There are two cases:
$(1): \quad A \ne B$
In this case:
:$A \subsetneqq B$
and from Cardinality of Proper Subset of Finite Set:
:$\card A < n$
$(2): \quad A = B$
In this case:
:$\card A = \card B$
and so:
:$\card A = n$
In both cases:
:$\card A \le n$
Hence the result.
{{qed}}
Theorem: Cardinality of Codomain of Surjection

Let $S$ be a set.
Let:
:$\card S = n$
where $\card S$ denotes the cardinality of $S$.
Let $f: S \to T$ be a surjection.
Then $\card T \le n$.
The equality:
:$\card T = n$
occurs {{iff}} $f$ is a bijection.

Proof:
We have that $\card S = n$.
Then by definition of cardinality:
:there is a surjection from $S$ to $T$
{{iff}}:
:there is a surjection from $\N_n$ to $T$.
So we need consider the case only when $S = \N_n$.
By definition of surjection:
:$\forall x \in T: f^{-1} \sqbrk {\set x} \ne \O$
where $f^{-1} \sqbrk {\set x}$ denotes the preimage of $\set x$ under $f$.
From the Well-Ordering Principle, $\N$ is well-ordered.
Therefore by Subset of Well-Ordered Set is Well-Ordered, $S = \N_n$ is well-ordered.
We have that $f^{-1} \sqbrk {\set x} \subseteq S$.
Therefore $f^{-1} \sqbrk {\set x}$ is also well-ordered.
Therefore, by definition of well-ordered set, $f^{-1} \sqbrk {\set x}$ has a smallest element.
Let $g: T \to S$ be the mapping defined as:
:$\forall x \in T: g \paren x =$ the smallest element of $f^{-1} \sqbrk {\set x}$
Let $x \in T$.
Then:
:$g \paren x \in f^{-1} \sqbrk {\set x}$
so:
:$f \paren {g \paren x} = x$
Thus:
:$f \circ g = I_T$
and by Identity Mapping is Bijection:
:$I_T: T \to g \sqbrk T$ is a bijection.
By Cardinality of Subset of Finite Set:
:$\card {g \sqbrk T} \le n$
Let $\card {g \sqbrk T} = m$.
By Set Equivalence behaves like Equivalence Relation:
:$\card T = m$
elements.
Suppose $m = n$.
Then by Cardinality of Subset of Finite Set:
:$g \sqbrk T = S$
so $g: T \to S$ is a bijection.
Therefore:
{{begin-eqn}}
{{eqn | l = f
      | r = f \circ I_S
      | c = 
}}
{{eqn | r = f \circ g \circ g^{-1}
      | c = 
}}
{{eqn | r = I_S \circ g^{-1}
      | c = 
}}
{{eqn | r = g^{-1}
      | c = 
}}
{{end-eqn}}
So $f: S \to T$ is a bijection.
{{Qed}}
Theorem: Equivalence of Mappings between Finite Sets of Same Cardinality

Let $S$ and $T$ be finite sets such that $\card S = \card T$.
Let $f: S \to T$ be a mapping.
Then the following statements are equivalent:
:$(1): \quad f$ is bijective
:$(2): \quad f$ is injective
:$(3): \quad f$ is surjective.

Proof:
$(2)$ implies $(3)$:
Let $f$ be an injection.
Then by Cardinality of Image of Injection:
:$\card S = \card {f \sqbrk S}$
where $f \sqbrk S$ denotes the image of $S$ under $f$.
Therefore the subset $f \sqbrk S$ of $T$ has the same number of elements as $T$.
Therefore:
:$f \sqbrk S = T$
and so $f$ is a surjection.
{{qed|lemma}}
$(3)$ implies $(1)$:
Let $f$ be surjective.
We have that $\card S = \card T$.
By Cardinality of Codomain of Surjection, $f$ is bijective.
{{qed|lemma}}
$(1)$ implies $(2)$:
Let $f$ be a bijection.
By definition of bijection, $f$ is also an injection.
{{qed}}
Theorem: Natural Numbers are Infinite

The set $\N$ of natural numbers is infinite.

Proof:
Let the mapping $s: \N \to \N$ be defined as:
:$\forall n \in \N: \map s n = n + 1$
$s$ is clearly an injection.
{{AimForCont}} $\N$ were finite.
By Equivalence of Mappings between Finite Sets of Same Cardinality it follows that $s$ is a surjection.
But:
:$\forall n \in \N: \map s n \ge 0 + 1 > 0$
So:
:$0 \notin \Img s$
and $s$ is not a surjection.
From this contradiction it is seen that $\N$ cannot be finite.
So, by definition, $\N$ is infinite.
{{Qed}}
Theorem: Finite Non-Empty Subset of Totally Ordered Set has Smallest and Greatest Elements

Let $\struct {S, \preceq}$ be a totally ordered set.
Then every finite $T$ such that $\O \subset T \subseteq S$ has both a smallest and a greatest element.

Proof:
Let $A \subseteq \N_{>0}$ such that every $B \subseteq S$ such that $\card B = n$ has a greatest and a smallest element.
Any $B \subseteq S$ such that $\card B = 1$ has $1$ element, $b \in B$ say.
Then $b$ is both the greatest and smallest element of $B$.
So $1 \in A$.
Let $n \in A$.
Let $B \subseteq S$ such that $\card B = n + 1$.
Then $\exists b \in B$, and $\card {B \setminus \set b} = n$ elements by Cardinality Less One.
So, by the induction hypothesis, $B \setminus \set b$ has a greatest element $c$ and a smallest element $a$, as $n \in A$.
Note that $b \ne c$ as $c \in B \setminus \set b$ but $b \notin B \setminus \set b$.
We have that $\struct {S, \preceq}$ is a totally ordered set.
Hence by the Trichotomy Law, either $b \prec c$ or $c \prec b$ as $b \ne c$.
If $b \prec c$ then $c$ is the greatest element of $B$, otherwise it's $b$.
Similarly, either $b \prec a$ or $a \prec b$, and thus either $a$ or $b$ is the smallest element of $B$.
Either way, $B$ has both a greatest and a smallest element, and therefore $n + 1 \in A$.
Therefore, by the Principle of Mathematical Induction, $A = \N_{>0}$ and the proof is complete.
{{qed}}
Theorem: Finite Non-Empty Subset of Totally Ordered Set has Smallest and Greatest Elements

Let $\struct {S, \preceq}$ be a totally ordered set.
Then every finite $T$ such that $\O \subset T \subseteq S$ has both a smallest and a greatest element.

Proof:
The result follows from:
: Finite Non-Empty Subset of Ordered Set has Maximal and Minimal Elements
: Minimal Element of Chain is Smallest Element
: Maximal Element of Chain is Greatest Element
{{qed}}
Theorem: Unique Isomorphism between Equivalent Finite Totally Ordered Sets

Let $S$ and $T$ be finite sets of the same cardinality.
That is:
:$\card S = \card T$
Let $\struct {S, \preceq}$ and $\struct {T, \preccurlyeq}$ be totally ordered sets.
Then there is exactly one order isomorphism from $\struct {S, \preceq}$ to $\struct {T, \preccurlyeq}$.

Proof:
It is sufficient to consider the case where $\struct {T, \preccurlyeq}$ is $\struct {\N_n, \le}$ for some $n \in \N$.
Let $A$ be the set of all $n \in \N$ such that if:
:$(1): \quad S$ is any set such that $\card S = n$, and
:$(2): \quad \preceq$ is any total ordering on $S$
then there is exactly one isomorphism from $\struct {S, \preceq}$ to $\struct {\N_n, \le}$.
$\O \in A$ from Empty Mapping is Mapping and Equivalence of Mappings between Finite Sets of Same Cardinality.
Now let $n \in A$.
Let $\struct {S, \preceq}$ be a totally ordered set with $n + 1$ elements.
By Finite Non-Empty Subset of Totally Ordered Set has Smallest and Greatest Elements, $S$ has a greatest element $b$.
Then $\card {S \setminus \set b} = n$ by Cardinality Less One.
The total ordering on $S \setminus \set b$ is the one induced from that on $S$.
So as $n \in A$, there exists a unique order isomorphism $f: S \setminus \set b \to \struct {\N_n, \le}$.
Let us define the mapping $g: S \to \N_{n + 1}$ as follows:
:$\forall x \in S: \map g x = \begin{cases}
\map f x: & x \in S \setminus \set b \\
n: & x = b
\end{cases}$
This is the desired order isomorphism from $\struct {S, \preceq}$ to $\struct {\N_{n + 1}, \le}$.
Now let $h: \struct {S, \preceq}$ to $\struct {\N_{n + 1}, \le}$ be an order isomorphism.
Then $\map h b = n$ (it has to be).
So the restriction of $h$ to $S \setminus \set b$ is an isomorphism from $S \setminus \set b$ to $\struct {\N_n, \le}$, and hence $h = f$ (as $n \in A$, any such order isomorphism is unique).
Thus:
:$\forall x \in S \setminus \set b: \map h x = \map f x = \map g x$
and:
:$\map h b = n = \map g b$
thus $h = g$.
Therefore $n + 1 \in A$.
The result follows from the Principle of Mathematical Induction.
{{qed}}
Theorem: Isomorphism to Closed Interval

Let $m, n \in \N$ such that $m < n$.
Let $\closedint {m + 1} n$ denote the integer interval from $m + 1$ to $n$.
Let $h: \N_{n - m} \to \closedint {m + 1} n$ be the mapping defined as:
:$\forall x \in \N_{n - m}: \map h x = x + m + 1$
Let the orderings on $\closedint {m + 1} n$ and $\N_{n - m}$ be those induced by the ordering of $\N$.
Then $h$ a unique order isomorphism.

Proof:
First note that the cardinality of $\closedint {m + 1} n$ is given by:
:$\card {\closedint {m + 1} n} = n - m$
From Unique Isomorphism between Equivalent Finite Totally Ordered Sets, it suffices to show that $h$ is an order isomorphism.
To this end, remark that, for all $x, y \in \N_{n - m}$:
{{begin-eqn}}
{{eqn | l = \map h x
      | r = \map h y
}}
{{eqn | ll= \leadstoandfrom
      | l = x + m + 1
      | r = y + m + 1
}}
{{eqn | ll = \leadstoandfrom
      | l = x
      | r = y
      | c = Natural Number Addition is Cancellable
}}
{{end-eqn}}
proving $h$ is an injection.
Hence from Equivalence of Mappings between Finite Sets of Same Cardinality, $h$ is also a bijection.
By Ordering on Natural Numbers is Compatible with Addition and Natural Number Addition is Cancellable for Ordering, it follows that:
:$x \le y \iff \map h x \le \map h y$
so $h$ is an order isomorphism.
{{qed}}
Theorem: Regular Representation wrt Cancellable Element on Finite Semigroup is Bijection

Let $\left({S, \circ}\right)$ be a finite semigroup.
Let $a \in S$ be cancellable.
Then:
:the left regular representation $\lambda_a$
and:
:the right regular representation $\rho_a$
of $\left({S, \circ}\right)$ with respect to $a$ are both bijections.

Proof:
By Cancellable iff Regular Representations Injective, $\lambda_a$ and $\rho_a$ are injections.
We have that $S$ is finite.
From Injection from Finite Set to Itself is Surjection, both $\lambda_a$ and $\rho_a$ are surjections.
Thus $\lambda_a$ and $\rho_a$ are injective and surjective, and therefore bijections.
{{qed}}
Category:Semigroups
Category:Regular Representations
Category:Cancellability
k62vgwldwv4np50anvdp0y1qep88fep
Theorem: Power Set of Natural Numbers is Uncountable

The power set $\powerset \N$ of the natural numbers $\N$ is uncountable.

Proof:
There is no bijection from a set to its power set.
From Injection from Set to Power Set, we have that there exists an injection $f: \N \to \powerset \N$.
From the Cantor-Bernstein-Schröder Theorem, there can be no injection $g: \powerset \N \to \N$.
So, by definition, $\powerset \N$ is uncountable.
{{qed}}
Theorem: Subset of Countably Infinite Set is Countable

Every subset of a countably infinite set is countable.

Proof:
Let $S = \set {a_0, a_1, a_2, \ldots}$ be countably infinite.
Let $T \subseteq S = \set {a_{n_0}, a_{n_1}, a_{n_2}, \ldots}$, where $a_{n_0}, a_{n_1}, a_{n_2}, \ldots$ are the elements of $S$ also in $T$.
If the set of numbers $\set {n_0, n_1, n_2, \ldots}$ has a largest number, then $T$ is finite.
Otherwise, consider the bijection $i \leftrightarrow n_i$.
This leads to the bijection $i \leftrightarrow a_{n_i}$
This latter bijection is the required one-to-one correspondence between the elements of $T$ and those of $\N$, showing that $T$ is indeed countable.
{{finish|formal justification}}
Theorem: Infinite Set has Countably Infinite Subset

Every infinite set has a countably infinite subset.

Proof:
Let $S$ be an infinite set.
We use Between Two Sets Exists Injection or Surjection.
Suppose that there exists an injection $\psi: \N \to S$.
Let $T$ be the image of $\psi$.
From Injection to Image is Bijection, it follows that $\psi^{-1}: T \to \N$ is a bijection.
Hence, $T$ is a countably infinite subset of $S$.
Now, suppose that that there exists a surjection $\phi: \N \to S$.
From Surjection from Natural Numbers iff Countable, it follows that $S$ is countably infinite.
So, from Set is Subset of Itself, we have that $S$ is a countably infinite subset of $S$.
{{qed}}
Theorem: Infinite Set has Countably Infinite Subset

Every infinite set has a countably infinite subset.

Proof:
Let $S$ be an infinite set.
First an injection $f: \N \to S$ is constructed.
Let $g$ be a choice function on $\powerset S \setminus \set \O$.
Then define $f: \N \to S$ as follows:
:$\forall n \in \N: \map f n = \begin {cases} \map g S & : n = 0 \\ \map g {S \setminus \set {\map f 0, \ldots, \map f {n - 1} } } & : n > 0 \end {cases}$
Since $S$ is infinite, $S \setminus \set {\map f 0, \ldots, \map f {n - 1} }$ is non-empty for each $n \in \N$.
Therefore $f \sqbrk \N$ is infinite.
To show that $f$ is injective, let $m, n \in \N$, say $m < n$.
Then:
:$\map f m \in \set {\map f 0, \ldots, \map f {n - 1} }$
but:
:$\map f n \in S \setminus \set {\map f 0, \ldots, \map f {n - 1} }$
Hence $\map f m \ne \map f n$.
Since $f$ is injective, it follows from Injection to Image is Bijection that $f$ is a bijection from $\N$ to $f \sqbrk \N$.
Thus $f \sqbrk \N$ is a countable subset of $S$.
{{Qed}}
Theorem: Infinite Set has Countably Infinite Subset

Every infinite set has a countably infinite subset.

Proof:
Let $S$ be an infinite set.
First an injection $f: \N \to S$ is constructed.
Let $f$ be a choice function on $\powerset S \setminus \set \O$.
That is:
:$\forall A \in \powerset S \setminus \set \O: \map f A \in A$
This is justified only if the Axiom of Choice is accepted.
Let $\CC$ be the set of all finite subsets of $S$.
Let $A \in \CC$.
Since $S$ is infinite it follows that $S \setminus A \ne \O$.
So $S \setminus A \in \Dom f$.
Let $g: \CC \to \CC$ be the mapping defined as:
:$\map g A = A \cup \set {\map f {S \setminus A} }$
That is, $\map g A$ is constructed by joining $A$ with the element that $f$ chooses from $S \setminus A$.
Consider the Recursion Theorem applied to $g$, starting with the set $\O$.
We obtain a mapping $U: \N \to \CC$ such that:
:$\map U x = \begin{cases}
\O & : x = 0 \\ \map U n \cup \set {\map f {S \setminus \map U n} } & : x = n^+
\end{cases}$
where here $\N$ is considered as the set of elements of the von Neumann construction of natural numbers.
Consider the mapping $v: \N \to S$, defined as:
:$\forall n \in \N: \map v n = \map f {S \setminus \map U n}$
We have that, by definition of $v$:
:$(1): \quad \forall n \in \N: \map v n \notin \map U n$
:$(2): \quad \forall n \in \N: \map v n \in \map U {n^+}$
:$(3): \quad \forall m, n \in \N: n \le m \implies \map U n \subseteq \map U m$
Then because $\map v n \in \map U m$ but $\map v m \notin \map U m$:
:$(4): \quad \forall m, n \in \N: n < m \implies \map v n \ne \map v m$
So $(4)$ implies that $v$ maps distinct elements of $\N$ onto distinct elements of $S$.
Thus $v: \N \to S$ is an injection.
It follows from Injection to Image is Bijection that $v$ is a bijection from $\N$ to $\map v \N$.
Thus $\map v \N$ is the countable subset of $S$ that was required.
{{Qed}}
Theorem: Infinite Set has Countably Infinite Subset

Every infinite set has a countably infinite subset.

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

A finite set can not be in one-to-one correspondence with one of its proper subsets.
That is, a finite set is not Dedekind-infinite.

Proof:
Let $S$ be a finite set.
Let $T$ be a proper subset of $S$.
Let $f: T \to S$ be an injection.
By Cardinality of Image of Injection and Cardinality of Subset of Finite Set:
:$\card {\Img f} = \card T < \card S$
where $\Img f$ denotes the image of $f$.
Thus $\Img f \ne S$, and so $f$ is not a bijection.
{{qed}}