Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Some Basic Properties of Sets

by
Czeslaw Bylinski

MML identifier: ZFMISC_1
[ Mizar article, MML identifier index ]

```environ

vocabulary BOOLE, TARSKI, ZFMISC_1;
notation TARSKI, XBOOLE_0;
constructors TARSKI, XBOOLE_0;
clusters XBOOLE_0;

begin

reserve v,x,x1,x2,y,y1,y2,z,A,B,X,X1,X2,X3,X4,Y,Y1,Y2,Z,N,M for set;

definition
let x, y be set;
cluster [x,y] -> non empty;
end;

definition let X;
func bool X means
:: ZFMISC_1:def 1
Z in it iff Z c= X;
end;

definition let X1,X2;
func [: X1,X2 :] means
:: ZFMISC_1:def 2
z in it iff ex x,y st x in X1 & y in X2 & z = [x,y];
end;

definition let X1,X2,X3;
func [: X1,X2,X3 :] equals
:: ZFMISC_1:def 3
[:[:X1,X2:],X3:];
end;

definition let X1,X2,X3,X4;
func [: X1,X2,X3,X4 :] equals
:: ZFMISC_1:def 4
[:[:X1,X2,X3:],X4:];
end;

begin
::
::  Empty set.
::

theorem :: ZFMISC_1:1
bool {} = { {} };

theorem :: ZFMISC_1:2
union {} = {};

::
::  Singleton and unordered pairs.
::

canceled 3;

theorem :: ZFMISC_1:6
{x} c= {y} implies x = y;

canceled;

theorem :: ZFMISC_1:8
{x} = {y1,y2} implies x = y1;

theorem :: ZFMISC_1:9
{x} = {y1,y2} implies y1 = y2;

theorem :: ZFMISC_1:10
{ x1,x2 } = { y1,y2 } implies x1 = y1 or x1 = y2;

canceled;

theorem :: ZFMISC_1:12
{x} c= {x,y};

theorem :: ZFMISC_1:13
{x} \/ {y} = {x} implies x = y;

theorem :: ZFMISC_1:14
{x} \/ {x,y} = {x,y};

canceled;

theorem :: ZFMISC_1:16
{x} misses {y} implies x <> y;

theorem :: ZFMISC_1:17
x <> y implies {x} misses {y};

theorem :: ZFMISC_1:18
{x} /\ {y} = {x} implies x = y;

theorem :: ZFMISC_1:19
{x} /\ {x,y} = {x};

theorem :: ZFMISC_1:20
{x} \ {y} = {x} iff x <> y;

theorem :: ZFMISC_1:21
{x} \ {y} = {} implies x = y;

theorem :: ZFMISC_1:22
{x} \ {x,y} = {};

theorem :: ZFMISC_1:23
x <> y implies { x,y } \ { y } = { x };

theorem :: ZFMISC_1:24
{x} c= {y} implies x = y;

theorem :: ZFMISC_1:25
{z} c= {x,y} implies z = x or z = y;

theorem :: ZFMISC_1:26
{x,y} c= {z} implies x = z;

theorem :: ZFMISC_1:27
{x,y} c= {z} implies {x,y} = {z};

theorem :: ZFMISC_1:28
{x1,x2} c= {y1,y2} implies x1 = y1 or x1 = y2;

theorem :: ZFMISC_1:29
x <> y implies { x } \+\ { y } = { x,y };

theorem :: ZFMISC_1:30
bool { x } = { {} , { x }};

theorem :: ZFMISC_1:31
union { x } = x;

theorem :: ZFMISC_1:32
union {{x},{y}} = {x,y};

::
::  Ordered pairs.
::

theorem :: ZFMISC_1:33
[x1,x2] = [y1,y2] implies x1 = y1 & x2 = y2;

theorem :: ZFMISC_1:34
[x,y] in [:{x1},{y1}:] iff x = x1 & y = y1;

theorem :: ZFMISC_1:35
[:{x},{y}:] = {[x,y]};

theorem :: ZFMISC_1:36
[:{x},{y,z}:] = {[x,y],[x,z]} & [:{x,y},{z}:] = {[x,z],[y,z]};

::
::  Singleton and unordered pairs included in a set.
::

theorem :: ZFMISC_1:37
{x} c= X iff x in X;

theorem :: ZFMISC_1:38
{x1,x2} c= Z iff x1 in Z & x2 in Z;

::
::  Set included in a singleton (or unordered pair).
::

theorem :: ZFMISC_1:39
Y c= { x } iff Y = {} or Y = { x };

theorem :: ZFMISC_1:40
Y c= X & not x in Y implies Y c= X \ { x };

theorem :: ZFMISC_1:41
X <> {x} & X <> {} implies ex y st y in X & y <> x;

theorem :: ZFMISC_1:42
Z c= {x1,x2} iff Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2};

::
::   Sum of an unordered pair (or a singleton) and a set.
::

theorem :: ZFMISC_1:43
{z} = X \/ Y implies
X = {z} & Y = {z} or X = {} & Y = {z} or X = {z} & Y = {};

theorem :: ZFMISC_1:44
{z} = X \/ Y & X <> Y implies X = {} or Y = {};

theorem :: ZFMISC_1:45
{x} \/ X c= X implies x in X;

theorem :: ZFMISC_1:46
x in X implies {x} \/ X = X;

theorem :: ZFMISC_1:47
{x,y} \/ Z c= Z implies x in Z;

theorem :: ZFMISC_1:48
x in Z & y in Z implies {x,y} \/ Z = Z;

theorem :: ZFMISC_1:49
{x} \/ X <> {};

theorem :: ZFMISC_1:50
{x,y} \/ X <> {};

::
::  Intersection of an unordered pair (or a singleton) and a set.
::

theorem :: ZFMISC_1:51
X /\ {x} = {x} implies x in X;

theorem :: ZFMISC_1:52
x in X implies X /\ {x} = {x};

theorem :: ZFMISC_1:53
x in Z & y in Z implies {x,y} /\ Z = {x,y};

theorem :: ZFMISC_1:54
{x} misses X implies not x in X;

theorem :: ZFMISC_1:55
{x,y} misses Z implies not x in Z;

theorem :: ZFMISC_1:56
not x in X implies {x} misses X;

theorem :: ZFMISC_1:57
not x in Z & not y in Z implies {x,y} misses Z;

theorem :: ZFMISC_1:58
{x} misses X or {x} /\ X = {x};

theorem :: ZFMISC_1:59
{x,y} /\ X = {x} implies not y in X or x = y;

theorem :: ZFMISC_1:60
x in X & (not y in X or x = y) implies {x,y} /\ X = {x};

canceled 2;

theorem :: ZFMISC_1:63
{x,y} /\ X = {x,y} implies x in X;

::
::   Difference of an unordered pair (or a singleton) and a set.
::

theorem :: ZFMISC_1:64
z in X \ {x} iff z in X & z <> x;

theorem :: ZFMISC_1:65
X \ {x} = X iff not x in X;

theorem :: ZFMISC_1:66
X \ {x} = {} implies X = {} or X = {x};

theorem :: ZFMISC_1:67
{x} \ X = {x} iff not x in X;

theorem :: ZFMISC_1:68
{x} \ X = {} iff x in X;

theorem :: ZFMISC_1:69
{x} \ X = {} or {x} \ X = {x};

theorem :: ZFMISC_1:70
{x,y} \ X = {x} iff not x in X & (y in X or x = y);

canceled;

theorem :: ZFMISC_1:72
{x,y} \ X = {x,y} iff not x in X & not y in X;

theorem :: ZFMISC_1:73
{x,y} \ X = {} iff x in X & y in X;

theorem :: ZFMISC_1:74
{x,y} \ X = {} or {x,y} \ X = {x} or {x,y} \ X = {y} or {x,y} \ X = {x,y};

theorem :: ZFMISC_1:75
X \ {x,y} = {} iff X = {} or X = {x} or X = {y} or X = {x,y};

::
::  Power Set.
::

canceled 3;

theorem :: ZFMISC_1:79
A c= B implies bool A c= bool B;

theorem :: ZFMISC_1:80
{ A } c= bool A;

theorem :: ZFMISC_1:81
bool A \/ bool B c= bool (A \/ B);

theorem :: ZFMISC_1:82
bool A \/ bool B = bool (A \/ B) implies A,B are_c=-comparable;

theorem :: ZFMISC_1:83
bool (A /\ B) = bool A /\ bool B;

theorem :: ZFMISC_1:84
bool (A \ B) c= { {} } \/ (bool A \ bool B);

canceled;

theorem :: ZFMISC_1:86
bool (A \ B) \/ bool (B \ A) c= bool (A \+\ B);

::
::  Union of a set.
::

canceled 5;

theorem :: ZFMISC_1:92
X in A implies X c= union A;

theorem :: ZFMISC_1:93
union { X,Y } = X \/ Y;

theorem :: ZFMISC_1:94
(for X st X in A holds X c= Z) implies union A c= Z;

theorem :: ZFMISC_1:95
A c= B implies union A c= union B;

theorem :: ZFMISC_1:96
union (A \/ B) = union A \/ union B;

theorem :: ZFMISC_1:97
union (A /\ B) c= union A /\ union B;

theorem :: ZFMISC_1:98
(for X st X in A holds X misses B) implies union A misses B;

theorem :: ZFMISC_1:99
union bool A = A;

theorem :: ZFMISC_1:100
A c= bool union A;

theorem :: ZFMISC_1:101
(for X,Y st X<>Y & X in A \/ B & Y in A \/ B holds X misses Y)
implies union(A /\ B) = union A /\ union B;

::
::  Cartesian product.
::

theorem :: ZFMISC_1:102
z in [:X,Y:] implies ex x,y st [x,y] = z;

theorem :: ZFMISC_1:103
A c= [:X,Y:] & z in A implies ex x,y st x in X & y in Y & z = [x,y];

theorem :: ZFMISC_1:104
z in [:X1, Y1:] /\ [:X2, Y2:]
implies ex x,y st z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2;

theorem :: ZFMISC_1:105
[:X,Y:] c= bool bool (X \/ Y);

theorem :: ZFMISC_1:106
[x,y] in [:X,Y:] iff x in X & y in Y;

theorem :: ZFMISC_1:107
[x,y] in [:X,Y:] implies [y,x] in [:Y,X:];

theorem :: ZFMISC_1:108
(for x,y holds [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:])
implies [:X1,Y1:]=[:X2,Y2:];

theorem :: ZFMISC_1:109
A c= [:X,Y:] & (for x,y st [x,y] in A holds [x,y] in B) implies A c= B;

theorem :: ZFMISC_1:110
A c= [:X1,Y1:] & B c= [:X2,Y2:] & (for x,y holds [x,y] in A iff [x,y] in B)
implies A = B;

theorem :: ZFMISC_1:111
(for z st z in A ex x,y st z=[x,y]) &
(for x,y st [x,y] in A holds [x,y] in B)
implies A c= B;

theorem :: ZFMISC_1:112
(for z st z in A ex x,y st z = [x,y]) & (for z st z in B ex x,y st z=[x,y]) &
(for x,y holds [x,y] in A iff [x,y] in B)
implies A = B;

theorem :: ZFMISC_1:113
[:X,Y:] = {} iff X = {} or Y = {};

theorem :: ZFMISC_1:114
X <> {} & Y <> {} & [:X,Y:] = [:Y,X:] implies X = Y;

theorem :: ZFMISC_1:115
[:X,X:] = [:Y,Y:] implies X = Y;

theorem :: ZFMISC_1:116
X c= [:X,X:] implies X = {};

theorem :: ZFMISC_1:117
Z <> {} & ([:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:]) implies X c= Y;

theorem :: ZFMISC_1:118
X c= Y implies [:X,Z:] c= [:Y,Z:] & [:Z,X:] c= [:Z,Y:];

theorem :: ZFMISC_1:119
X1 c= Y1 & X2 c= Y2 implies [:X1,X2:] c= [:Y1,Y2:];

theorem :: ZFMISC_1:120
[:X \/ Y, Z:] = [:X, Z:] \/ [:Y, Z:] & [:Z, X \/ Y:] = [:Z, X:] \/ [:Z, Y:];

theorem :: ZFMISC_1:121
[:X1 \/ X2, Y1 \/ Y2:] = [:X1,Y1:] \/ [:X1,Y2:] \/ [:X2,Y1:] \/ [:X2,Y2:];

theorem :: ZFMISC_1:122
[:X /\ Y, Z:] = [:X, Z:] /\ [:Y, Z:] & [:Z, X /\ Y:] = [:Z, X:] /\ [:Z, Y:];

theorem :: ZFMISC_1:123
[:X1 /\ X2, Y1 /\ Y2:] = [:X1,Y1:] /\ [:X2, Y2:];

theorem :: ZFMISC_1:124
A c= X & B c= Y implies [:A,Y:] /\ [:X,B:] = [:A,B:];

theorem :: ZFMISC_1:125
[:X \ Y, Z:] = [:X, Z:] \ [:Y, Z:] & [:Z, X \ Y:] = [:Z, X:] \ [:Z, Y:];

theorem :: ZFMISC_1:126
[:X1,X2:] \ [:Y1,Y2:] = [:X1\Y1,X2:] \/ [:X1,X2\Y2:];

theorem :: ZFMISC_1:127
X1 misses X2 or Y1 misses Y2 implies [:X1,Y1:] misses [:X2,Y2:];

theorem :: ZFMISC_1:128
[x,y] in [:{z},Y:] iff x = z & y in Y;

theorem :: ZFMISC_1:129
[x,y] in [:X,{z}:] iff x in X & y = z;

theorem :: ZFMISC_1:130
X <> {} implies [:{x},X:] <> {} & [:X,{x}:] <> {};

theorem :: ZFMISC_1:131
x <> y implies [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:];

theorem :: ZFMISC_1:132
[:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:];

canceled;

theorem :: ZFMISC_1:134
X1 <> {} & Y1 <> {} & [:X1,Y1:] = [:X2,Y2:] implies X1 = X2 & Y1 = Y2;

theorem :: ZFMISC_1:135
X c= [:X,Y:] or X c= [:Y,X:] implies X = {};

theorem :: ZFMISC_1:136
ex M st N in M &
(for X,Y holds X in M & Y c= X implies Y in M) &
(for X holds X in M implies bool X in M) &
(for X holds X c= M implies X,M are_equipotent or X in M);
```