The abstract of the Mizar article:

Some Basic Properties of Sets

by

Czeslaw Bylinski

Received February 1, 1989

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);