How can I axiomatically prove that infinitely many tuples exist?

Using Kuratowskis definition of n-tuples, we get:

$$\langle ~ \rangle := \emptyset \\ \langle a_1 \rangle := a_1 \\ \langle a_1,a_2 \rangle := \{\{a_1 \},\{ a_1,a_2 \} \} \\ \langle a_1, a_2, …, a_{n+1} \rangle := \langle \langle a_1, a_2, …, a_n \rangle, a_{n+1} \rangle$$

We can simply prove the existence of arbitrarily many n-tupels by applying the axiom of pairing. Let $$a_1$$ and $$a_2$$ be arbitrary sets. By the axiom of pairing, we get $$\{a_1\}$$ and $$\{a_1,a_2\}$$. Using the axiom of pairing again, we get $$\{\{a_1\}, \{\{a_1,a_2\}\}$$ and, by the above definition, $$\langle a_1, a_2 \rangle$$. You can define n-tuples easily this way. Nonetheless, you will only get finitely many n-tuples.

Now since there are functions with infinite domains and (the graphs of) functions are defined as sets of tuples, there must also be infinitely many tuples. But how do the axioms of set theory guarantee that this is the case?

It seems to me that the axiom of replacement plays an important role here in combination with the axiom of infinity. Define the natural numbers as the cut of all inductive subsets of the powerset of any set A the axiom of infinity specifies:

$$\mathbb{N} := \bigcap \{x\in\mathfrak{P}(A)\mid\forall y (y\in A \to y\cup\{y\}\in A)\}$$

Now replace every element of $$\mathbb{N}$$ by a tuple. That's the informal idea. Let $$\alpha[x,y]$$ be an open formula containing only $$x$$ and $$y$$ free. The formal idea is to find a substitution instance for the following axiom:

$$\forall x\forall y\forall z(\alpha[x,y] \land \alpha [x,z] \to y=z) \to \forall x\exists y\forall z(z\in y \leftrightarrow \exists x'(x'\in x \land \alpha[x',z]))$$

Now I have two questions:

1. How exactly does the substitution instance look like? Why are there equivalent formulations of the axiom of replacement which feature replacement functions?
2. There of course are infinitely many tuples. But are there also tuples with infinitely many components, e.g. $$\langle 0,1,2,...\rangle$$? If so, how can you prove it? If not, how can you prove it?
• There's no need for replacement in the first question. For example, here's a hint for how to obtain the graph of the successor function $\mathbb{N}\to\mathbb{N}$: note first that $\langle m,n\rangle$ is an element of $M:=\mathfrak{P}(\mathfrak{P}(\mathbb{N}))$ for every $m,n\in \mathbb{N}$. Then try to use the axiom of restricted comprehension on $M$ to get a set that looks like $\{\langle n,n+1\rangle:n\in\mathbb{N}\}$. Dec 13, 2021 at 1:19
• For the second question, it depends on what exactly you mean by a tuple with infinitely many components; the recursive definition of an $n$-tuple only tells you what a finite tuple looks like. What would you like the "shape" of an infinite tuple to look like? Dec 13, 2021 at 1:19
• As to the first question: You're absolutely right. You can just take $\{\langle x,y \rangle \mid x \in y \}$ as a condition to get $>$, which is a superset of the set you describe. It obviously has infinitely many tuples as elements. As to the second question. That's already a partial answer: Tuples are not defined to have infinitely many components. You define n-tuples. Thank you for the insight already. Could you go into some detail as to why it is possible to formulate the axiom of replacement by means of a choice function? Dec 13, 2021 at 10:38