The abstract of the Mizar article:

Boolean Properties of Sets

by

Zinaida Trybulec, and

Halina Swieczkowska

Received January 6, 1989

MML identifier: BOOLE

[ Mizar article, MML identifier index ]

environ

 vocabulary TARSKI, BOOLE;
 notation TARSKI;
 constructors TARSKI;


begin

 reserve x,y,z for set, X,Y,Z,V for set;

 scheme Separation { A()-> set, P[set] } :
   ex X st for x holds x in X iff x in A() & P[x];

definition
  func {} -> set means
:: BOOLE:def 1  
not ex x st x in it;
 let X,Y;
  func X \/ Y -> set means
:: BOOLE:def 2  
x in it iff x in X or x in Y;
  commutativity;
  idempotence;

  func X /\ Y -> set means
:: BOOLE:def 3  
x in it iff x in X & x in Y;
  commutativity;
  idempotence;

  func X \ Y -> set means
:: BOOLE:def 4  
x in it iff x in X & not x in Y;
end;

definition let X,Y;
  pred X misses Y means
:: BOOLE:def 5
 X /\ Y = {};
  symmetry;
  antonym X meets Y;
end;

definition let X,Y;
 canceled;

 func X \+\ Y -> set equals
:: BOOLE:def 7
 (X \ Y) \/ (Y \ X);
 commutativity;
end;

::
::     THEOREMS RELATED TO MEMBERSHIP
::
::            1.Definitional theorems
::

definition let X,Y;
 redefine pred X = Y means
:: BOOLE:def 8
  X c= Y & Y c= X;
end;

theorem :: BOOLE:1 
 X meets Y iff ex x st x in X & x in Y;

theorem :: BOOLE:2 
 X meets Y iff ex x st x in X /\ Y;

canceled 20;

theorem :: BOOLE:23
  x in X \+\ Y iff not (x in X iff x in Y);

canceled;

theorem :: BOOLE:25
  (for x holds not x in X iff (x in Y iff x in Z)) implies X = Y \+\ Z;

::
::     THEOREMS IN WHICH "in" DOES NOT OCCUR
::
::       2.1 Theorems related to inclusion
::

canceled;

theorem :: BOOLE:27
  {} c= X;

canceled;

theorem :: BOOLE:29
  X c= Y & Y c= Z implies X c= Z;

theorem :: BOOLE:30
  X c= {} implies X = {};

theorem :: BOOLE:31
  X c= X \/ Y;

theorem :: BOOLE:32
  X c= Z & Y c= Z implies X \/ Y c= Z;

theorem :: BOOLE:33
  X c= Y implies X \/ Z c= Y \/ Z;

theorem :: BOOLE:34
  X c= Y & Z c= V implies X \/ Z c= Y \/ V;

theorem :: BOOLE:35
  X c= Y implies X \/ Y = Y;

canceled;

theorem :: BOOLE:37
  X /\ Y c= X;

theorem :: BOOLE:38
  X /\ Y c= X \/ Z;

theorem :: BOOLE:39
  Z c= X & Z c= Y implies Z c= X /\ Y;

theorem :: BOOLE:40
  X c= Y implies X /\ Z c= Y /\ Z;

theorem :: BOOLE:41
  X c= Y & Z c= V implies X /\ Z c= Y /\ V;

theorem :: BOOLE:42
  X c= Y implies X /\ Y = X;

canceled;

theorem :: BOOLE:44
  X c= Z implies X \/ Y /\ Z = (X \/ Y) /\ Z;

theorem :: BOOLE:45
  X \ Y = {} iff X c= Y;

theorem :: BOOLE:46 
  X c= Y implies X \ Z c= Y \ Z;

theorem :: BOOLE:47 
  X c= Y implies Z \ Y c= Z \ X;

theorem :: BOOLE:48
  X c= Y & Z c= V implies X \ V c= Y \ Z;

theorem :: BOOLE:49
  X \ Y c= X;

theorem :: BOOLE:50
  X c= Y \ X implies X = {};

theorem :: BOOLE:51
  X c= Y & X c= Z & Y misses Z  implies X = {};

theorem :: BOOLE:52
  X c= Y \/ Z implies X \ Y c= Z;

theorem :: BOOLE:53
  (X /\ Y) \/ (X /\ Z) = X implies X c= Y \/ Z;

theorem :: BOOLE:54
  X c= Y implies Y = X \/ (Y \ X);

theorem :: BOOLE:55
  X c= Y & Y misses Z implies X misses Z;

theorem :: BOOLE:56
  X = Y \/ Z iff Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V;

theorem :: BOOLE:57
  X = Y /\ Z iff X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X;

theorem :: BOOLE:58
  X \ Y c= X \+\ Y;

::
::       2.2 Identities
::

theorem :: BOOLE:59
  X \/ Y = {} implies X = {} & Y = {};

