Dès que l'on dispose des axiomes de l'ensemble vide, de la paire, et de la réunion, l'ensemble A dont on a affirmé l'existence contient pour chaque entier naturel un représentant, que l'on va prendre comme définition en théorie des ensembles. Par exemple 1 étant successeur de 0, et le singleton d'élément l'ensemble vide (c'est-à-dire 0) :
De même, 2 en tant que successeur de 1, est la paire {0,1} :
et ainsi de suite. Une conséquence de cette définition est que chaque nombre entier est égal à l'ensemble de tous les nombres entiers qui le précèdent. Ainsi l'axiome affirme essentiellement qu’il existe un ensemble contenant tous les nombres entiers naturels.
L'existence de chacun de ces entiers est assurée sans axiome de l'infini, mais on utilise celui-ci pour montrer que l'ensemble des entiers naturels existe. On peut former en effet un ensemble, noté ω en théorie des ensembles, qui est l'intersection de tous les ensembles contenant 0 et clos par successeur (c'est-à-dire le plus petit au sens de l'inclusion des ensembles contenant 0 et clos par successeur). Pour que cette définition soit correcte, il faut intuitivement que la classe des ensembles contenant 0 et clos par successeur soit non vide, ce qu'assure l'axiome de l'infini. Plus formellement l'existence de ω est assurée par le schéma d'axiomes de compréhension et son unicité par l'axiome d'extensionnalité. En effet, notons Cl(Y) pour « ∅ ∈ Y et ∀ y (y ∈ Y ⇒ y ∪ {y} ∈ Y) », c'est-à-dire « Y est clos par successeur et 0 lui appartient », et soit A un ensemble vérifiant Cl(A) dont l'existence est assurée par l'axiome de l'infini, alors ω se définit ainsi (A n'intervient que pour pouvoir définir ω, mais ω ne dépend pas de A) :
La définition même de l'ensemble ω donne un énoncé du principe de récurrence sur les entiers : tout ensemble à qui 0 appartient et qui est clos par successeur est un sur-ensemble de ω. On peut en donner un énoncé un peu plus familier mais équivalent en théorie des ensembles par le schéma de compréhension, on note x+ le successeur de x, on a alors pour une propriété arbitraire exprimée dans le langage de la théorie des ensembles par la formule P x a1…ak (pas d'autre variable libre) :
La récurrence est valide pour toute propriété exprimée dans le langage de la théorie des ensemble : ce n'est pas anodin, cela fait de cette récurrence une propriété beaucoup plus forte que la récurrence de l'arithmétique de Peano (comme théorie du premier ordre), le langage de la théorie des ensembles étant strictement plus expressif que celui de l'arithmétique de Peano.
Pour qu'il soit tout à fait légitime de considérer ω comme l'ensemble des entiers naturels, il reste à vérifier que le successeur est bien injectif : comme un successeur, qui est un ensemble non vide, ne peut jamais être nul, cela confirme que l'ensemble construit est bien infini au sens intuitif. De plus, comme la propriété de récurrence est conséquence directe de la définition de l'ensemble des entiers naturels, on aura vérifié ainsi les axiomes de Peano, qui sont donc des théorèmes dans ce contexte, et qui associés aux axiomes de la théorie des ensembles, permettent de construire les ensembles de nombres usuels comme les relatifs, les rationnels, les réels, les complexes, ...
Une façon simple pour obtenir cette propriété est d'étudier la structure définie par la relation d'appartenance sur les entiers que l'on a construit : on montre qu'il s'agit d'un ordre strict total (et la propriété de récurrence dit alors que c'est un bon ordre). On peut utiliser la propriété de récurrence, qui est déjà démontrée.
On montre que tout élément d'un entier est un entier par une récurrence immédiate. La transitivité de l'appartenance sur les entiers naturels s'écrit alors :
c'est-à-dire :
tout élément d'un entier en est aussi un sous-ensemble. Cette propriété se démontre à nouveau par récurrence. Elle est évidente pour l'ensemble vide. On la suppose pour x entier. Un élément de x+ est alors soit x, inclus donc dans x+=x ∪ {x}, soit appartient à x et on conclut par hypothèse de récurrence. On dit aussi que les entiers naturels sont des ensembles transitifs, et c'est également le cas de ω.
On montre maintenant l'irréflexivité de l'appartenance sur les entiers naturels : aucun entier naturel n'appartient à lui-même :
Cette propriété se démontre par récurrence à l'aide de la propriété précédente. Elle est évidente pour l'ensemble vide. On la suppose pour x entier. On suppose que x+ ∈ x+ et on montre que c'est absurde. Deux cas sont possibles : soit x+=x, mais alors x ∈ x ce qui contredit l'hypothèse de récurrence ; soit x+ ∈ x et d'après la propriété précédente x+ ⊂ x, donc x ∈ x ce qui contredit à nouveau l'hypothèse de récurrence.
L'appartenance définit donc bien un ordre strict sur les entiers. Pour montrer la totalité, on caractérise d'abord l'ordre large sur les entiers correspondant à l'ordre strict de l'appartenance : c'est l'inclusion. On doit donc montrer l'équivalence :
La réciproque a déjà été démontrée (c'est essentiellement la transitivité de l'appartenance). On montre par récurrence sur x que tout entier naturel qui est sous-ensemble de x est soit x, soit un élément de x. Elle est évidente pour l'ensemble vide. Supposons là pour l'entier x. Soit y un entier sous-ensemble de x+=x ∪ {x}. Si x ∈ y, alors x ⊂ y, donc x+ ⊂ y donc x+ = y. Sinon, y est sous-ensemble de x : par hypothèse de récurrence, c'est soit x, élément de x+, soit un élément de x donc de x+.
On peut maintenant montrer la totalité, à savoir que deux entiers distincts sont toujours comparables par l'appartenance :
On démontre la totalité par récurrence sur x. L'ensemble vide est élément de tout entier naturel qui est un successeur par une récurrence immédiate, et on a donc le résultat quand x est vide. Supposons la propriété pour x :
Soit donc un entier naturel y quelconque, si x = y ou y ∈ x, alors y ∈ x+. Reste à traiter le cas x ∈ y. On a donc, d'après la transitivité x+=x ∪ {x} ⊂ y. Alors x+ = y, ou x+ est élément de y, ce qui achève la récurrence.
Une fois définie la structure d'ordre total sur les entiers naturels, on obtient l'injectivité du successeur en montrant qu'il s'agit d'une application strictement croissante sur les entiers naturels. On suppose que x ∈ y. On en déduit par transitivité que x ∪ {x} = x+ ⊂ y, donc x+ ⊂ y+, et x+ ≠ y+, puisque y ∉ y, donc x+ ∈ y+. L'opération successeur est strictement croissante donc injective par totalité de l'ordre.
En résumé, l'axiome de l'infini a permis de définir un ensemble ω qui représente fidèlement les entiers naturels, en particulier parce qu'il vérifie les axiomes de Peano (qui deviennent donc des théorèmes) :
On a démontré directement au passage l'existence d'un bon ordre strict sur les entiers, dont on montre facilement qu'il est la clôture transitive du successeur, c'est-à-dire l'ordre usuel sur les entiers.
Une fois ces propriétés démontrées on peut ignorer la façon dont les entiers ont été construits pour les développements mathématiques usuels. On montre en particulier le principe de définition par récurrence qui permet d'introduire par exemple l'addition, la multiplication, l'exponentielle, etc. Le principe de définition par récurrence permet également de montrer qu'en théorie des ensembles deux structures munies d'un 0 et d'une opération successeur et qui vérifient ces trois axiomes sont isomorphes. La façon dont on les a construits n'est donc pas très importante.
Par là même l'énoncé de l'axiome de l'infini n'a pas le caractère intrinsèque des autres axiomes : l'existence de n'importe quel ensemble qui permet une construction analogue convient. De plus, grâce à la définition par récurrence et au schéma de remplacement, on montre que l'existence de n'importe quel ensemble représentant les entiers a pour conséquence l'existence d'un autre ensemble représentant les entiers, avec un autre choix pour le 0 et le successeur.
Pour relativiser ce qui précède, il faut quand même ajouter que cette construction est particulièrement importante en théorie des ensembles. D'une part elle se généralise aux ordinaux et cette construction des ordinaux joue un rôle fondamental dans la théorie des ensembles moderne. D'autre part elle correspond à l'idée intuitive qui est de caractériser les classes d'équipotence des ensembles finis en en donnant un représentant par classe (chaque entier de von Neumann obtenu en appliquant n fois le successeur à partir de 0, a bien n éléments, (n étant l'entier au sens intuitif), et on choisit de définir un entier comme l'ensemble de tous les entiers qui le précèdent. Cette construction (pour les ordinaux en général) a d'ailleurs été découverte plusieurs fois : si elle a été introduite par Von Neumann en 1923, elle avait été développée de façon plus informelle dans deux articles de Dmitry Mirimanoff en 1917, et par Zermelo en 1915 dans des écrits non publiés.