I am confused about an issue in set theory.

Tychonoff's theorem says that "an arbitrary product of compact topological spaces is compact". We often talk of an index set $I$ and then for each $n\in I$ we have a compact topological space $X_n$, and the claim is that $\prod_{n\in I}X_n$ is compact. There's a really cool super-short proof of this using filters by the way ;-)

My question is about how one might formalise this in ZFC. In Lean I just found myself writing X : I → Type for the family, and in the set theory model of Lean this is a "function" from a set $I$ to "the universe of all sets". This can't be done in ZFC, so one might want to start brandishing the axiom of replacement around a bit. My question is I think on the details of this.

Let's say I'm talking to you, a set theorist, and I ask you what your definition of a topological space structure is. You say it's an ordered pair consisting of a set $X$ and a topology $\mathcal{T}$ on $X$, which is a collection of subsets of $X$ satisfying some axioms. I say great, I write a few lines of computer code (just a small interface corresponding to your definition), run a proof checking system on my code, and it outputs a Haskell function which takes as input a natural number n and then prints out two strings which uniquely define a set X n and a topology T n on X n. To be more precise, for an input n it actually prints out a term which a set theory-based theorem prover such as Mizar or Metamath can understand -- it makes no "external" assumptions about the explicit model of ZFC we're working in, and X n and T n are provably well-defined unique objects. Furthermore I can prove that X n is compact for all n and indeed a computer has checked my proof, but I won't bore you with the details. The question is how now to state that the product of the X n is compact in ZFC, because I have not given you a function in the internal sense of a set which happens to be a function in the sense that it's a set of ordered pairs blah blah blah.

What I am unclear about is whether one can make the set of pairs $(n,X_n)$ in ZFC in order to be able to form the product needed to state Tychonoff's theorem.