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

### Boolean Properties of Sets

by
Zinaida Trybulec, and
Halina Swieczkowska

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 = {};

::
::

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;

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