Не понял, зачем выбирать? Насколько я понимаю, у нас уже есть (по условию) счётное множество счётных множеств. В моей терминологии это - последовательность последовательностей.
Извините, но есть стандартная терминология, давайте её и придерживаться. Вы здесь сами себя этой своей терминологией и запутали.
Если говорят, что задана последовательность элементов множества

, то это означает, что
задано некоторое отображение

. Когда говорят, что эта последовательность есть нумерация элементов

, имеют в виду, что

взаимно однозначно отображает

на

.
Если говорят, что задано счётное множество

, то это означает, что существует хотя бы одна нумерация элементов

, но никакая конкретная нумерация
не задана. Вам, как стороннику конструктивизма, должна быть понятна разница между этими двумя ситуациями.
Теперь, если у нас есть одно счётное множество, в классической математике мы можем сказать, что, поскольку

счётно, существует нумерация его элементов

, и далее работать с этим

, никак его не конкретизируя. (В конструктивной математике мы обязаны определить это

явно любым конструктивным способом.) Если у нас есть конечное семейство счётных множеств, то мы можем повторить эту фразу соответствующее число раз. Если же у нас семейство множеств бесконечное, то мы лишаемся этой возможности. Бесконечно длинные рассуждения классическая математика не признаёт и не использует.
Если Вы заглянете в книжку "Теория множеств" К.Куратовского и А.Мостовского, то обнаружите там две теоремы: "Вашу" теорему о счётности множества элементов последовательности последовательностей, которая доказывается без аксиомы выбора, и теорему о счётности объединения счётного множества счётных множеств, доказательство которой требует аксиомы выбора. Роль аксиомы выбора здесь состоит как раз в том, что она позволяет заменить
бесконечную совокупность произвольных выборов
одним произвольным выбором.
Но ведь при использовании диагональной процедуры нумерации мы и будем на каждом шаге иметь дело с конечным семейством множеств.
Ну, Вы имеете в виду стандартно используемую в математических рассуждениях неформальную "индуктивную" процедуру построения, когда на каждом шаге выбирается очередной произвольный элемент из очередного множества. Это построение в буквальном виде не формализуемо. Более того, нет никакой аксиомы, на основании которой можно было бы утверждать, что совокупность выбранных таким образом элементов будет множеством. Интуитивно я уверен, что такая аксиома была бы много сильнее аксиомы выбора. Использование аксиомы выбора позволяет преобразовать эту "индуктивную" процедуру в настоящую схему определения по индукции, доказуемую в ZF: до начала построения мы выбираем одну функцию выбора, а затем, когда нам в очередном шаге нужно "выбрать" очередной элемент, ссылаемся на эту функцию выбора. Подробности схем определений по индукции (в том числе - трансфинитной), доказуемых в ZF, можно посмотреть в упомянутой выше книге.