I'm studying the paper by Michael Hrusak, and Ariet Ramos-Garcia:
Hrusak, M.; Ramos-Garcia, U.A., Malykhin's problem, Adv. Math. 262, 193-212 (2014). ZBL1291.03095.
In this paper they construct model of ZFC such that every countable Fréchet group is metrizable.
I include here the proof of the main theorem (i.e. It is consistent with ZFC that every first countable topological group is metrizable):
[In brief, the idea is to iterate a forcing that introduces a set into each group of uncountable weight (i.e. each non-metrizable group, by Birkhoff-Kakutani) such that the group identity is in its clousure but it contains no sequence converging to it, and have care to have the rest of the iteration preserve this.]
I have studied very few forcing iterations, just some of the basic ones presented in Kunen's Set Theory. So I do not know what this "standard argument" referred to in the second paragraph is. If somebody could point it out to me or guide me to where I can see an explanation of it I'd be very grateful. I'm also confused on why iterating $\omega_2$ times is enough but I imagine this has something to do with it.
I have two other questions about the proof:
Informally, I interpret the fact that C is a club as: "during the iteration, we had a lot (a club many) of opportunities to consider this group." Why does it follow from this that at some stage in the iteration we did in fact consider the group?
Why is every sequence $\tau_\alpha$-converging to 0, also $\tau$-converging? $(\tau_\alpha=\tau \cap V[G_\alpha]).$
Earlier in the text the authors state:
"The information about the future group topologies extending our topology τ, includes information about convergent sequences: If C converges to 1G in τ it will also converge in all future topologies."
But without much further comment.