Theorem S.I.1
If x and y are sets then {x,y} = {y,x} and {x,y} != O.
Proof
Let z = {x,y}.
By Definition S.A.1 /\(a) (a:-z <=> (a = x or a = y)).
Thus /\(a) (a:-z <=> (a = y or a = x)). So z = {y,x}.
By Definition S.A.1 x:-{x,y}.
Thus by Axiom ZF1 {x,y} != O.
Definition S.I.2 - Intersection
Let x be a set.
We define that n(x) = {a:-u(x)|/\(b:-x) a:-b}.
Definition S.I.3 - Basic set operations
Let x,y be sets.
We define that:
x u y = u({x,y}),
x n y = n({x,y}),
x\y = {a:-x|!(a:-y)}.
x u y, x n y and x\y are sets
by Axiom ZF5 and Axiom ZF4.
Theorem S.I.4
If x,y,z are sets then the following statements are true.
(1) x u y = z <=> /\(a) ( a:-z <=> (a:-x or a:-y) ),
(2) x n y = z <=> /\(a) ( a:-z <=> (a:-x and a:-y) ),
(3) x\y = z <=> /\(a) ( a:-z <=> a:-x and !(a:-y) ),
Proof
(1)
Assume that x u y = z. By Definition S.I.3 z = u({x,y}).
Take any set a.
a:-z <=> a:-u({x,y}) <=> \/(w) w:-{x,y} and a:-w <=>
\/(w) (w = x or w = y) and a:-w <=> a:-x or a:-y.
We have showed (=>).
Assume that /\(a) a:-z <=> (a:-x or a:-y).
Take any set a.
a:-z <=> (a:-x or a:-y) <=>
\/(w) (w = x or w = y) and a:-w <=>
\/(w) w:-{x,y} and a:-w <=> a:-u({x,y}) <=> a:-x u y.
By Axiom ZF1 z = x u y.
We have showed (<=).
(2)
Notice that:
x n y = n({x,y}) = {a:-u({x,y}) | /\(b:-{x,y}) a:-b} =
{a:-x u y | a:-x and a:-y}.
Assume that x n y = z. Then z = {a:-x u y | a:-x and a:-y}.
Take any set a.
It is obvious that (a:-z => a:-x and a:-y).
We have to show (a:-x and a:-y => a:-z).
If a:-x and a:-y then by Definition S.A.1
and Definition S.I.3 a:-u({x,y}) = x u y.
Thus by Definition S.A.2 a:-{b:-x u y | b:-x and b:-y}.
So a:-z.
We have showed that
x n y = z => ( /\(a) a:-z <=> (a:-x and a:-y) ).
Now, assume that /\(a) a:-z <=> a:-x and a:-y.
Take any set a.
a:-z <=> a:-x and a:-y <=>
a:-{b:-x u y | b:-x and b:-y} <=> a:- x n y.
By Axiom ZF1 z = x n y.
We have showed that
( /\(a) a:-z <=> (a:-x and a:-y) ) => z = x n y.
(3)
x\y = z <=> z = {b:-x|!(b:-y)} <=>
(a:-z <=> a:-x and !(a:-y)).
Theorem S.I.5 - Bool Algebra
If x,y,z are sets then the following statements are true.
(1) x u O = x,
(2) x u y = y u x,
(3) (x u y) u z = x u (y u z),
(4) x n O = O,
(5) x n y = y n x,
(6) (x n y) n z = x n (y n z),
(7) x u (y n z) = (x u y) n (x u z),
(8) x n (y u z) = (x n y) u (x n z),
(9) z\(x u y) = (z\x) n (z\y),
(10) z\(x n y) = (z\x) u (z\y).
Proof
One can prove the statements above
applying Theorem S.I.4 and Axiom ZF1.
Definitin S.I.6 - Inclusion
Let x,y be sets.
We define that x c y <=> ( /\(a) (a:-x => a:-y) ).
Theorem S.I.7
If x,y,z are sets then the following statements are true.
(1) O c x,
(2) x c x,
(3) x c y and y c z => x c z,
(4) x c y and y c x => x = y,
(5) x c y => (z u x) c (z u y),
(6) x c y => (z n x) c (z n y),
(7) y\x c y.
Proof
One can prove the statements above
applying Theorem S.I.4 and Axiom ZF1.
Theorem S.I.8
If x,y,x are sets then the following statements are true.
(1) x c y u x,
(2) x c y n x.
(3) y c x => x\(x\y) = y.
Proof
(1)
By Theorem S.I.7.1 we have O c y.
By Theorem S.I.7.5 and Theorem S.I.5.1 x = (O u x) c y u x.
(2)
By Theorem S.I.7.1 we have O c y.
By Theorem S.I.7.5 and Theorem S.I.5.1 x = (O n x) c y n x.
(3)
We have
x\(x\y) = {z:-x | !(z:-x\y)} = {z:-x | !(z:-x and !(x:-y))} =
{z:-x | !(z:-x) or x:-y} = {z:-x | x:-y} = y.
Theorem S.I.9
If x,z are sets, z:-x and z != O then u(x) != O.
Proof
By Definition S.A.1 /\(a) (a:-u(x) <=> \/(b:-x) a:-b).
We have z:-x and z != O. Thus we have a:-z. Thus a:-u(x). So u(x) != O.