Теория множеств [1]

Обозначения:

/\ - для любых
\/ - существует
! - не
:- принадлежит
<:=:> - тогда и только тогда по определению
:= - определяется как (равно по определению)
{O} - пустое множество
u(x) - объединение по всем элементам семейства x.

В ZF основными (неопределяемыми) понятиями являются = и :-.

Аксиомы теории множеств ZF:

ZF1 [Объёмности] : x = y <=> ( /\(z) z:-x <=> z:-y )
Два множества равны <=> они состоят из одних элементов.
ZF2 [Пустого можества] : \/(y) : /\(x) !(x:-y)
Существует пустое множество.
ZF3 [Неупорядоченной пары] : \/(z) : /\(a) : (a:-z <=> (a = x или a = y))
Для любых двух множеств, существует множество, чьими единственными элементами они являются.
ZF4 [Выделения] : /\(z) \/(y) : /\(x) ( x:-y <=> (x:-z и A(x)) ). A - не содержит y.
Для любого множества z и свойства A, такого что на z оно либо истино, либо ложно, существует множество, состоящее в точности из тех x, для которых A(x) - истинно.
ZF5 [Объединения] : \/(y) : /\(a) ( a:-y <=> (\/(z) z:-x и a:-z) ).
Для любого множества x существует множество u(x), состоящее в точности из всех элементов, принадлежащих элементам из x
ZF6 [Степени] : /\(x) \/(z) : /\(y)( y:-z <=> ( /\(a) (a:-y => a:-x) ) ).
Для любого множества x существует множество всех его подмножеств P(x).
ZF7 [Бесконечности] : \/(m) : {O}:-m и /\(x) (x:-m => u({x,{x}}):-m).
Индуктивные множества существуют.
ZF9 [Фундирования] : x != {O} => \/(y) (y:-x и /\(a) !(a:-x и a:-y)).
Не существует убывающих цепей: x:-x, x:-y:-x, x:-y:-z:-x, ...

Определения:

D1 : {O} = y <:=:> /\(x) !(x:-y). Определение корректно, т.к. такое множество единственно: ZF1.
D2 : {x,y} = z <:=:> /\(a) (a:-z <=> (a = x или a = y)). Определим {x} = {x,x}. Корректно: ZF1.
D3 : {x:-z | A} = y <:=:> if /\(x) ( x:-y <=> (x:-z и A) ). Корректно: ZF1.
D4 : u(x) = y <:=:> /\(a) ( a:-y <=> (\/(z) z:-x и a:-z) ). Корректно: ZF1.