Product of compacts is compacts using closedness of projection to second component?

Question

A well known characterization of compactness says $X$ is compact iff for all spaces $Y$ the projection $X\times Y\rightarrow Y$ is a closed map.

I'm wondering whether there's some simple formal way to prove a (finite?) product of compacts is compact using this characterization.

Let $X,Y$ be compact. Starting with $\pi _X:X\times Z\rightarrow Z,\pi _Y:Y\times Z\rightarrow Z$, which we know are closed, how can we move (categorically) to $\pi_{X\times Y}:(X\times Y)\times Z\rightarrow Z$ and show it's closed?

Added. Just to clarify - I'm looking for a formal (categorical as possible) way to prove this. So far the most elegant proof I can think of uses the fact a closed map with compact fibers is proper:

Short proof. If $X$ is compact, $\pi:X\times Y\rightarrow Y$ is closed (tube lemma). The fibers of $\pi$ are all homeomorphic to $X$ and hence are all compact, therefore $\pi$ is proper. If $Y$ is compact, so must be it's preimage, $X\times Y$.

Answer 1

Let us say that a continuous map $f : X \to S$ is universally closed if, for every continuous map $g : Y \to S$, the projection $\{ (x, y) \in X \times Y : f (x) = g (y) \} \to Y$ is closed. The characterisation of compactness you allude to is this:

A topological space $X$ is compact if and only if the unique map $X \to 1$ is universally closed.

It is easy to verify the following:

• The class of universally closed maps is closed under pullback.
• The class of universally closed maps is closed under composition.

(Use the pullback pasting lemma.)

We obtain the following corollary:

• The class of universally closed maps is closed under binary product.

Indeed, given universally closed maps $f_0 : X_0 \to S_0$ and $f_1 : X_1 \to S_1$, we have the following pullback diagrams, $$\require{AMScd} \begin{CD} X_0 \times X_1 @>>> X_0 \\ @V{f_0 \times \mathrm{id}_{X_1}}VV @VV{f_0}V \\ S_0 \times X_1 @>>> S_0 \end{CD}$$ $$\begin{CD} S_0 \times X_1 @>>> X_1 \\ @V{\mathrm{id}_{S_0} \times f_1}VV @VV{f_1}V \\ S_0 \times S_1 @>>> S_1 \end{CD}$$ so by taking the composite of the left vertical arrows, it follows that $f_0 \times f_1 : X_0 \times X_1 \to S_0 \times S_1$ is universally closed. In particular, the product of two compact topological spaces is compact.

Incidentally, universally closed maps are the same as proper maps.