Theorem: Tychonoff's Theorem

Let $I$ be an indexing set.
Let $\family {X_i}_{i \mathop \in I}$ be an indexed family of non-empty topological spaces.
Let $\ds X = \prod_{i \mathop \in I} X_i$ be the corresponding product space.
Then $X$ is compact {{iff}} each $X_i$ is compact.

Proof:
First assume that $X$ is compact. 
From Projection from Product Topology is Continuous, the projections $\pr_i : X \to X_i$ are continuous.
It follows from Continuous Image of Compact Space is Compact that the $X_i$ are compact.
Assume now that each $X_i$ is compact.
By Compact Space satisfies Finite Intersection Axiom, it suffices to show that: 
:for each family $\CC$ of closed subsets of $X$ with: 
::$\ds \bigcap_{C \mathop \in \CC} C = \O$ 
:there exists a finite subset $\SS \subseteq \CC$ such that: 
::$\ds \bigcap_{G \mathop \in \SS} G = \O$
We show the contrapositive.
That is, let $\CC$ be a family of closed subsets of $X$ such that:
:$\ds \bigcap_{G \mathop \in \SS} G \ne \O$
for all finite subsets $\SS \subseteq \CC$.
{{Recall|Finite Intersection Property|the finite intersection property}}
{{:Definition:Finite Intersection Property}}
We aim to show that: 
:$\ds \bigcap_{C \mathop \in \CC} C \ne \O$
Let: 
:$S = \leftset {\CC \subseteq \AA : \AA}$ has the finite intersection property$\rightset {}$
=== Lemma 1 ===
{{:Tychonoff's Theorem/Lemma 1}}{{qed|lemma}}
It will now suffice to show that: 
:$\ds \bigcap_{A \mathop \in \AA} \map \cl A \ne \O$ 
where $\map \cl A$ denotes the closure of $A$.
=== Lemma 2 ===
{{:Tychonoff's Theorem/Lemma 2}}{{qed|lemma}}
=== Lemma 3 ===
{{:Tychonoff's Theorem/Lemma 3}}{{qed|lemma}}
We now show that: 
:$\set {\map \cl { {\pr_i} \sqbrk A} : A \in \AA}$
has the finite intersection property for each $i \in I$, with $\map \cl {\map {\pr_i} A}$ being the closure taken in $X_i$. 
Fix $i \in I$. 
Pick a finite set:
:$\set { {\pr_i} \sqbrk {A_1}, \ldots, {\pr_i} \sqbrk {A_n} } \subseteq \set { {\pr_i} \sqbrk A : A \in \AA}$
with $A_j \in \AA$ for each $1 \le j \le n$.
Since $\AA$ has the finite intersection property, we have: 
:$\ds \bigcap_{j \mathop = 1}^n A_j \ne \O$
so that: 
:$\ds {\pr_i} \sqbrk {\bigcap_{j \mathop = 1}^n A_j} \ne \O$
From Image of Intersection under Mapping: General Result, we have:
:$\ds \O \ne {\pr_i} \sqbrk {\bigcap_{j \mathop = 1}^n A_j} \subseteq \bigcap_{j \mathop = 1}^n {\pr_i} \sqbrk {A_j}$
and in particular:
:$\ds \bigcap_{j \mathop = 1}^n {\pr_i} \sqbrk {A_j} \ne \O$
From Closure of Intersection is Subset of Intersection of Closures, we then have: 
:$\ds \O \ne \map \cl {\bigcap_{j \mathop = 1}^n {\pr_i} \sqbrk {A_j} } \subseteq \bigcap_{j \mathop = 1}^n \map \cl { {\pr_i} \sqbrk {A_j} }$ 
in particular:
:$\ds \bigcap_{j \mathop = 1}^n \map \cl { {\pr_i} \sqbrk {A_j} } \ne \O$ 
So:
:$\set {\map \cl { {\pr_i} \sqbrk A} : A \in \AA}$ has the finite intersection property.
Since $X_i$ is compact {{hypothesis}}, we have: 
:$\ds \bigcap_{A \mathop \in \AA} \map \cl { {\pr_i} \sqbrk A} \ne \O$
for each $i \in I$, using Compact Space satisfies Finite Intersection Axiom.
Now pick:
:$\ds x_i \in \bigcap_{A \mathop \in \AA} \map \cl { {\pr_i} \sqbrk A}$
for each $i \in I$. 
Let $x = \family {x_i}_{i \mathop \in I}$.
We will show that: 
:$\ds x \in \bigcap_{A \mathop \in \AA} \map \cl A$
We will then have: 
:$\ds \bigcap_{A \mathop \in \AA} \map \cl A \ne \O$
and in particular:
:$\ds \bigcap_{C \mathop \in \CC} C \ne \O$
In order to show: 
:$x \in \map \cl A$ for each $A \in \AA$
by Condition for Point being in Closure, we can show that for each open neighborhood $V$ of $x$ in $X$, we have: 
:$V \cap A \ne \O$
Let $V$ be an open neighborhood of $x$ in $X$. 
First, suppose that there exists $\delta_1, \ldots, \delta_n \in I$ and open neighborhoods $U_i \in \tau_{\delta_i}$ of $x_i$ such that: 
:$\ds V = \bigcap_{i \mathop = 1}^n \pr_i^{-1} \sqbrk {U_i}$
Recall that $x$ was constructed so that we have, for each $1 \le i \le n$: 
:$\ds x_{\delta_i} \in \bigcap_{A \mathop \in \AA} \map \cl {\pr_{\delta_i} \sqbrk A}$
so that, by Condition for Point being in Closure:
:$U_i \cap \pr_{\delta_i} \sqbrk A \ne \O$
for each $1 \le i \le n$. 
Then there exists $v \in U_i \cap \pr_{\delta_i} \sqbrk A$.
That is, there exists $u \in A$ such that $\map {\pr_{\delta_i} } u = v \in U_i$.
So we have: 
:$u \in A \cap \pr_{\delta_i}^{-1} \sqbrk {U_i}$ 
so that: 
:$A \cap \pr_{\delta_i}^{-1} \sqbrk {U_i} \ne \O$ 
for each $A \in \AA$ and $1 \le i \le n$.
So by {{Lemma|Tychonoff's Theorem|3}}, we have $\pr_{\delta_i}^{-1} \sqbrk {U_i} \in \AA$ for each $1 \le i \le n$. 
Then, by {{Lemma|Tychonoff's Theorem|2}}, we have: 
:$\ds V = \bigcap_{i \mathop = 1}^n \pr_{\delta_i}^{-1} \sqbrk {U_i} \in \AA$
So $V$ has the finite intersection property and: 
:$V \cap A \ne \O$ for each $A \in \AA$. 
Now take a general open neighborhood of $x$ in $X$.
Then there exists an indexing set $J$, $n_j \in \N$, $i_{j, 1}, \ldots, i_{j, n_j} \in I$ and $U_k \in \tau_{i_{j, k} }$ for each $1 \le k \le n$ such that: 
:$\ds V = \bigcup_{j \mathop \in J} \bigcap_{k \mathop = 1}^{n_j} \pr_{i_{j, k} }^{-1} \sqbrk {U_k}$
Then, for each $A \in \AA$, we have: 
:$\ds V \cap A = \bigcup_{j \mathop \in J} \paren {A \cap \bigcap_{k \mathop = 1}^{n_j} \pr_{i_{j, k} }^{-1} \sqbrk {U_k} }$
by Intersection Distributes over Union.
By what we have already shown, we have that: 
:$\ds A \cap \bigcap_{k \mathop = 1}^{n_j} \pr_{i_{j, k} }^{-1} \sqbrk {U_k} \ne \O$ 
for each $1 \le k \le n$, and so $V \cap A \ne \O$. 
So we have $x \in \map \cl A$ for each $A \in \AA$, and hence: 
:$\ds x \in \bigcap_{A \mathop \in \AA} \map \cl A$
Now note that since $\CC \subseteq \AA$, we have: 
:$\ds \bigcap_{A \mathop \in \AA} \map \cl A \subseteq \bigcap_{C \mathop \in \CC} \map \cl C$ 
From Set is Closed iff Equals Topological Closure, we have: 
:$\map \cl C = C$ for each $C \in \CC$
and hence: 
:$\ds \bigcap_{A \mathop \in \AA} \map \cl A \subseteq \bigcap_{C \mathop \in \CC} C$ 
We hence obtain: 
:$\ds x \in \bigcap_{C \mathop \in \CC} C$ 
so that: 
:$\ds \bigcap_{C \mathop \in \CC} C \ne \O$
and the proof is complete.
{{qed}}