The infinite product of connected spaces is connected in the product topology. Is my proof correct? Any general feedback on proof writing style is also much appreciated!
1. Theorem
The infinite product of connected spaces is connected in the product topology. In particular, let $ \{X_\alpha \}_{\alpha \in A}$ be an infinite collection of connected topological spaces. Then
$$ X := \prod_{\alpha \in A} X_\alpha $$
is connected, where $ (X, \tau_X) $ has the product topology.
2. Lemma
Fix $ x \in X $ and define $X_K \subseteq X$ for finite index set $K$ as
$$ X_K := \{ z \in X : \forall i \notin K, z_i = x_i   \} $$
Then  $x \in X_K$ and $ X_K $ is homeomorphic to $ \prod_{k \in K} X_k $.
3. Proof of Lemma
Define $ f : X_K \rightarrow \prod X_k $ as simply removing coordinates not in $K$.
This is clearly surjective. And injective: if $f(u) = 0$, then $u_k = 0$ for each $ k \in K $ (and the coordinates outside of $K$ are fixed).
Next, note that for any open $U \subset X_K$, as subspace of $X$, there exists in $V \in \tau_X$ such that $ U = V \cap X_K $. Thus, each $U_k$ is open in $X_k$ and the remaining coordinates are fixed.
Since any open $ W \subset \prod X_k $ has open $W_k$ in $X_k$, it's immediate that $f$ and $f^{-1}$ map $ U_k \leftrightarrow U_k $. It follows that f is a homeomorphism. $\square$
4. Proof of Theorem
Again fix $ x \in X $. Let $ E := C(x) $, the connected component of $x$ in $X$.
Since E is closed (we will not prove this here), it suffices to show that E is dense.
First note that $\prod X_K$ is connected for any for any finite $K$, since the finite product of connected sets is connected (not proven here). Now we use the Lemma to conclude that $X_K = f^{-1}(\prod X_k)$ is connected (connectedness is a topological property). It follows that $X_K \subseteq E $ for all finite $K$.
It remains to show that $ F:= \bigcup \{ X_K : finite~K \} $ is dense in X. This will follow from a property of the product topology. Also, note that the arbitrary union of connected sets is connected (not shown here), so $F \subseteq E$.
We will show that all points of $X$ are adherent to $X_K$ for some finite $K$ and then be done. Fix $y \in X$ and a y-neighborhood $U \in \tau_X$. From the product topology, we have
$ U = \prod U_\alpha $ with $U_\alpha \ne X_\alpha $ only finitely often with $ U_\alpha$ open in $X_\alpha$.
Then let $I$ be the finite set of indices where $U_\alpha \ne X_\alpha$.
Then we can choose a $z \in X_K$ with $K = I$ and $ z_k = k_k $ for each $ k \in K$.
It follows that $z \in U$ and all points of $X$ are adherent to $F \subseteq E$. $\square$
5. Related posts.
This post does not provide a complete proof but is relevant.
I think this post provides a complete proof. Thanks @Henno Brandsma.
6. Updates
Thanks to @diracdeltafunk and @Henno Brandsma for pointing out errors/confusing conventions in my original proof.
I think this version (2022/2/12 at 12:30 ET) fixes those issues, so I'll treat this as an answer unless someone raises another issue.
 A: I'm submitting a finalized version of my original proof as a proposed answer.
1. Theorem
The infinite product of connected spaces is connected in the product topology. In particular, let $ \{X_\alpha \}_{\alpha \in A}$ be an infinite collection of connected topological spaces. Then
$$ X := \prod_{\alpha \in A} X_\alpha $$
is connected, where $ (X, \tau_X) $ has the product topology.
2. Lemma
Fix $ x \in X $ and define $X_K \subseteq X$ for finite index set $K$ as
$$ X_K := \{ z \in X : \forall i \notin K, z_i = x_i   \} $$
Then  $x \in X_K$ and $ X_K $ is homeomorphic to $ \prod_{k \in K} X_k $.
3. Proof of Lemma
Define $ f : X_K \rightarrow \prod X_k $ as simply removing coordinates not in $K$.
This is clearly surjective. And injective: if $f(u) = 0$, then $u_k = 0$ for each $ k \in K $ (and the coordinates outside of $K$ are fixed).
Next, note that for any open $U \subset X_K$, as subspace of $X$, there exists in $V \in \tau_X$ such that $ U = V \cap X_K $. Thus, each $U_k$ is open in $X_k$ and the remaining coordinates are fixed.
Since any open $ W \subset \prod X_k $ has open $W_k$ in $X_k$, it's immediate that $f$ and $f^{-1}$ map $ U_k \leftrightarrow U_k $. It follows that f is a homeomorphism. $\square$
4. Proof of Theorem
Again fix $ x \in X $. Let $ E := C(x) $, the connected component of $x$ in $X$.
Since E is closed (we will not prove this here), it suffices to show that E is dense.
First note that $\prod X_K$ is connected for any for any finite $K$, since the finite product of connected sets is connected (not proven here). Now we use the Lemma to conclude that $X_K = f^{-1}(\prod X_k)$ is connected (connectedness is a topological property). It follows that $X_K \subseteq E $ for all finite $K$.
It remains to show that $ F:= \bigcup \{ X_K : finite~K \} $ is dense in X. This will follow from a property of the product topology. Also, note that the arbitrary union of connected sets is connected (not shown here), so $F \subseteq E$.
We will show that all points of $X$ are adherent to $X_K$ for some finite $K$ and then be done. Fix $y \in X$ and a y-neighborhood $U \in \tau_X$. From the product topology, we have
$ U = \prod U_\alpha $ with $U_\alpha \ne X_\alpha $ only finitely often with $ U_\alpha$ open in $X_\alpha$.
Then let $I$ be the finite set of indices where $U_\alpha \ne X_\alpha$.
Then we can choose a $z \in X_K$ with $K = I$ and $ z_k = k_k $ for each $ k \in K$.
It follows that $z \in U$ and all points of $X$ are adherent to $F \subseteq E$. $\square$
