Текст анонсированного доказательства можно скачать в виде
PDF-файла.
По традиции этот текст дублирован ниже в теле сообщения.
(Опять-таки, ничего нового. Просто доказательство известного факта.
Основная возня связана с обоснованием рекурсивного построения
функции по элементам вполне упорядоченного множества.)
Итак...
Любое вполне упорядоченное множествопорядково изоморфно некоторому ординалуПодробное доказательство в ZFCДля упорядоченного множества

и элемента

условимся
обозначать множество

символом

.
Индукция по элементам вполне упорядоченного множестваДля любой теоретико-множественной формулы 
следующее утверждение является теоремой ZFC.
Если
— произвольное вполне упорядоченное множество
и для любого
из
следует
,
то
для всех
.
Положим
.
Предположим вопреки доказываемому, что
.
Положим
.
Поскольку
, мы имеем
.
Следовательно,
, что противоречит включению
.
Обозначим через

формализацию утверждения
« множество
является функцией с областью определения
».
Для

и

положим
![$f[E]:=\{f(e):e\in E\}$ $f[E]:=\{f(e):e\in E\}$](https://dxdy-02.korotkov.co.uk/f/5/d/b/5dbf635152c0dd9e46a6f5445c2390bb82.png)
.
Всюду ниже

— произвольное вполне упорядоченное множество.
Для

и

будем писать

вместо
![$(\forall\,y\in x{\downarrow})\bigl(\,f(y)=f[y{\downarrow}]\,\bigr)$ $(\forall\,y\in x{\downarrow})\bigl(\,f(y)=f[y{\downarrow}]\,\bigr)$](https://dxdy-02.korotkov.co.uk/f/d/a/f/daf02b02da84b775de2ebb93769829a082.png)
.
Положим

.
Лемма 1.
Если
, то
.Пусть
,
,
и
.
Докажем
индукцией по
.
Пусть
и
. Покажем, что
.
Из
следует
.
Из
следует
.
Из
следует
.
Таким образом, для всякого

имеется единственная функция

,
удовлетворяющая условию

, т.е. такая, что
![$f^x(y)=f^x[y{\downarrow}]$ $f^x(y)=f^x[y{\downarrow}]$](https://dxdy-02.korotkov.co.uk/f/9/e/d/9ed5acb87ea896d9623a355df5f874f482.png)
для всех

.
Лемма 2.
Пусть
и
. Тогда
и
.Как легко видеть, из
вытекает
.
Следовательно,
.
Поскольку
и
, мы имеем
по лемме 1.
Определим функцию

, полагая
(Отметим, что существование такой функции

можно обосновать
с помощью схемы аксиом подстановки.)
Лемма 3.
Пусть
. Тогда
.Покажем, что
.
Пусть
. Покажем, что
.
По лемме 2 мы имеем
и
.
Следовательно,
.
Таким образом,
.
Лемма 4.
Справедливо равенство
.Достаточно показать, что
.
Докажем последнее утверждение индукцией по
.
Пусть
и
. Покажем, что
.
Пусть
. Покажем, что
.
Поскольку
, мы имеем
.
По лемме 3 мы имеем
.
Следовательно,
.
Лемма 5.
Для всякого
мы имеем
.
В частности, если
и
, то
.Утверждение леммы 5 непосредственно вытекает из лемм 3 и 4.
Лемма 6.
Для всякого
множество
является ординалом.Покажем, что для всякого
множество
транзитивно.
Пусть
и
. Покажем, что
.
По лемме 5 найдутся
такие, что
,
и
.
Поскольку
, по лемме 5 мы имеем
.
Покажем, что для всякого
все элементы множества
транзитивны.
По лемме 5 все элементы множества
имеют вид
,
а значит, они транзитивны по доказанному выше.
Таким образом, для всякого
множество
транзитивно
и все его элементы транзитивны, т.е.
является ординалом.
Положим
![$A:=F[X]=\{F(x):x\in X\}$ $A:=F[X]=\{F(x):x\in X\}$](https://dxdy-03.korotkov.co.uk/f/6/6/f/66fb6ddc461e15d4dfe919b35e8f07b882.png)
.
Лемма 7.
Множество
является ординалом.По лемме 6 все элементы множества
транзитивны.
Остается показать, что само множество
транзитивно.
Пусть
. Покажем, что
.
Поскольку
, имеется
такой, что
.
Поскольку
, по лемме 5 имеется
такой, что
.
Следовательно,
.
Лемма 8.
Функция
является порядковым изоморфизмом
на ординал
.По определению
функция
является сюръекцией
на
.
Покажем, что для любых
из
следует
.
По лемме 5 из
следует
, т.е.
.
Покажем, что для любых
из
следует
.
Пусть
. Покажем, что
.
Если бы
или
, то с учетом доказанного выше мы бы имели
или
вопреки неравенству
.
Следовательно,
(в силу линейности порядка на
).