Proof That Product of Two Compact Spaces Is Compact w/o Choice Axiom

[poochie_d]

In Theorem 26.7 of Munkres' Topology, it is proved that a product of two compact spaces is compact, and I think the author seems to (rather sneakily) use the choice axiom without mentioning it... Could anyone tell me if this is indeed the case? I don't have a problem with the choice axiom, but it kinda seems unnecessary to have a proof that involves choice when you can instead use the almighty Tychonoff =)

Anyway, here goes the proof:

The first part of the proof proves the tube lemma, which states that:
Given the product space X x Y, where Y is compact, if N is an open set in X x Y containing the slice x0 x Y of X x Y, ,then there is a neighbourhood W of x0 in X such that N contains W x Y (no choice here).

In the second part, the theorem is proved: Suppose X and Y are compact, and let A be an open covering of X x Y. For each element x0 in X, the slice x0 x Y is compact (being homeomorphic to Y), and thus can be covered by finitely many elements A1, ..., Am of A (choice used here?!). The union N = A1 U ... U Am is then an open set containing x0 x Y, so by the tube lemma there is a neighbourhood W_x0 of x0 in X such that W_x0 x Y is contained in N. Now do this for each x0 in X, so you get a neighbourhood W_x0 for each x0. The W_x0's then cover X, which is compact, so a finite number of them, say, W1, ..., Wk, cover X. This implies that W1 x Y, ..., Wk x Y cover X x Y, and since each Wi x Y is in turn covered by finitely many elements of A, it follows that X x Y is covered by finitely elements of A. QED

This is all well and good, but isn't the choice axiom used when the sets A1, ..., Am are chosen for each x0, since {A1, ..., Am} is only one possible finite subcollection of A containing x0 x Y? This is not an issue if the space X happens to be finite, since in that case you are making only finitely many choices, but this cannot be assumed in general.

Is there a way to modify the proof to avoid the choice axiom?

 

[micromass]

Choice seems to be used here. Here is an argument that doesn't use choice:

It suffices to prove that every filter \mathcal{F} in XxY has a cluster point. Denote p_X,p_Y the projections on X and Y. Denote \mathcal{V}_X(x) the neighborhood filter of x in the space X (or Y).

The filter \{G\subseteq X~\vert~p_X^{-1}(G)\in \mathcal{F}\} has a cluster point x_0.
Let \mathcal{F}_0 be the filter generated by

\mathcal{F}\cup \{p_X^{-1}(U)~\vert~U\in \mathcal{V}_X(x_0)\}

The filter \{G\subseteq Y~\vert~p_Y^{-1}(G)\in \mathcal{F}_0\} has a cluster point x_1.

Then (x_0,x_1) is a cluster point of \mathcal{F}.

 

[poochie_d]

Hmm... I don't know what filters are... Better go look it up. Anyway, thanks for the quick reply, micromass! *runs off to wikipedia*