Так, мы поняли, что Вам не нравится аксиома выделения. Не хотите - не надо, аналог теоремы Кантора можно даже в простой теории типов доказать.
Множество функций из
в
будем обозначать
. Множество из двух элементов обозначим
, на нем введем функцию
, которая элементы переставляет. Вместо подмножеств будем рассматривать их характеристические функции, т.е. элементы
Теорема.
мощнее
, то есть не существует функции
такой, что у каждого элемента
есть прообраз
.
Доказательство. От противного. Предположим, что
существует. Рассмотрим функцию
, которая каждому элементу
сопоставляет значение
. Пусть
--- прообраз
, т.е.
. Тогда
, что невозможно, так как для обоих элементов
не выполняется
.
В этом доказательстве Вам какие аксиомы не нравятся? Их тут немного: 1) существование множества
и функции
; 2) метод доказательства от противного; 3) Если
и
, то существует
; 4) Вычисление по формуле (
- абстракция): если
--- переменная типа
и
--- формула с этой переменной, то существует функция, сопоставляющая каждому
значение формулы
на этом
;