Так, мы поняли, что Вам не нравится аксиома выделения. Не хотите - не надо, аналог теоремы Кантора можно даже в простой теории типов доказать.
Множество функций из

в

будем обозначать

. Множество из двух элементов обозначим

, на нем введем функцию

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

Теорема.

мощнее

, то есть не существует функции

такой, что у каждого элемента

есть прообраз

.
Доказательство. От противного. Предположим, что

существует. Рассмотрим функцию

, которая каждому элементу

сопоставляет значение

. Пусть

--- прообраз

, т.е.

. Тогда

, что невозможно, так как для обоих элементов

не выполняется

.
В этом доказательстве Вам какие аксиомы не нравятся? Их тут немного: 1) существование множества

и функции

; 2) метод доказательства от противного; 3) Если

и

, то существует

; 4) Вычисление по формуле (

- абстракция): если

--- переменная типа

и
![$\phi[z]$ $\phi[z]$](https://dxdy-02.korotkov.co.uk/f/1/2/6/126a763bb44c27f7b6d2f83a3b7580ba82.png)
--- формула с этой переменной, то существует функция, сопоставляющая каждому

значение формулы

на этом

;