Неупорядоченная пара собственных классов

[nide9]

В книге Мендельсона на стр. 180 вводится функциональная буква $\{X, Y\}$ для обозначения неупорядоченной пары любых двух классов $X$ и $Y$. $\{X, Y\} = 0$, если хотя бы один из классов $X$, $Y$ не является множеством. Вводится неупорядоченная пара на основании следующей теоремы, которую у меня не получается доказать:
$\vdash_{NBG} \exists_1Z((M(X) \& M(Y) \& \forall u(u \in Z \equiv u = X \vee u = Y))$ $ \vee (( \neg M(X) \vee \neg M(Y)) \& Z =\emptyset))$.
С доказательством единственности $Z$ проблем у меня не возникнет. Попробую дойти до доказательства этой теоремы сверху вниз. Разобьём формулу на две части и применим определение для связки $\vee$:
$\vdash_{NBG} \neg (\exists Z(M(X) \& M(Y) \& \forall u(u \in Z \equiv u = X \vee u = Y)))$ $ \supset \exists Z (( \neg M(X) \vee \neg M(Y)) \& Z =\emptyset)$.
Очевидно, $\neg (\exists Z(M(X) \& M(Y) \& \forall u(u \in Z \equiv u = X \vee u = Y)))$ $\vdash_{NBG} \exists Z (( \neg M(X) \vee \neg M(Y)) \& Z =\emptyset)$.
Применив определение для $\exists$ ($\exists x \mathcal{A} := \neg(\forall x(\neg \mathcal{A}))$) и логическую аксиому $\forall x_i \mathcal{A}(x_i) \supset \mathcal{A}(x_i) $, а также утверждение $\mathcal{A} \vdash \mathcal{A}$, получаем
$\neg (\exists Z(M(X) \& M(Y) \& \forall u(u \in Z \equiv u = X \vee u = Y)))$ $\vdash_{NBG} \neg (M(X) \& M(Y) \& \forall u(u \in Z \equiv u = X \vee u = Y))$.
Обозначим гипотезу буквой $\mathcal{C}$ и применим закон де Моргана.
$\mathcal{C} \vdash_{NBG} (\neg M(X) \vee \neg M(Y)) \vee \neg (\forall u(u \in Z \equiv u = X \vee u = Y) $.
Поменяем местами члены дизъюнкции и применим определение для $\vee$:
$\mathcal{C} \vdash_{NBG} \neg \neg (\forall u(u \in Z \equiv u = X \vee u = Y) \supset (\neg M(X) \vee \neg M(Y))$ (Возможно, это пригодится).
Осталось доказать $\mathcal{C}\vdash_{NBG} (\neg M(X) \vee \neg M(Y)) \& Z =\emptyset$.
После этого можно будет собрать доказательство изначальной теоремы, но я не знаю, как доказать последнее утверждение.

[gefest_md]

Вы подставили вместо $\forall Z$ некоторую переменную $Z$ и хотите доказать, что она просто так равна пустому множеству. Вы использовали несколько формул логики предикатов, но можно бы вспомнить и логику высказываний (ради $X$ и $Y$).