Теорема Кантора и аксиома выделения

[alex_dorin]

В доказательстве теоремы Кантора :
"Любое множество менее мощно, чем множество всех его подмножеств"
используется аксиома выделения. Пожалуйста, покажите в формальной записи
конкретный ее вид, примененный в доказательстве (как я понял , используется не схема аксиом, а одна из них, которая
выразима в первопорядковой логике).

[Xaositect]

Как минимум $\forall x\, \forall f (f \in (\mathcal{P}x)^x \to \exists z\, \forall u (u\in z \leftrightarrow u\notin f(u)))$ (существование множества $\{u\in x| u\notin f(u)\}$)

[alex_dorin]

Что обозначает степень x ?

[Xaositect]

$b^a$ - множество функций из $a$ в $b$

[alex_dorin]

Привожу ссылку в этом форуме -
topic12069.html

... Между тем утверждение о том, что любые два множества сравнимы по мощности, без аксиомы выбора не доказуемо. ...

Где об этом можно прочитать более подробно ?

[Someone]

К. Куратовский, А. Мостовский. Теория множеств. "Мир", Москва, 1970.

Смотрите главу VIII, § 6.

Замечание. В книге излагается теория множеств ZFC с некоторыми отличиями: авторы не включают в число аксиом аксиому регулярности, хотя считают её "интуитивно очевидной", и включают придуманную ими аксиому, которую называют аксиомой реляционных типов.
Кроме того, они тщательно отслеживают применение аксиомы выбора.

[alex_dorin]

Несколько механическим путем с использованием логического прувера я получил доказательство
теоремы Кантора без использования какой-либо формы аксиомы выделения , но с присоединением аксиомы выбора
в мультипликативной форме.
Нет ли здесь ошибки в этом результате на пути к механической математики ?

[Deggial]

alex_dorin в сообщении #961834 писал(а):

Привожу ссылку в этом форуме - topic12069.html

... Между тем утверждение о том, что любые два множества сравнимы по мощности, без аксиомы выбора не доказуемо. ...

alex_dorin, замечание за неправильное оформление цитат.