Nit: the explanation of Cantor's diagonal argument is incorrect. The actual proof starts by assuming for contradiction that all of the reals can be enumerated.
Your version only shows that rationals are a strict subset of the reals, which is much weaker than showing that the cardinality of the rationals is less than the cardinality of the reals (by analogy, imagine the Natural numbers and the Natural numbers plus {0}. These have the same cardinality by the map x |-> x-1, but one strictly contains the other)
Ha! I thought I was the only one. Mine proceeds to think "f is a function mapping from A to B" which I guess might work alright because [everything is a function](https://arxiv.org/pdf/1612.09375)
Nit: the explanation of Cantor's diagonal argument is incorrect. The actual proof starts by assuming for contradiction that all of the reals can be enumerated.
Your version only shows that rationals are a strict subset of the reals, which is much weaker than showing that the cardinality of the rationals is less than the cardinality of the reals (by analogy, imagine the Natural numbers and the Natural numbers plus {0}. These have the same cardinality by the map x |-> x-1, but one strictly contains the other)