[proofplan]
We use the characterisation of compactness via the finite intersection property (FIP): a topological space is compact if and only if every family of closed subsets with the FIP has non-empty intersection. Given a family $\mathcal{C}$ of closed subsets of $X$ with the FIP, we apply Zorn's lemma to enlarge $\mathcal{C}$ to a maximal family $\mathcal{F}$ of subsets (not necessarily closed) with the FIP. Maximality forces two structural properties: $\mathcal{F}$ is closed under finite intersections, and any set meeting every member of $\mathcal{F}$ already lies in $\mathcal{F}$. For each coordinate $\gamma \in \Gamma$, the projected family $\{\overline{\pi_\gamma(A)} : A \in \mathcal{F}\}$ has the FIP in the compact space $X_\gamma$, so we can pick $x_\gamma$ in its intersection. The candidate point $x = (x_\gamma)_\gamma$ then lies in $\overline{A}$ for every $A \in \mathcal{F}$ — using the structural properties of $\mathcal{F}$ to pass from a coordinatewise statement to a joint statement on cylinder neighbourhoods — and in particular $x$ lies in $\bigcap_{C \in \mathcal{C}} C$.
[/proofplan]
[step:Reduce to showing the FIP characterisation: every family of closed sets with the FIP has non-empty intersection]
Recall the **finite intersection property (FIP) characterisation of compactness**: a topological space $X$ is compact if and only if every family $\mathcal{C}$ of closed subsets of $X$ with the property
\begin{align*}
C_1 \cap \cdots \cap C_n \neq \varnothing \quad \text{for every finite } C_1, \ldots, C_n \in \mathcal{C}
\end{align*}
satisfies $\bigcap_{C \in \mathcal{C}} C \neq \varnothing$. This is the contrapositive of the open-cover definition: $\mathcal{C}$ has the FIP and empty intersection iff $\{X \setminus C : C \in \mathcal{C}\}$ is an open cover with no finite subcover.
Fix a family $\mathcal{C}$ of closed subsets of $X = \prod_\gamma X_\gamma$ with the FIP. We must produce a point $x \in \bigcap_{C \in \mathcal{C}} C$.
[guided]
The strategy of the proof is to work, not with the closed family $\mathcal{C}$ itself, but with a *maximally enlarged* family $\mathcal{F}$ of subsets of $X$ (not required to be closed) that still has the FIP and contains $\mathcal{C}$. The maximal family is rich enough to allow coordinatewise reasoning: each projection $\pi_\gamma(\mathcal{F}) := \{\pi_\gamma(A) : A \in \mathcal{F}\}$ inherits the FIP, so by compactness of $X_\gamma$ we can pick a coordinate witness $x_\gamma$ in $\bigcap_{A \in \mathcal{F}} \overline{\pi_\gamma(A)}$. The candidate $x = (x_\gamma)_\gamma$ then needs to be shown to lie in $\overline{A}$ for every $A \in \mathcal{F}$, which we do using two structural properties of $\mathcal{F}$ that follow from maximality.
The FIP characterisation is the contrapositive of the open-cover definition of compactness: $\mathcal{C}$ has the FIP and empty intersection if and only if the open cover $\{X \setminus C : C \in \mathcal{C}\}$ admits no finite subcover. Thus showing compactness via FIP is equivalent to showing it via open covers; we choose FIP because closed-set arguments compose cleanly with closures of projections.
Fix a family $\mathcal{C}$ of closed subsets of $X = \prod_\gamma X_\gamma$ with the FIP. Our goal is to produce $x \in \bigcap_{C \in \mathcal{C}} C$.
[/guided]
[/step]
[step:Enlarge $\mathcal{C}$ to a maximal family $\mathcal{F}$ of subsets with the FIP via Zorn's lemma]
Let
\begin{align*}
\mathcal{Z} := \{\mathcal{H} \subseteq \mathcal{P}(X) : \mathcal{C} \subseteq \mathcal{H} \text{ and } \mathcal{H} \text{ has the FIP}\},
\end{align*}
ordered by inclusion. Note that members of $\mathcal{H}$ need not be closed. The set $\mathcal{Z}$ is non-empty because $\mathcal{C} \in \mathcal{Z}$.
We verify the chain condition for Zorn's lemma. Let $(\mathcal{H}_\alpha)_{\alpha \in A}$ be a totally ordered chain in $\mathcal{Z}$, and set $\mathcal{H} := \bigcup_\alpha \mathcal{H}_\alpha$. Then $\mathcal{C} \subseteq \mathcal{H}$, and given any finite $H_1, \ldots, H_n \in \mathcal{H}$, by the chain property there exists a single $\alpha$ with $H_1, \ldots, H_n \in \mathcal{H}_\alpha$; the FIP of $\mathcal{H}_\alpha$ then gives $H_1 \cap \cdots \cap H_n \neq \varnothing$. So $\mathcal{H} \in \mathcal{Z}$, and $\mathcal{H}$ is an upper bound for the chain.
By Zorn's lemma, $\mathcal{Z}$ has a maximal element $\mathcal{F}$, so $\mathcal{C} \subseteq \mathcal{F}$, $\mathcal{F}$ has the FIP, and any strict superset of $\mathcal{F}$ in $\mathcal{P}(X)$ fails the FIP.
[/step]
[step:Derive structural properties of $\mathcal{F}$ from maximality]
We establish two properties of $\mathcal{F}$.
**Property (i): $\mathcal{F}$ is closed under finite intersections.** Let $A, B \in \mathcal{F}$. Set $\mathcal{F}' := \mathcal{F} \cup \{A \cap B\}$. We claim $\mathcal{F}'$ has the FIP. Given a finite collection $H_1, \ldots, H_n \in \mathcal{F}'$, group them: those equal to $A \cap B$ contribute $A$ and $B$ separately to a finite collection in $\mathcal{F}$, and the rest are already in $\mathcal{F}$. Concretely, the intersection $H_1 \cap \cdots \cap H_n$ equals an intersection of finitely many members of $\mathcal{F}$ (replacing each appearance of $A \cap B$ by the two factors $A, B$), which is non-empty by the FIP of $\mathcal{F}$. Hence $\mathcal{F}' \in \mathcal{Z}$, so by maximality $\mathcal{F}' = \mathcal{F}$, i.e. $A \cap B \in \mathcal{F}$.
**Property (ii): If $A \subseteq X$ satisfies $A \cap B \neq \varnothing$ for every $B \in \mathcal{F}$, then $A \in \mathcal{F}$.** Set $\mathcal{F}' := \mathcal{F} \cup \{A\}$. To show $\mathcal{F}' \in \mathcal{Z}$, fix a finite collection $H_1, \ldots, H_n \in \mathcal{F}'$. If none equals $A$, the FIP of $\mathcal{F}$ gives non-emptiness. If some $H_i = A$, list the remaining $H_j \in \mathcal{F}$; by Property (i), $B := \bigcap_{j \neq i} H_j \in \mathcal{F}$ (using induction over finitely many factors), so by hypothesis $A \cap B \neq \varnothing$, i.e. $H_1 \cap \cdots \cap H_n = A \cap B \neq \varnothing$. So $\mathcal{F}'$ has the FIP, hence $\mathcal{F}' \in \mathcal{Z}$, and by maximality $\mathcal{F}' = \mathcal{F}$, i.e. $A \in \mathcal{F}$.
[/step]
[step:For each coordinate $\gamma$, choose $x_\gamma \in \bigcap_{A \in \mathcal{F}} \overline{\pi_\gamma(A)}$ using compactness of $X_\gamma$]
Fix $\gamma \in \Gamma$ and consider the family
\begin{align*}
\mathcal{G}_\gamma := \{\overline{\pi_\gamma(A)} : A \in \mathcal{F}\}
\end{align*}
of closed subsets of $X_\gamma$. We verify the FIP. Given $A_1, \ldots, A_n \in \mathcal{F}$, the FIP of $\mathcal{F}$ gives a point $z \in A_1 \cap \cdots \cap A_n$, and then $\pi_\gamma(z) \in \pi_\gamma(A_i) \subseteq \overline{\pi_\gamma(A_i)}$ for each $i$, so $\overline{\pi_\gamma(A_1)} \cap \cdots \cap \overline{\pi_\gamma(A_n)} \neq \varnothing$.
Since $X_\gamma$ is compact and $\mathcal{G}_\gamma$ is a family of closed subsets with the FIP, the FIP characterisation of compactness gives
\begin{align*}
\bigcap_{A \in \mathcal{F}} \overline{\pi_\gamma(A)} \neq \varnothing.
\end{align*}
Pick $x_\gamma \in \bigcap_{A \in \mathcal{F}} \overline{\pi_\gamma(A)}$. (We use the axiom of choice to do this simultaneously for all $\gamma$.)
Set $x := (x_\gamma)_{\gamma \in \Gamma} \in X$.
[/step]
[step:Show that every basic open neighbourhood of $x$ in $X$ meets every $A \in \mathcal{F}$]
A basic open neighbourhood of $x$ in the product topology has the form
\begin{align*}
V = \pi_{\gamma_1}^{-1}(U_1) \cap \cdots \cap \pi_{\gamma_n}^{-1}(U_n),
\end{align*}
where $\gamma_1, \ldots, \gamma_n \in \Gamma$ are distinct and each $U_i \subseteq X_{\gamma_i}$ is open with $x_{\gamma_i} \in U_i$.
Fix such a $V$ and fix $A \in \mathcal{F}$. We show $V \cap A \neq \varnothing$.
For each $i$, since $x_{\gamma_i} \in U_i$ and $x_{\gamma_i} \in \overline{\pi_{\gamma_i}(B)}$ for every $B \in \mathcal{F}$ (by Step 4), the open set $U_i$ meets $\pi_{\gamma_i}(B)$ for every $B \in \mathcal{F}$. Equivalently, for every $B \in \mathcal{F}$, the set $\pi_{\gamma_i}^{-1}(U_i) \cap B$ is non-empty (any preimage of a point in $U_i \cap \pi_{\gamma_i}(B)$ provides a witness).
By Property (ii) of Step 3, applied to the set $A_i := \pi_{\gamma_i}^{-1}(U_i)$, we conclude $\pi_{\gamma_i}^{-1}(U_i) \in \mathcal{F}$ for each $i = 1, \ldots, n$.
By Property (i) of Step 3 (applied $n-1$ times), $V = \pi_{\gamma_1}^{-1}(U_1) \cap \cdots \cap \pi_{\gamma_n}^{-1}(U_n) \in \mathcal{F}$. The FIP of $\mathcal{F}$ applied to the pair $V, A \in \mathcal{F}$ now gives $V \cap A \neq \varnothing$, as claimed.
[guided]
A basic open neighbourhood of $x$ in the product topology has the form
\begin{align*}
V = \pi_{\gamma_1}^{-1}(U_1) \cap \cdots \cap \pi_{\gamma_n}^{-1}(U_n),
\end{align*}
where $\gamma_1, \ldots, \gamma_n \in \Gamma$ are distinct indices and $U_i \subseteq X_{\gamma_i}$ are open sets containing $x_{\gamma_i}$. The product topology is generated by such cylinder sets — finite-dimensional restrictions on the coordinates — so the basic open neighbourhoods of $x$ are precisely the sets of this form.
Fix such a $V$ and fix $A \in \mathcal{F}$. We must show $V \cap A \neq \varnothing$. The argument proceeds in three sub-steps.
*Sub-step (a): each cylinder $\pi_{\gamma_i}^{-1}(U_i)$ meets every $B \in \mathcal{F}$.* For each $i \in \{1, \ldots, n\}$, the witness $x_{\gamma_i}$ chosen in Step 4 lies in $\overline{\pi_{\gamma_i}(B)}$ for every $B \in \mathcal{F}$. Since $U_i$ is an open neighbourhood of $x_{\gamma_i}$, the closure characterisation of contact points gives $U_i \cap \pi_{\gamma_i}(B) \neq \varnothing$ for every $B \in \mathcal{F}$. Pick any $y \in U_i \cap \pi_{\gamma_i}(B)$ and any $z \in B$ with $\pi_{\gamma_i}(z) = y$; then $z \in \pi_{\gamma_i}^{-1}(U_i) \cap B$, witnessing
\begin{align*}
\pi_{\gamma_i}^{-1}(U_i) \cap B \neq \varnothing \quad \text{for every } B \in \mathcal{F}.
\end{align*}
*Sub-step (b): each $\pi_{\gamma_i}^{-1}(U_i)$ lies in $\mathcal{F}$.* The condition just established is precisely the hypothesis of Property (ii) (Step 3) applied to $A_i := \pi_{\gamma_i}^{-1}(U_i)$. Therefore $\pi_{\gamma_i}^{-1}(U_i) \in \mathcal{F}$ for each $i = 1, \ldots, n$.
Why does this matter? It is the place where the maximality of $\mathcal{F}$ does real work. The cylinders are not in $\mathcal{C}$ a priori, but maximality forces them into $\mathcal{F}$ once they meet everything in $\mathcal{F}$. This is what allows the *coordinatewise* witnesses $x_\gamma$ to be assembled into a *joint* witness in $X$.
*Sub-step (c): $V \in \mathcal{F}$, hence $V \cap A \neq \varnothing$.* By Property (i) of Step 3, $\mathcal{F}$ is closed under finite intersections; iterating gives $V = \pi_{\gamma_1}^{-1}(U_1) \cap \cdots \cap \pi_{\gamma_n}^{-1}(U_n) \in \mathcal{F}$. The FIP of $\mathcal{F}$ applied to the pair $V, A \in \mathcal{F}$ gives $V \cap A \neq \varnothing$.
[/guided]
[/step]
[step:Conclude that $x \in \bigcap_{C \in \mathcal{C}} C$]
Fix $C \in \mathcal{C}$. Since $\mathcal{C} \subseteq \mathcal{F}$, we have $C \in \mathcal{F}$. By Step 5, every basic open neighbourhood $V$ of $x$ satisfies $V \cap C \neq \varnothing$. By the closure characterisation of contact points (a point lies in the closure of a set if and only if every open neighbourhood meets the set), $x \in \overline{C}$. Since $C$ is closed, $\overline{C} = C$, so $x \in C$.
This holds for every $C \in \mathcal{C}$, so $x \in \bigcap_{C \in \mathcal{C}} C$. The arbitrary family $\mathcal{C}$ of closed sets with the FIP therefore has non-empty intersection, which by the FIP characterisation of compactness recalled in Step 1 establishes that $X$ is compact.
[/step]
