Can anybody look over my proposed proof for Exercise 3.5.2 B in Analysis I by Tao? The goal is to prove that the cartesian product of $X_1,...X_n $ exists rigorously. I've seen other attempts on this forum, but those proofs merely showed existence; they did not show that the resulting set had the desired properties of the cartesian product.
One thing to note is that Tao technically defines the cartesian product over an n-tuple of sets $(X_1,...,X_n)$ rather than as a product of the sets themselves, but I don't think it impacts my proof.
Let $i,n∈N$, and let $X_i$ be a set for $1≤i≤n.$ The cartesian product $X_1×…×X_n$ is defined as a set such that
$$X_1×…×X_n=\{(x_1,...x_n) : x_i\in X_i\text{ for all } 1\le i \le n\}$$
where $(x_1,…,x_n)$ is an ordered n-tuple. The cartesian product has the property that
$$p \in X_1\times...\times X_n \iff p\text{ is an ordered } n \text{-tuple and }p_i\in X_i \text{ for all } 1\le i \le n.$$
We can define an ordered n-tuple $x=(x_1,…,x_n)$ as a surjective function from $\{i∈N | 1≤i≤n\}$ to some other set $X$, which can vary from ordered n-tuple to ordered n-tuple. We denote $x_i=x(i)$ for all $i∈{1,…,n}$. Of course, the codomain of a surjective function is completely determined by its domain and functional values on its domain, since $$f(\text{dom } f)=\{f(i) | i∈\text{ dom } f\}=\text{codomain of }f$$
We can show that $Λ$, defined below, exists using the various axioms of set theory. $$Λ=\{ f∈Γ^D │f\text{ is a surjective function with dom }f=D \text{ and }f(i)∈X_i \text{ for all }1≤i≤n)\}$$
where $D=\{1,…,n\}$, $Γ=⋃_{1≤i≤n}X_i$ , and $Γ^D$ is the set of partial functions from domain $D$ to codomain $Γ$.
First, note that $D=\{i∈N | 1≤i≤n\}$ is well-defined from the axiom of specification and the axiom of infinity. Γ is well-defined from the axiom of union, and $Γ^D$ is well-defined from the power set axiom. Finally, $Λ$ is defined from the axiom of specification. It remains to show that $Λ$ has the defining property of the cartesian product described above.
To demonstrate this, let $p∈Λ$, so that $p∈Γ^D$ is a surjective function from $D$ to a subset of $Γ$, and for all $1≤i≤n$, $p(i)∈X_i$. It immediately follows (by definition) that $p$ is an ordered n-tuple (as it is surjective and has the correct domain) and $p_i=p(i)∈X_i$ for all $1≤i≤n$.
Alternatively, let $p$ be an ordered n-tuple with $p_i∈X_i$ for all $1≤i≤n$. It follows that $p$ is a surjective function with domain $D$ and some codomain, and that $p_i=p(i)$ for all $1≤i≤n$. It remains to show that the codomain of $p$ is a subset of $Γ$, which would imply that $p∈Γ^D$ and thus $p∈Λ$. As discussed above, the codomain of a surjective function is defined entirely by its domain and functional values, so that $$C(p)=\text{codomain of }p=p(\text{dom }p)=\{p(i) | 1≤i≤n\}$$
To show that $C(p)⊆Γ$, it suffices to show that $c∈C(p)→c∈Γ$. Indeed, let $c∈C(p)$ so that $c=p_m$ for some $1≤m≤n$. $p_m∈X_m$ by assumption, so that $p_m∈⋃_{1≤i≤n}X_i =Γ$. Thus $p∈\Lambda$ as desired.