For given set $A$, show that there exist a set of 'every finite sequence on $A$'.

Question

To be specific, I'll state some definitions first.

1. $0=\emptyset$
   $1=\{\emptyset\}=\{0\}$
   $2=\{\emptyset,\{\emptyset\}\}=\{0,1\}$
   ...
   $n=\{0,1,2,....,n-1\}$

2. For given set $\text A$ and $\text B$,
   $\text B^\text A=\{ f\in P(\text A \times \text B) $ | $ f:\text A \to \text B \}$

3. Any function $f:n\to \text{A} $ is finite sequence.
   Any function $f:\mathbb N \to \text A$ is infinite sequence.

In terms of above definitions, $$\bigcup_{n\in \mathbb N} A^n $$ is set of every finite sequence on $A$.

I want to prove this set exists. If I prove $J=\{\text A^0,\text A^1, \text A^2, ....\}$ exists, above set exsits by Axiom of union.

But I have no idea how to prove $J$ exists. I know each $\text A^n$ exist. but how can I construct such a big set?
I'm sure that I can't apply Axiom of pair infinitely many times.

Answer 1

This is exactly what the Axiom of Replacement is for. Once you know $\mathbb N$ exists, the Axiom of Replacement guarantees that $$ \{ A^i \mid i \in \mathbb N \} $$ is a set.

Answer 2

Either use the Axiom Schema of Replacement, $$J=\{\,A^n\mid n\in\Bbb N\,\} $$ Or note that all $A^n$ are subsets of $P(\Bbb N\times A)$ and use the Axiom Schema of Separation from there.