Definition 66: Von Neumann Numerals

The von Neumann numeral ${𝑁}_{𝑘}$ for a natural number $𝑘$ is defined as the set of all von Neumann numerals less than $𝑘$, or $\varnothing$ if $𝑘=0$. Formally:

Definition 67: Successor Function

The successor function, denoted $\text{succ}$, is defined as follows:

Definition 68: Zermelo-Fraenkel Axioms

1. Extensionality. Two sets are equal if and only if they have the same elements:

   $$\forall 𝑥\forall 𝑦\left[\forall 𝑧\left(𝑧\in 𝑥\iff 𝑧\in 𝑦\right)\Rightarrow 𝑥=𝑦\right].$$
2. Regularity.