theorem :: BOOLE:60
  X \/ {} = X;

theorem :: BOOLE:61
  X misses {};

canceled 2;

theorem :: BOOLE:64
  (X \/ Y) \/ Z = X \/ (Y \/ Z);

canceled 2;

theorem :: BOOLE:67
  (X /\ Y) /\ Z = X /\ (Y /\ Z);

theorem :: BOOLE:68
  X /\ (X \/ Y) = X;

theorem :: BOOLE:69
  X \/ (X /\ Y) = X;

theorem :: BOOLE:70
  X /\ (Y \/ Z) = X /\ Y \/ X /\ Z;

theorem :: BOOLE:71
  X \/ Y /\ Z = (X \/ Y) /\ (X \/ Z);

theorem :: BOOLE:72
  (X /\ Y) \/ (Y /\ Z) \/ (Z /\ X) = (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X);

canceled;

theorem :: BOOLE:74
  X \ {} = X;

theorem :: BOOLE:75
  {} \ X = {};

theorem :: BOOLE:76
  X \ (X \/ Y) = {};

theorem :: BOOLE:77
  X \ X /\ Y = X \ Y;

theorem :: BOOLE:78
  X \ Y misses Y;

theorem :: BOOLE:79
  X \/ (Y \ X) = X \/ Y;

theorem :: BOOLE:80
  X /\ Y \/ (X \ Y) = X;

theorem :: BOOLE:81
  X \ (Y \ Z) = (X \ Y) \/ X /\ Z;

theorem :: BOOLE:82
  X \ (X \ Y) = X /\ Y;

theorem :: BOOLE:83
  (X \/ Y) \ Y = X \ Y;

theorem :: BOOLE:84
  X misses Y iff X \ Y = X;

theorem :: BOOLE:85
  X \ (Y \/ Z) = (X \ Y) /\ (X \ Z);

theorem :: BOOLE:86
  X \ (Y /\ Z) = (X \ Y) \/ (X \ Z);

theorem :: BOOLE:87
  (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X);

theorem :: BOOLE:88
  (X \ Y) \ Z = X \ (Y \/ Z);

theorem :: BOOLE:89
  (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z);

theorem :: BOOLE:90
  X \ Y = Y \ X implies X = Y;

canceled;

theorem :: BOOLE:92
  X \+\ {} = X;

theorem :: BOOLE:93
  X \+\ X = {};

canceled;

theorem :: BOOLE:95
  X \/ Y = (X \+\ Y) \/ X /\ Y;

theorem :: BOOLE:96
  X \+\ Y = (X \/ Y) \ X /\ Y;

theorem :: BOOLE:97
  (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z));

theorem :: BOOLE:98
  X \ (Y \+\ Z) = X \ (Y \/ Z) \/ X /\ Y /\ Z;

theorem :: BOOLE:99
  (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z);

::
::       2.3  "meets" and "misses"
::

theorem :: BOOLE:100
  X meets Y \/ Z iff X meets Y or X meets Z;

theorem :: BOOLE:101
  X meets Y & Y c= Z implies X meets Z;

theorem :: BOOLE:102
  X meets Y /\ Z implies X meets Y;

canceled;

theorem :: BOOLE:104
  X misses {};

canceled 5;

theorem :: BOOLE:110
  X meets X iff X <> {};

theorem :: BOOLE:111
  X /\ Y misses X \ Y;

theorem :: BOOLE:112
  X /\ Y misses X \+\ Y;

theorem :: BOOLE:113
  X meets Y \ Z implies X meets Y;

theorem :: BOOLE:114
  X c= Y & X c= Z & Y misses Z implies X = {};

::
::                  ADDITIONAL THEOREMS
::

theorem :: BOOLE:115
  X \ Y c= Z & Y \ X c= Z implies X \+\ Y c= Z;

theorem :: BOOLE:116
  X /\ (Y \ Z) = (X /\ Y) \ Z;

theorem :: BOOLE:117
  X /\ (Y \ Z) = X /\ Y \ X /\ Z;

canceled 2;

theorem :: BOOLE:120
  X c= Y \/ Z & X misses Z implies X c= Y;

begin :: Addendum, 2000.01.10, A.T.

definition let X,Y;
 pred X c< Y means
:: BOOLE:def 9
 X c= Y & X <> Y;
 irreflexivity;
end;

theorem :: BOOLE:121
 X c< Y & Y c= Z implies X c< Z;

theorem :: BOOLE:122 
 X c= Y & Y c< Z implies X c< Z;

theorem :: BOOLE:123
 X c< Y & Y c< Z implies X c< Z;

theorem :: BOOLE:124
 X <> {} implies {} c< X;

theorem :: BOOLE:125
 not ex X st X c< {};

theorem :: BOOLE:126
 not ex X,Y st X c< Y & Y c< X;

theorem :: BOOLE:127
 X c= Y implies not Y c< X;