Существование базиса в любом ВП

[EminentVictorians]

mihaild в сообщении #1529527 писал(а):

А у вас нет совокупности множеств. У вас есть по множеству для каждого $n$, а общее, содержащее их все, без аксиомы выбора существовать не обязано.

Пусть есть множества $X_i$ индексированные множеством $I$ (т.е. $i \in I$). Получается, что взять объединение $\bigcup\limits_{i \in I}^{}X_i$ без аксиомы выбора нельзя. А если есть совокупность множеств $\{X_i\}$, индексированных множеством $I$, то $\bigcup\limits_{i \in I}^{}X_i$ взять можно без аксиомы выбора, так что ли?

[mihaild]

EminentVictorians в сообщении #1529534 писал(а):

Пусть есть множества $X_i$ индексированные множеством $I$ (т.е. $i \in I$).

Вот нужно уточнять, что это в точности значит. Вы доказали, что $\forall i \in I \exists X: P(i, X)$. Чтобы из этого построить функцию $f$ такую что $\forall i: P(f(i))$, нужна аксиома выбора. Ну и дальше можно будет уже взять объединение $\bigcup_i f(i)$.

[Nemiroff]

EminentVictorians в сообщении #1529523 писал(а):

Потом просто возьмем объединение этих подпространств и все.

И что всё? Ну взяли вы объединение.

[Someone]

EminentVictorians в сообщении #1529534 писал(а):

Пусть есть множества $X_i$ индексированные множеством $I$ (т.е. $i \in I$).

Если $I$ бесконечное, то у Вас такого семейства нет.
Давайте посмотрим внимательнее. Пусть у нас есть некоторая формализованная теория $T$ (пусть это будет теория множеств ZF без аксиомы выбора, поскольку мы рассуждаем о множествах).
Допустим, у нас есть некоторое бесконечномерное линейное пространство $L$.
Сначала у нас пустое множество векторов, и его линейная оболочка $V_0=\{\mathbf 0\}$ содержит только нулевой вектор.
Далее, поскольку L бесконечномерно, то базиса пока нет, и мы выбираем некоторый вектор $\mathbf x_1\in L\setminus V_0$ и строим линейную оболочку $V_1$ множества $\{\mathbf x_1\}$. Система векторов $\{\mathbf x_1\}$ линейно независима.
Далее, поскольку L бесконечномерно, то базиса пока нет, и мы выбираем некоторый вектор $\mathbf x_2\in L\setminus V_1$ и строим линейную оболочку $V_2$ множества $\{\mathbf x_1,\mathbf x_2\}$. Система векторов $\{\mathbf x_1,\mathbf x_2\}$ линейно независима.
…
…
…
Наконец, поскольку L бесконечномерно, то базиса после построения $\{\mathbf x_1,\mathbf x_2,\ldots,\mathbf x_{n-1}\}$ нет, и мы выбираем некоторый вектор $\mathbf x_2\in L\setminus V_{n-1}$ и строим линейную оболочку $V_n$ множества $\{\mathbf x_1,\mathbf x_2,\ldots,\mathbf x_{n-1},\mathbf x_n\}$.Система векторов $\{\mathbf x_1,\mathbf x_2,\ldots,\mathbf x_{n-1},\mathbf x_n\}$ линейно независима.
Формализовать в ZF это рассуждение с многоточиями нельзя, его надо добросовестно выписать полностью, ничего не пропуская и не заменяя повторяющиеся рассуждения многоточиями. В результате получится доказательство существования $n$ линейно независимых векторов для конкретного натурального числа $n$.
Далее Вы ссылаетесь на то, что это рассуждение можно проделать для любого натурального $n$ (позаботившись при этом, чтобы эти множества линейно независимых векторов образовывали растущую цепочку множеств), и поэтому у Вас якобы есть бесконечная цепочка множеств. Однако формулы и доказательства теории $T$ не являются её объектами (теория ZF говорит о множествах, а не о формулах и не о доказательствах), и в её языке нет средств для формализации этого рассуждения. Они могут существовать в метатеории, но тогда мы получаем метатеорему, а не теорему ZF. Эта метатеорема плоха тем, что совокупность $\{\mathbf x_n:n\in\mathbb N\setminus\{0\}\}$, которую Вы хотите получить, может быть множеством в метатеории, но не быть множеством в ZF.