Can I deduce ZFC Standard from "ZFC Dedekind"?

Question

ZFC Standard: Infinity, Extensionality, Specification, Pairing, Union, Replacement, Power Set, Choice and Regularity.
ZFC Dedekind: Infinity replaced bij Dedekind Inifinity, other 8 axioms the same as standard.
Infinity in ZFC Standard: the existence of a succesor set $S$ with $\emptyset\in S$ and for every $x \in S$ $x \cup \{x\} \in S$ .
Dedekind Infinity: the existence of a Dedekind-set $D$ having a proper subset $E$ that is equipollent to $D$. Equipollent means: there exists a property $P(x,y)$ of sets such that for every $x \in D$ there exists an unique $y \in D$ such that $P(x,y)$ holds and reversely there exists for every $y \in E$ an unique $x \in D$ such that $P(x,y)$ holds.

Starting form the existence of $D$ en from the 8 other axioms, I would like to prove the existence of $S$.

I managed to do the following. The property $P(x,y)$ induces een class relation $f$, defined bij $(x,y) \in f$ iff $P(x,y)$. The restriction of $f$ to D is a bijection $D \to E$. For a $d_0 \in D\setminus E$ define the set $N$ to be the intersection of all sets $X\subseteq D$ such that $d_0 \in X$ and such that $f(x) \in X$ for every $x \in X$. It can be proved that the Peano axioms hold for $N$ with zero $d_0$ and successor function $f$. So $N$ can be truly seen as an instance of the set of natural numbers.
I also managed to prove the Recursion Theorem for $N$. That is, given an set $A$, een $N$-recursive definition leads to a well defined and unique function $a: N \to A$. Now take $S=\{a(x):x \in N\}$ where $a(d_0)=\emptyset$ and $a(f(x))=a(x) \cup \{a(x)\}$. $S$ satisfies the conditions and by Replacement $S$ is a set because $N$ is as set. So it seems done.

But what should I choose for the set $A$?

Answer 1

We are given $D, E, P$ and pick some $d_0\in D\setminus E$. Say that $G$ is a nice graph if

1. $G\subseteq D\times\alpha$ for some ordinal $\alpha$
2. $\langle d_0,\emptyset\rangle\in G$
3. $\langle d,x\rangle,\langle d,y\rangle\in G\to x=y$
4. $\langle d,x\rangle,\langle e,y\rangle\in G, P(d,e)\to y=S(x)$
5. $d\in D, e\in \operatorname{dom}(G), P(d,e)\to d\in\operatorname{dom}(G)$

[The intention is that $G$ is the graph of an order-preserving bijection of an initial segemant of $D$ with (an initial segment of) an ordinal]

Say that $D'\subseteq D$ is a nice domain if there exists exactly one nice graph $G$ with $\operatorname{dom}(G)=D'$.

Say that $d\in D$ is a nice point if there exists a unique $y$ such that $\langle d,y\rangle \in G$ for every nice graph with a nice domain containing $d$. Then we have a class function $\phi$ that maps a nice point $d$ to that unique $y=:\phi(d)$. Let $N$ be the set of nice points, and by the Axiom Schema of Replacement let $\Omega=\{\,\phi(d):d\in N\,\}$.

We note that $\{\langle d_0,\emptyset\rangle \}$ is a nice graph. By conditions 2 and 3, this makes $\{d_0\}$ a nice domain and $d_0$ a nice point with $\phi(d_0)=\emptyset$, so that ultimately $\emptyset\in\Omega$.

Next let $d\in N$ and let $e\in E$ be the unique element with $P(d,e)$. Since $d$ is a nice point, there exists a nice domain $D'\ni d$. Let $G$ be the unique nice graph with domain $D'$. Then $D'\cup \{e\}$ is also a nice domain. For if $e\notin D'$ then $G\cup\{\langle e,S(\phi(d))\rangle\}$ is a nice graph and easily verified to be unique with this domain, given the uniqueness of $G$ over $D'$. This, together with the observation that every nice domain containing $e$ also contains $d$, makes $e$ a nice point with $\phi(e)=S(\phi(d))$. We conclude that $\Omega$ is closed under $S$, i.e., $\Omega$ is an inductive set.

Answer 2

It is easier to start with an equivalent definition of Dedekind-infinite:

A set $X$ is Dedekind-infinite iff there exists $f:X\to X$ where $f$ is injective but not surjective.

Since $D$ is Dedekind-infinite, there must exist $f:D\to D$ where $f$ is injective but not surjective.

Since $f$ is not surjective, there must exist $x_0\in D$ such that for all $x\in D$ we have $f(x)\ne x_0$.

Construct subset $N\subseteq D$ such that $N=\{x_0, f(x_0), f(f(x_0)), \cdots\}$

More formally, apply Specification to obtain:

$\forall a:[a\in N \iff a\in D \land \forall b:[x_0\in b \land \forall c:[c\in b \land c \in D \implies f(c)\in b] \implies a \in b]]$

Construct $S:N\to N$ such that $S(x)=f(x)$

$(N,S,x_0)$ can then be shown to satisfy the usual Peano axioms where $S$ is the successor function on $N$ and $x_0$ is the first element of $N$.

Answer 3

Since a Dedekind infinite set cannot be in bijection with any finite ordinals, the set of all ordinals that inject into is an infinite ordinal. So we can define $\omega$ which is the smallest inductive set.