The Matrix in ZFC: A Set-Theoretic Foundation of Matrices?

Today, we can use ZFC to found all of mathematics. We show from ten or so axioms the existence of everything from ordered pairs and Cartesian products to relations and functions (whose existence follows from the existence of Cartesian products). I have learned, from reading books like Enderton's 1977 Elements of Set Theory, that it is not enough simply to define something (for example, we define the ordered pair of $a$ and $b$ as the set $(a,b)=\{\{a\},\{a,b\}\}$), but we must also prove that what we have defined exists within ZFC.

I have done some searching, but have not found a set-theoretic construction of matrices. Wikipedia's Matrix page states the definition of an $m \times n$ matrix as simply a "rectangular array", but this definition does not show that a matrix is a set which actually exists in ZFC.

Does anyone know how to construct matrices in ZFC? Please feel free to point me in the direction of books in set theory which tackle this. Thanks for reading my question!

Solution 1:

Consider an $m\times n$ matrix with elements in some field $F$. Let $J_m=\{1,2,\ldots, m\}$ and $J_n=\{1,2,\ldots, n\}$, then a matrix can be viewed as a function $a:J_m\times J_n\to F$ with $a(i,j)=a_{ij}$.