Tychonoff theorem (1/2) I was trying to prove Tychonoff theorem. First I used (which I showed also):

The following are equivalent
(a) $X$ is compact
(b) every filter of closed set $F$ on $X$ has non-empty intersection
(c) every ultrafilter of closed set $F$ on  $X$  has non-empty
  intersection

Then my proof is this:
Let $F$ be a filter of closed sets on $X$. Then $\bigcap F \neq \varnothing$:
Define $F_i = \{ Y \subseteq X_i \mid \pi^{-1}_i Y \in F \}$. Inverse maps preserve intersections and subsets and $\pi_i$ are continuous then $F_i$ is a filter of closed sets in $X_i$ and hence has non-empty intersection. Let $x_i \in \bigcap F_i$ and let $x = (x_i)_{i \in I}$. Then $x \in \bigcap F$: By contradiction assume $x \in (\bigcap F)^c = \bigcup F^c$. Then there is $S \in F^c$ with $x \in S$. Then $\pi_i x = x_i \in \pi_i S \subseteq X_i$ for all $i$. By how $S$ was chosen, $\pi_i S \notin F_i$. To see this, assume $\pi_i S \in F_i$. Then $\pi_i^{-1} \pi S \subseteq S \in F^c$. It means $\pi_i^{-1} \pi S$ is a subset of a complement of a set in $F$ and can therefore not be in $F$. But then $x_i \notin f$ for all $f \in F_i$ which is a contradiction to how $x$ was defined.
Is this valid proof? Many thank you for help.
 A: The proof as it stands does not work. Your definition of $\mathcal{F}_i$ for the filter $\mathcal{F}$ (slightly different notation, I prefer script letters for families of subsets) is fine, but your proof of how $x$ must be in $\cap \mathcal{F}$ does not work. 
If $x$ is not in the intersection of all members of $\mathcal{F}$ we know there is some member $F_0$ of $\mathcal{F}$ such that $x \notin F_0$, so $x \in X \setminus F_0$, the latter set you call $S$.
So for all $i$, $x_i \in \pi_i[X \setminus F_0]$. But then $x_i$ could also be in $\pi_i[F_0]$, as projections are not injections (far from it) we cannot say $\pi^{-1}\pi[S] \subset S$, this only works for injective functions $\pi$. So in that step the proof breaks down.
The usual proof for Tychonoff's theorem does not use ultrafilters of closed sets, but just ultrafilters on the powerset, and very extensive write-up (with all preliminaries) is at Yuan's blog. It uses the convenience that when we have ultrafilters, their images (the set of images of members of the ultrafilter) is itself an ultrafilter, and uses the limits in the coordinate spaces.
Engelking's proof (theorem 3.2.4 in my edition) starts with a family of closed sets with fip and starts by extending it to a maximal one. In other words, he takes an ultrafilter as well, and we could see it as one in the lattice of closed sets. He then goes on to show that for a fixed $i$, $\left\{ \overline{\pi_i[F]} : F \in \mathcal{F} \right\}$, when $\mathcal{F}$ is such an ultrafilter, is a family of closed sets in $X_i$ that has the finite intersection property and so has a point in the intersection. This approach would also work in your set-up, I think. 
Added in response to comments 
Actually, what Engelking does is a bit more clever: he goes outside the realm of ultrafilters on closed sets. He starts with a family of closed sets $\mathcal{C}$ of $X$ with the finite intersection property (FIP), and he extends it to a family $\mathcal{F}$ of arbitrary subsets of $X$ (that contains $\mathcal{C}$) and is maximal with respect to inclusion, using your favourite maximum principle (Tukey's lemma or Zorn's lemma). This is of course just the ultrafilter on $X$ generated by $\mathcal{C}$, although he doesn't call it that. He does mention 2 key facts that follow from the maximality: 
(1) $\mathcal{F}$ is closed under finite intersections (we can add all finite intersections of members of $\mathcal{F}$ and cannot get a larger set).
(2) If a set $A$ intersects all members of $\mathcal{F}$, then $A \in \mathcal{F}$. (Same argument, as we can add $A$ to $\mathcal{F}$ and still have a family with FIP, so by maximality, $A \in \mathcal{F}$.)
Now he defines the forward images $\mathcal{F}_i = \{\overline{\pi_i[F]}: F \in \mathcal{F} \}$, and these families have the FIP and consist of closed sets, so by  compactness of each $X_i$ we have a point $x_i \in \cap \mathcal{F}_i$. 
Now we use that we constructed $\mathcal{F}$ to have arbitrary members: the claim is that for any open set $O \subset X_i$ that contains $x_i$, $\pi^{-1}[O] \in \mathcal{F}$. This follows as for any $F \in \mathcal{F}$, $x_i \in \overline{\pi_i[F]}$, so $O \cap \pi_i[F] \neq \emptyset$, which implies that $\pi_i^{-1}[O] \cap F \neq \emptyset$ (any $p \in F$, with $\pi_i(p) \in O$ is a witness to this). So $\pi_i^{-1}[O]$ intersects all member sof $\mathcal{F}$ and so by (2), $\pi_i^{-1}[O] \in \mathcal{F}$.
And as any basic open neighbourhood of $x = (x_i)_{i \in I}$ is of the form $\pi_{i_1}^{-1}[O_{i_1}] \cap \ldots \cap \pi_{i_k}^{-1}[O_{i_k}]$ for some finite $k$, and open sets $O_{i_j} \subset X_{i_j}$ that contain $x_{i_j}$, by (1), all basic neighbourhoods of $x$ are in $\mathcal{F}$, and in particular (!) they have non-empty intersection with all members of the original $\mathcal{C}$. But this says that $x \in \cap \{\overline{C} : C \in \mathcal{C} \} = \cap \mathcal{C}$, as these sets are closed. So a family of closed sets with the FIP in $X$ has non-empty intersection and so $X$ is compact.
I don't quite see yet how this proof will work if we restrict ourselves to consider (ultra)filters of closed sets. We can define the $\mathcal{F}_i$ the same way or we might define them as your $\mathcal{F'}_i = \{ F \subset X_i : F \mbox{ closed }, \pi_i^{-1}[F] \in \mathcal{F} \}$. Again by the FIP we get the $x_i$, for either case, but then how to proceed?
We can start by taking an arbitrary basic neighbourhood $\pi_{i_1}^{-1}[O_{i_1}] \cap \ldots \cap \pi_{i_k}^{-1}[O_{i_k}]$ of $x$, and some fixed $F \in \mathcal{F}$, trying to show te former intersects tha latter, so $x$ is in the closure of all $F$. Using the $\mathcal{F}_i$ I defined above, we get again that $O_{i_j} \cap \pi_{i_j}[F]$ is non-empty and so $\pi_{i_j}^{-1}[O_{i_j}] \cap F$ is non-empty. And we know this separately for every $j$ in $\{1,\ldots k\}$, but it does not give us a point in the basic open set yet! And we cannot use the finite intersections as we did above, as the inverse images of open sets are not in $\mathcal{F}$ when we restrict it to filters on closed sets. So that proof sort of stops here, I think, without getting into further complications. And if we use the $\mathcal{F'}_i$ I don't see an improvement. We start with $F \in \mathcal{F}$, trying to show $x \in \overline{F}$ as before, how do we do that using the $\mathcal{F'}_i$ now? I'm open to suggestions.. 
My conclusion remains that allowing arbitrary sets (so general ultrafilters) leads to a nicer, "flowing" proof, while restricting to ultrafilters of closed sets we run into some technical snags. 
