Copyright (c) 1989 Association of Mizar Users
environ
vocabulary TARSKI, BOOLE;
constructors TARSKI;
notation TARSKI;
definitions TARSKI;
theorems TARSKI;
schemes 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]
proof
A1: for x,y,z st (x = y & P[y]) & (x = z & P[z]) holds y = z;
consider X such that
A2: for x holds
x in X iff ex y st y in A() & (y = x & P[x]) from Fraenkel(A1);
take X; let x;
x in X iff ex y st y in A() & (y = x & P[x]) by A2;
hence thesis;
end;
definition
func {} -> set means :Def1: not ex x st x in it;
existence
proof
consider X;
consider Y such that A1: x in Y iff x in X & contradiction
from Separation;
take Y;
thus thesis by A1;
end;
uniqueness
proof
let X,Y such that A2: not ex x st x in X and
A3: not ex x st x in Y;
x in Y iff x in X by A2,A3;
hence thesis by TARSKI:2;
end;
let X,Y;
func X \/ Y -> set means :Def2: x in it iff x in X or x in Y;
existence
proof
take union {X,Y};
let x;
thus x in union {X,Y} implies x in X or x in Y
proof
assume x in union {X,Y};
then ex X0 being set st x in X0 & X0 in {X,Y} by TARSKI:def 4;
hence thesis by TARSKI:def 2;
end;
assume x in X or x in Y;
then consider X0 being set such that
A4: X0 = X or X0 = Y and
A5: x in X0;
X0 in {X,Y} by A4,TARSKI:def 2;
hence x in union {X,Y} by TARSKI:def 4,A5;
end;
uniqueness
proof
let A1, A2 be set such that
A6: x in A1 iff x in X or x in Y and
A7: x in A2 iff x in X or x in Y;
now
let x;
x in A1 iff x in X or x in Y by A6;
hence x in A1 iff x in A2 by A7;
end;
hence A1 = A2 by TARSKI:2;
end;
commutativity;
idempotence;
func X /\ Y -> set means :Def3: x in it iff x in X & x in Y;
existence from Separation;
uniqueness
proof
let A1, A2 be set such that
A8: x in A1 iff x in X & x in Y and
A9: x in A2 iff x in X & x in Y;
now
let x;
x in A1 iff x in X & x in Y by A8;
hence x in A1 iff x in A2 by A9;
end;
hence A1 = A2 by TARSKI:2;
end;
commutativity;
idempotence;
func X \ Y -> set means :Def4: x in it iff x in X & not x in Y;
existence from Separation;
uniqueness
proof
let A1, A2 be set such that
A10: x in A1 iff x in X & not x in Y and
A11: x in A2 iff x in X & not x in Y;
now
let x;
x in A1 iff x in X & not x in Y by A10;
hence x in A1 iff x in A2 by A11;
end;
hence A1 = A2 by TARSKI:2;
end;
end;
definition let X,Y;
pred X misses Y means
:Def5: X /\ Y = {};
symmetry;
antonym X meets Y;
end;
definition let X,Y;
canceled;
func X \+\ Y -> set equals
:Def7: (X \ Y) \/ (Y \ X);
correctness;
commutativity;
end;
::
:: THEOREMS RELATED TO MEMBERSHIP
::
:: 1.Definitional theorems
::
definition let X,Y;
redefine pred X = Y means
:Def8: X c= Y & Y c= X;
compatibility
proof
thus X = Y implies X c= Y & Y c= X;
assume X c= Y & Y c= X;
then for x holds ( x in X iff x in Y) by TARSKI:def 3;
hence X = Y by TARSKI:2;
end;
end;
theorem Th1:
X meets Y iff ex x st x in X & x in Y
proof
hereby assume X meets Y;
then X /\ Y <> {} by Def5;
then consider x such that
A1: x in X /\ Y by Def1;
take x;
thus x in X & x in Y by Def3,A1;
end;
given x such that
A2: x in X & x in Y;
x in X /\ Y by Def3,A2;
then X /\ Y <> {} by Def1;
hence thesis by Def5;
end;
theorem Th2:
X meets Y iff ex x st x in X /\ Y
proof
hereby assume X meets Y;
then X /\ Y <> {} by Def5;
then consider x such that
A1: x in X /\ Y by Def1;
take x;
thus x in X /\ Y by A1;
end;
given x such that
A2: x in X /\ Y;
X /\ Y <> {} by A2,Def1;
hence thesis by Def5;
end;
canceled 20;
theorem
x in X \+\ Y iff not (x in X iff x in Y)
proof
X \+\ Y = (X \ Y) \/ (Y \ X) by Def7;
then x in X \+\ Y iff x in X \ Y or x in Y \ X by Def2;
hence thesis by Def4;
end;
canceled;
theorem
(for x holds not x in X iff (x in Y iff x in Z)) implies X = Y \+\ Z
proof
assume A1: not x in X iff (x in Y iff x in Z);
now let x;
x in X iff x in Y & not x in Z or x in Z & not x in Y by A1;
then x in X iff x in Y \ Z or x in Z \ Y by Def4;
then x in X iff x in (Y \ Z) \/ (Z \ Y) by Def2;
hence x in X iff x in Y \+\ Z by Def7;
end;
hence thesis by TARSKI:2;
end;
::
:: THEOREMS IN WHICH "in" DOES NOT OCCUR
::
:: 2.1 Theorems related to inclusion
::
canceled;
theorem
Th27: {} c= X
proof let x;
thus thesis by Def1;
end;
canceled;
theorem
Th29: X c= Y & Y c= Z implies X c= Z
proof
assume that A1: X c= Y and
A2: Y c= Z;
let x; assume x in X; then x in Y by A1,TARSKI:def 3;
hence thesis by A2,TARSKI:def 3;
end;
theorem
Th30: X c= {} implies X = {}
proof
assume X c= {};
hence X c= {} & {} c= X by Th27;
end;
theorem
Th31: X c= X \/ Y
proof
let x;
thus thesis by Def2;
end;
theorem
Th32: X c= Z & Y c= Z implies X \/ Y c= Z
proof
assume A1: X c= Z & Y c= Z;
let x;
assume x in X \/ Y;
then x in X or x in Y by Def2;
hence thesis by A1,TARSKI:def 3;
end;
theorem
X c= Y implies X \/ Z c= Y \/ Z
proof
assume A1: X c= Y;
let x; assume x in X \/ Z;
then x in X or x in Z by Def2;
then x in Y or x in Z by A1,TARSKI:def 3;
hence thesis by Def2;
end;
theorem
X c= Y & Z c= V implies X \/ Z c= Y \/ V
proof
assume A1: X c= Y;
assume A2: Z c= V;
let x; assume x in X \/ Z;
then x in X or x in Z by Def2;
then x in Y or x in V by A1,A2,TARSKI:def 3;
hence thesis by Def2;
end;
theorem
X c= Y implies X \/ Y = Y
proof
assume A1: X c= Y;
thus X \/ Y c= Y
proof
let x; assume x in X \/ Y ; then
x in X or x in Y by Def2;
hence thesis by A1,TARSKI:def 3;
end;
let x;
thus thesis by Def2;
end;
canceled;
theorem
Th37: X /\ Y c= X
proof
let x;
thus thesis by Def3;
end;
theorem
X /\ Y c= X \/ Z
proof
X /\ Y c= X & X c= X \/ Z by Th31,Th37;
hence thesis by Th29;
end;
theorem
Th39: Z c= X & Z c= Y implies Z c= X /\ Y
proof
assume A1: Z c= X & Z c= Y;
let x;
assume x in Z;
then x in X & x in Y by A1,TARSKI:def 3;
hence thesis by Def3;
end;
theorem
Th40: X c= Y implies X /\ Z c= Y /\ Z
proof
assume A1: X c= Y;
let x;
assume x in X /\ Z;
then x in X & x in Z by Def3;
then x in Y & x in Z by A1,TARSKI:def 3;
hence thesis by Def3;
end;
theorem
X c= Y & Z c= V implies X /\ Z c= Y /\ V
proof
assume A1: X c= Y & Z c= V;
let x;
assume x in X /\ Z;
then x in X & x in Z by Def3;
then x in Y & x in V by A1,TARSKI:def 3;
hence thesis by Def3;
end;
theorem
Th42: X c= Y implies X /\ Y = X
proof
assume A1: X c= Y;
thus X /\ Y c= X by Th37;
let x;
assume x in X;
then x in X & x in Y by A1,TARSKI:def 3;
hence thesis by Def3;
end;
canceled;
theorem
X c= Z implies X \/ Y /\ Z = (X \/ Y) /\ Z
proof assume
A1: X c= Z;
thus X \/ Y /\ Z c= (X \/ Y) /\ Z
proof let x;
assume x in X \/ Y /\ Z;
then x in X or x in Y /\ Z by Def2;
then x in X or x in Y & x in Z by Def3;
then x in (X \/ Y) & x in Z by A1,Def2,TARSKI:def 3;
hence thesis by Def3;
end;
let x;
assume x in (X \/ Y) /\ Z;
then x in X \/ Y & x in Z by Def3;
then (x in X or x in Y) & x in Z by Def2;
then x in X & x in Z or x in Y /\ Z by Def3;
hence thesis by Def2;
end;
theorem
Th45: X \ Y = {} iff X c= Y
proof
thus X \ Y = {} implies X c= Y
proof
assume A1:X \ Y = {};
let x;
assume x in X & not x in Y;
then x in X \ Y by Def4;
hence contradiction by A1,Def1;
end;
assume A2:X c= Y;
now let x;
x in X & not x in Y iff contradiction by A2,TARSKI:def 3;
hence x in X \ Y iff x in {} by Def4,Def1;
end;
hence thesis by TARSKI:2;
end;
theorem Th46:
X c= Y implies X \ Z c= Y \ Z
proof
assume A1:X c= Y;
let x;
assume x in X \ Z;
then x in X & not x in Z by Def4;
then x in Y & not x in Z by A1,TARSKI:def 3;
hence thesis by Def4;
end;
theorem Th47:
X c= Y implies Z \ Y c= Z \ X
proof
assume A1:X c= Y;
let x;
assume x in Z \ Y;
then x in Z & not x in Y by Def4;
then x in Z & not x in X by A1,TARSKI:def 3;
hence thesis by Def4;
end;
theorem
X c= Y & Z c= V implies X \ V c= Y \ Z
proof
assume that A1:X c= Y and
A2:Z c= V;
A3:X \ V c= Y \ V by A1,Th46;
Y \ V c= Y \ Z by A2, Th47;
hence thesis by A3,Th29;
end;
theorem
X \ Y c= X
proof
let x;
thus thesis by Def4;
end;
theorem
X c= Y \ X implies X = {}
proof
assume A1:X c= Y \ X;
thus X c= {}
proof let x;
assume
A2: x in X;
then x in Y \ X by A1,TARSKI:def 3;
hence thesis by A2,Def4;
end;
thus thesis by Th27;
end;
theorem
X c= Y & X c= Z & Y misses Z implies X = {}
proof
assume that A1:X c= Y and
A2:X c= Z and
A3:Y /\ Z = {};
X c= {} by A3,A1,A2,Th39;
hence X = {} by Th30;
end;
theorem
X c= Y \/ Z implies X \ Y c= Z
proof
assume A1: X c= Y \/ Z;
let x; assume x in X \ Y;
then x in X & not x in Y by Def4;
then x in Y \/ Z & not x in Y by A1,TARSKI:def 3;
hence thesis by Def2;
end;
theorem
(X /\ Y) \/ (X /\ Z) = X implies X c= Y \/ Z
proof
assume A1:(X /\ Y) \/ (X /\ Z) = X;
now let x;
assume x in X;
then x in (X /\ Y) or x in (X /\ Z) by Def2,A1;
then (x in X & x in Y) or (x in X & x in Z) by Def3;
hence x in Y \/ Z by Def2;
end;
hence thesis by TARSKI:def 3;
end;
theorem
X c= Y implies Y = X \/ (Y \ X)
proof
assume A1: X c= Y;
now let x;
x in Y iff x in X or x in (Y \ X) by Def4,A1,TARSKI:def 3;
hence x in Y iff x in X \/ (Y \ X) by Def2;
end;
hence thesis by TARSKI:2;
end;
theorem
X c= Y & Y misses Z implies X misses Z
proof
assume A1: X c= Y & Y /\ Z = {}; then
X /\ Z c= Y /\ Z by Th40; then
X /\ Z = {} by A1,Th30;
hence thesis by Def5;
end;
theorem
X = Y \/ Z iff Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V
proof
thus X = Y \/ Z implies
Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V
by Th31,Th32;
assume that A1: Y c= X and
A2: Z c= X and
A3: Y c= V & Z c= V implies X c= V;
Y c= Y \/ Z & Z c= Y \/ Z by Th31;
hence X c= Y \/ Z by A3;
thus Y \/ Z c= X by A1,A2,Th32;
end;
theorem
X = Y /\ Z iff X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X
proof
thus X = Y /\ Z implies
X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X
by Th37,Th39;
assume that A1: X c= Y and
A2: X c= Z and
A3: V c= Y & V c= Z implies V c= X;
thus X c= Y /\ Z by Th39,A1,A2;
Y /\ Z c= Y & Y /\ Z c= Z implies Y /\ Z c= X by A3;
hence Y /\ Z c= X by Th37;
end;
theorem
X \ Y c= X \+\ Y
proof X \+\ Y = (X \ Y) \/ (Y \ X) by Def7; hence thesis by Th31; end;
::
:: 2.2 Identities
::
theorem
X \/ Y = {} implies X = {} & Y = {}
proof
assume
A1: X \/ Y = {};
A2:not ex x st x in X
proof
given x such that A3:x in X;
x in X \/ Y by Def2,A3;
hence contradiction by A1,Def1;
end;
not ex x st x in Y
proof
given x such that A4:x in Y;
x in X \/ Y by Def2,A4;
hence contradiction by A1,Def1;
end;
hence thesis by Def1,A2;
end;
theorem
Th60: X \/ {} = X
proof
thus X \/ {} c= X
proof let x;
assume x in X \/ {}; then x in X or x in {} by Def2;
hence thesis by Def1;
end;
let x;
thus thesis by Def2;
end;
theorem
X misses {}
proof
thus X /\ {} c= {}
proof let x;
thus thesis by Def3;
end;
let x;
thus thesis by Def1;
end;
canceled 2;
theorem
Th64: (X \/ Y) \/ Z = X \/ (Y \/ Z)
proof
thus (X \/ Y) \/ Z c= X \/ (Y \/ Z)
proof let x;
assume x in (X \/ Y) \/ Z;
then x in X \/ Y or x in Z by Def2;
then x in X or x in Y or x in Z by Def2;
then x in X or x in Y \/ Z by Def2;
hence thesis by Def2;
end;
let x;
assume x in X \/ (Y \/ Z);
then x in X or x in Y \/ Z by Def2;
then x in X or x in Y or x in Z by Def2;
then x in X \/ Y or x in Z by Def2;
hence thesis by Def2;
end;
canceled 2;
theorem
Th67: (X /\ Y) /\ Z = X /\ (Y /\ Z)
proof
thus (X /\ Y) /\ Z c= X /\ (Y /\ Z)
proof let x;
assume x in (X /\ Y) /\ Z;
then x in X /\ Y & x in Z by Def3;
then x in X & x in Y & x in Z by Def3;
then x in X & x in Y /\ Z by Def3;
hence thesis by Def3;
end;
let x;
assume x in X /\ (Y /\ Z);
then x in X & x in Y /\ Z by Def3;
then x in X & x in Y & x in Z by Def3;
then x in X /\ Y & x in Z by Def3;
hence thesis by Def3;
end;
theorem
X /\ (X \/ Y) = X
proof
thus X /\ (X \/ Y) c= X
proof let x;
thus thesis by Def3;
end;
let x;
assume x in X;
then x in X & x in X \/ Y by Def2;
hence thesis by Def3;
end;
theorem
Th69: X \/ (X /\ Y) = X
proof
thus X \/ (X /\ Y) c= X
proof let x;
assume x in X \/ (X /\ Y);
then x in X or x in X /\ Y by Def2;
hence thesis by Def3;
end;
let x;
thus thesis by Def2;
end;
theorem
Th70: X /\ (Y \/ Z) = X /\ Y \/ X /\ Z
proof
thus X /\ (Y \/ Z) c= X /\ Y \/ X /\ Z
proof let x;
assume x in X /\ (Y \/ Z);
then x in X & x in Y \/ Z by Def3;
then x in X & (x in Y or x in Z) by Def2;
then x in X /\ Y or x in X /\ Z by Def3;
hence thesis by Def2;
end;
let x;
assume x in X /\ Y \/ X /\ Z;
then x in X /\ Y or x in X /\ Z by Def2;
then x in X & x in Y or x in X & x in Z by Def3;
then x in X & x in Y \/ Z by Def2;
hence thesis by Def3;
end;
theorem
Th71: X \/ Y /\ Z = (X \/ Y) /\ (X \/ Z)
proof
thus X \/ Y /\ Z c= (X \/ Y) /\ (X \/ Z)
proof let x;
assume x in X \/ Y /\ Z;
then x in X or x in Y /\ Z by Def2;
then x in X or x in Y & x in Z by Def3;
then x in X \/ Y & x in X \/ Z by Def2;
hence thesis by Def3;
end;
let x;
assume x in (X \/ Y) /\ (X \/ Z);
then x in X \/ Y & x in X \/ Z by Def3;
then (x in X or x in Y) & (x in X or x in Z) by Def2;
then x in X or x in Y /\ Z by Def3;
hence thesis by Def2;
end;
theorem
(X /\ Y) \/ (Y /\ Z) \/ (Z /\ X) = (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X)
proof
thus
X /\ Y \/ Y /\ Z \/ Z /\ X
= (X /\ Y \/ Y /\ Z \/ Z) /\ (X /\ Y \/ Y /\ Z \/ X) by Th71
.= (X /\ Y \/ (Y /\ Z \/ Z)) /\ (X /\ Y \/ Y /\ Z \/ X) by Th64
.= (X /\ Y \/ Z) /\ (X /\ Y \/ Y /\ Z \/ X) by Th69
.= (X /\ Y \/ Z) /\ (X /\ Y \/ X \/ Y /\ Z) by Th64
.= (X /\ Y \/ Z) /\ (X \/ Y /\ Z) by Th69
.= (X \/ Z) /\ (Y \/ Z) /\ (X \/ Y /\ Z) by Th71
.= (X \/ Z) /\ (Y \/ Z) /\ ((X \/ Y) /\ (X \/ Z)) by Th71
.= (X \/ Y) /\ ((Y \/ Z) /\ (X \/ Z) /\ (X \/ Z)) by Th67
.= (X \/ Y) /\ ((Y \/ Z) /\ ((X \/ Z) /\ (X \/ Z))) by Th67
.= (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X) by Th67;
end;
canceled;
theorem
Th74: X \ {} = X
proof
now let x;
x in X & not x in {} iff x in X by Def1;
hence x in X \ {} iff x in X by Def4;
end;
hence thesis by TARSKI:2;
end;
theorem
Th75: {} \ X = {}
proof
{} c= X by Th27;
hence thesis by Th45;
end;
theorem
X \ (X \/ Y) = {}
proof
X c= X \/ Y & X c= Y \/ X by Th31;
hence thesis by Th45;
end;
theorem
Th77: X \ X /\ Y = X \ Y
proof
now let x;
x in X & not x in X /\ Y iff x in X & not x in Y by Def3;
hence x in X \ X /\ Y iff x in X \ Y by Def4;
end;
hence X \ X /\ Y = X \ Y by TARSKI:2;
end;
theorem
X \ Y misses Y
proof
not ex x st x in (X \ Y) /\ Y
proof
given x such that A1:x in (X \ Y) /\ Y;
x in X \ Y & x in Y by A1,Def3;
hence contradiction by Def4;
end;
hence (X \ Y) /\ Y = {} by Def1;
end;
theorem
X \/ (Y \ X) = X \/ Y
proof
thus X \/ (Y \ X) c= X \/ Y
proof
let x;
assume x in X \/ (Y \ X);
then x in X or x in Y \ X by Def2;
then x in X or x in Y by Def4;
hence thesis by Def2;
end;
let x;
assume x in X \/ Y;
then x in X or x in Y & not x in X by Def2;
then x in X or x in Y \ X by Def4;
hence thesis by Def2;
end;
theorem
Th80: X /\ Y \/ (X \ Y) = X
proof
thus X /\ Y \/ (X \ Y) c= X
proof
let x;
assume x in X /\ Y \/ (X \ Y);
then x in X /\ Y or x in (X \ Y) by Def2;
hence thesis by Def4,Def3 ;
end;
let x;
assume x in X;
then x in X & x in Y or x in (X\Y) by Def4;
then x in X /\ Y or x in (X \ Y) by Def3;
hence thesis by Def2;
end;
theorem
Th81: X \ (Y \ Z) = (X \ Y) \/ X /\ Z
proof
thus x in X \ (Y \ Z) implies x in (X \ Y) \/ X /\ Z
proof
assume x in X \ (Y \ Z);
then x in X & not x in (Y \ Z) by Def4;
then (x in X & not x in Y) or x in X & x in Z by Def4;
then x in (X \ Y) or x in X /\ Z by Def3,Def4;
hence thesis by Def2;
end;
thus x in (X \ Y) \/ X /\ Z implies x in X \ (Y \ Z)
proof
assume x in (X \ Y) \/ X /\ Z;
then x in (X \ Y) or x in X /\ Z by Def2;
then (x in X & not x in Y) or (x in X & x in Z) by Def3,Def4;
then x in X & not x in (Y \ Z) by Def4;
hence x in X \ (Y \ Z) by Def4;
end;
end;
theorem
X \ (X \ Y) = X /\ Y
proof
thus x in X \ (X \ Y) implies x in X /\ Y
proof
assume x in X \ (X \ Y);
then x in X & not x in (X \ Y) by Def4;
then x in X & (not x in X or x in Y) by Def4;
hence thesis by Def3;
end;
thus x in X /\ Y implies x in X \ (X \ Y)
proof
assume x in X /\ Y;
then x in X & (not x in X or x in Y) by Def3;
then x in X & not x in (X \ Y) by Def4;
hence thesis by Def4;
end;
end;
theorem
(X \/ Y) \ Y = X \ Y
proof
thus x in (X \/ Y) \ Y implies x in X \ Y
proof
assume x in (X \/ Y) \ Y;
then x in (X \/ Y) & not x in Y by Def4;
then (x in X or x in Y) & not x in Y by Def2;
hence thesis by Def4;
end;
thus x in X \ Y implies x in (X \/ Y) \ Y
proof
assume x in X \ Y;
then (x in X or x in Y) & not x in Y by Def4 ;
then x in (X \/ Y) & not x in Y by Def2;
hence thesis by Def4;
end;
end;
theorem
X misses Y iff X \ Y = X
proof
thus X misses Y implies X \ Y = X
proof
assume A1:X /\ Y = {};
thus for x holds x in X \ Y implies x in X by Def4;
let x;
not x in X /\ Y implies not x in X or not x in Y by Def3;
hence x in X implies x in X \ Y by A1,Def1,Def4;
end;
assume
A2: X \ Y = X;
not ex x st x in X /\ Y
proof
given x such that A3: x in X /\ Y;
x in X & x in Y by Def3,A3;
hence contradiction by A2,Def4;
end;
hence thesis by Th2;
end;
theorem
X \ (Y \/ Z) = (X \ Y) /\ (X \ Z)
proof
Y c= Y \/ Z by Th31;
then A1:X \(Y \/ Z) c= X \ Y by Th47;
Z c= Y \/ Z by Th31;
then X \ (Y \/ Z) c= X \ Z by Th47;
hence X \ (Y \/ Z) c= (X \ Y) /\ (X \ Z) by A1,Th39;
let x;
assume x in (X \ Y) /\ (X \ Z);
then x in (X \ Y) & x in (X \ Z) by Def3;
then x in X & (not x in Y & not x in Z) by Def4 ;
then x in X & not x in (Y \/ Z) by Def2;
hence thesis by Def4;
end;
theorem
Th86: X \ (Y /\ Z) = (X \ Y) \/ (X \ Z)
proof
thus X \ (Y /\ Z) c= (X \ Y) \/ (X \ Z)
proof
let x;
assume x in X \ (Y /\ Z);
then x in X & not x in (Y /\ Z) by Def4;
then x in X & (not x in Y or not x in Z) by Def3;
then x in (X \ Y) or x in (X \ Z) by Def4;
hence thesis by Def2;
end;
Y /\ Z c= Y & Y /\ Z c= Z by Th37;
then (X \ Y) c= X \ (Y /\ Z) & X \ Z c= X \ (Y /\ Z) by Th47;
hence (X \ Y) \/ (X \ Z) c= X \ (Y /\ Z) by Th32;
end;
theorem
Th87: (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X)
proof
x in (X \/ Y) \ (X /\ Y) iff x in (X \ Y) \/ (Y \ X)
proof
thus x in (X \/ Y) \ (X /\ Y) implies x in (X \ Y) \/ (Y \ X)
proof
assume x in (X \/ Y) \ (X /\ Y);
then x in (X \/ Y) & not x in (X /\ Y) by Def4;
then (x in X or x in Y) & (not x in X or not x in Y) by Def3,Def2;
then x in (X \ Y) or x in( Y \ X) by Def4;
hence thesis by Def2;
end;
assume x in (X \ Y) \/ (Y \ X);
then x in (X \ Y) or x in (Y \ X) by Def2;
then (x in X & not x in Y) or (x in Y & not x in X) by Def4;
then not x in (X /\ Y) & x in (X \/ Y) by Def3,Def2;
hence thesis by Def4;
end;
hence thesis by TARSKI:2;
end;
theorem
Th88: (X \ Y) \ Z = X \ (Y \/ Z)
proof
thus x in (X \ Y) \ Z implies x in X \ (Y \/ Z)
proof
assume x in (X \ Y) \ Z;
then x in (X \ Y) & not x in Z by Def4;
then x in X & not (x in Y or x in Z) by Def4;
then x in X & not x in (Y \/ Z) by Def2;
hence thesis by Def4 ;
end;
thus x in X \ (Y \/ Z) implies x in (X \ Y) \ Z
proof
assume x in X \ (Y \/ Z);
then x in X & not x in (Y \/ Z) by Def4;
then (x in X & not x in Y) & not x in Z by Def2;
then x in (X \ Y) & not x in Z by Def4;
hence thesis by Def4;
end;
end;
theorem
Th89: (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z)
proof
thus (X \/ Y) \ Z c= (X \ Z) \/ (Y \ Z)
proof
let x;
assume x in (X \/ Y) \ Z;
then x in (X \/ Y) & not x in Z by Def4;
then (x in X & not x in Z) or (x in Y & not x in Z) by Def2 ;
then x in (X \ Z) or x in (Y \ Z) by Def4;
hence thesis by Def2;
end;
let x;
assume x in(( X \ Z) \/ (Y \ Z));
then x in (X \ Z) or x in (Y \ Z) by Def2;
then (x in X & not x in Z) or (x in Y & not x in Z) by Def4;
then x in (X \/ Y) & not x in Z by Def2;
hence thesis by Def4;
end;
theorem
X \ Y = Y \ X implies X = Y
proof
assume A1: X \ Y = Y \ X;
now let x;
(x in X & not x in Y) iff x in Y \ X by Def4,A1;
hence x in X iff x in Y by Def4;
end;
hence thesis by TARSKI:2;
end;
canceled;
theorem
X \+\ {} = X
proof
thus X \+\ {} = (X \ {}) \/ ({} \ X) by Def7
.= X \/ ({} \ X) by Th74
.= X \/ {} by Th75
.= X by Th60;
end;
theorem
X \+\ X = {}
proof
thus X \+\ X = (X \ X) \/ (X \ X) by Def7
.= {} by Th45;
end;
canceled;
theorem
X \/ Y = (X \+\ Y) \/ X /\ Y
proof
thus X \/ Y = ((X \ Y) \/ X /\ Y) \/ Y by Th80
.= (X \ Y) \/ (X /\ Y \/ Y) by Th64
.= (X \ Y) \/ Y by Th69
.= (X \ Y) \/ ((Y \ X) \/ (Y /\ X)) by Th80
.= ((X \ Y) \/ (Y \ X)) \/ Y /\ X by Th64
.= (X \+\ Y) \/ X /\ Y by Def7 ;
end;
theorem
Th96: X \+\ Y = (X \/ Y) \ X /\ Y
proof
thus X \+\ Y = (X \ Y) \/ (Y \ X) by Def7
.= (X \ X /\ Y) \/ (Y \ X) by Th77
.= (X \ X /\ Y) \/ (Y \ X /\ Y) by Th77
.= (X \/ Y) \ X /\ Y by Th89;
end;
theorem
(X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z))
proof
thus (X \+\ Y) \ Z = ((X \ Y) \/ (Y \ X)) \ Z by Def7
.= (X \ Y \ Z) \/ (Y \ X \ Z) by Th89
.= (X \ (Y \/ Z)) \/ (Y \ X \ Z) by Th88
.= (X \ (Y \/ Z)) \/ (Y \ (X \/ Z)) by Th88;
end;
theorem
X \ (Y \+\ Z) = X \ (Y \/ Z) \/ X /\ Y /\ Z
proof
thus X \ (Y \+\ Z) = X \ ((Y \/ Z) \ Y /\ Z) by Th96
.= X \ (Y \/ Z) \/ X /\ (Y /\ Z) by Th81
.= X \ (Y \/ Z) \/ X /\ Y /\ Z by Th67;
end;
theorem
(X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
proof
set S1 = X \ (Y \/ Z), S2 = Y \ (X \/ Z),
S3 = Z \ (X \/ Y), S4 = X /\ Y /\ Z;
thus (X \+\ Y) \+\ Z = ((X \ Y) \/ (Y \ X)) \+\ Z by Def7
.= (((X \ Y) \/ (Y \ X)) \ Z) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Def7
.= (((X \ Y) \ Z) \/ ((Y \ X) \ Z)) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Th89
.= ( S1 \/ ((Y \ X) \ Z)) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Th88
.= ( S1 \/ S2) \/ (Z \ ((X \ Y) \/ (Y \ X))) by Th88
.= ( S1 \/ S2) \/ (Z \ ((X \/ Y) \ (X /\ Y))) by Th87
.= (S1 \/ S2) \/ (S4 \/ S3) by Th81
.= (S1 \/ S2 \/ S4) \/ S3 by Th64
.= (S1 \/ S4 \/ S2) \/ S3 by Th64
.= (S1 \/ S4) \/ (S2 \/ S3) by Th64
.= (S1 \/ X /\ (Y /\ Z)) \/ (S2 \/ S3) by Th67
.= X \ ((Y \/ Z) \ (Y /\ Z)) \/ (S2 \/ S3) by Th81
.= X \ ((Y \ Z) \/ (Z \ Y)) \/ (S2 \/ (Z \ (Y \/ X))) by Th87
.= X \ ((Y \ Z) \/ (Z \ Y)) \/ ((Y \ (Z \/ X)) \/ (Z \ Y \ X)) by Th88
.= X \ ((Y \ Z) \/ (Z \ Y)) \/ ((Y \ Z \ X) \/ (Z \ Y \ X)) by Th88
.= X \ ((Y \ Z) \/ (Z \ Y)) \/ (((Y \ Z) \/ (Z \ Y)) \ X) by Th89
.= X \+\ ((Y \ Z) \/ (Z \ Y)) by Def7
.= X \+\ (Y \+\ Z) by Def7;
end;
::
:: 2.3 "meets" and "misses"
::
theorem
Th100: X meets Y \/ Z iff X meets Y or X meets Z
proof
thus X meets Y \/ Z implies X meets Y or X meets Z
proof
assume X meets Y \/ Z;
then consider x such that A1:x in X and
A2:x in Y \/ Z by Th1;
x in X & x in Y or x in X & x in Z by A1,A2,Def2;
hence thesis by Th1;
end;
A3: X meets Y implies X meets Y \/ Z
proof assume X meets Y;
then consider x such that A4:x in X & x in Y by Th1;
x in X & x in Y \/ Z by Def2,A4;
hence thesis by Th1;
end;
X meets Z implies X meets Y \/ Z
proof assume X meets Z;
then consider x such that A5:x in X & x in Z by Th1;
x in X & x in Y \/ Z by Def2,A5;
hence thesis by Th1;
end;
hence thesis by A3;
end;
theorem
X meets Y & Y c= Z implies X meets Z
proof assume X meets Y;
then consider x such that A1: x in X & x in Y by Th1;
assume Y c= Z;
then x in Z by A1,TARSKI: def 3;
hence thesis by A1,Th1;
end;
theorem
X meets Y /\ Z implies X meets Y
proof assume X meets Y /\ Z;
then consider x such that A1: x in X & x in Y /\ Z by Th1;
x in X & x in Y by A1,Def3;
hence thesis by Th1;
end;
canceled;
theorem
X misses {}
proof
assume X meets {};
then ex x st x in X & x in {} by Th1;
hence contradiction by Def1;
end;
canceled 5;
theorem
X meets X iff X <> {}
proof
hereby assume X meets X;
then ex x st x in X & x in X by Th1;
hence X <> {} by Def1;
end;
assume X <> {};
then X /\ X <> {};
hence thesis by Def5;
end;
theorem
Th111: X /\ Y misses X \ Y
proof
now let x;
not(x in X & x in Y & not x in Y);
hence not (x in X /\ Y & x in X \ Y) by Def3,Def4;
end;
hence thesis by Th1;
end;
theorem
X /\ Y misses X \+\ Y
proof
X /\ Y misses X \ Y & X /\ Y misses Y \ X by Th111;
then X /\ Y misses (X \ Y) \/ (Y \ X) by Th100;
hence thesis by Def7;
end;
theorem
X meets Y \ Z implies X meets Y
proof assume X meets Y \ Z;
then consider x such that A1:x in X & x in Y \ Z by Th1;
x in X & x in Y by Def4,A1;
hence thesis by Th1;
end;
theorem
X c= Y & X c= Z & Y misses Z implies X = {}
proof
assume that A1: X c= Y and
A2: X c= Z and
A3: Y misses Z;
thus X c= {}
proof let x;
assume x in X;
then x in Y & x in Z by A1,A2,TARSKI:def 3;
hence x in {} by A3,Th1;
end;
thus thesis by Th27;
end;
::
:: ADDITIONAL THEOREMS
::
theorem
X \ Y c= Z & Y \ X c= Z implies X \+\ Y c= Z
proof
assume X \ Y c= Z & Y \ X c= Z;
then (X \ Y) \/ (Y \ X) c= Z by Th32;
hence thesis by Def7;
end;
theorem
Th116: X /\ (Y \ Z) = (X /\ Y) \ Z
proof
now
let x;
x in X & x in Y & not x in Z iff x in X & x in Y & not x in Z;
then x in X & x in (Y \ Z) iff x in (X /\ Y) & not x in Z by Def4,Def3;
hence x in X /\ (Y \ Z) iff x in (X /\ Y) \ Z by Def3,Def4;
end;
hence thesis by TARSKI:2;
end;
theorem
X /\ (Y \ Z) = X /\ Y \ X /\ Z
proof
A1: X /\ Y c= X by Th37;
X /\ Y \ X /\ Z = ((X /\ Y) \ X) \/ ((X /\ Y) \ Z) by Th86
.= {} \/ ((X /\ Y) \ Z) by A1,Th45
.= (X /\ Y) \ Z by Th60;
hence X /\ (Y \ Z) = X /\ Y \ X /\ Z by Th116;
end;
canceled 2;
theorem
X c= Y \/ Z & X misses Z implies X c= Y
proof
assume that A1: X c= Y \/ Z and
A2: X /\ Z = {};
X /\ (Y \/ Z)= X by Th42,A1;
then Y /\ X \/ {} = X by A2,Th70;
then Y /\ X = X by Th60;
hence thesis by Th37;
end;
begin :: Addendum, 2000.01.10, A.T.
definition let X,Y;
pred X c< Y means
:Def9: X c= Y & X <> Y;
irreflexivity;
end;
theorem
X c< Y & Y c= Z implies X c< Z
proof assume that
A1: X c< Y and
A2: Y c= Z;
X c= Y by A1,Def9;
hence X c= Z & X <> Z by A2,Th29,A1,Def8;
end;
theorem Th122:
X c= Y & Y c< Z implies X c< Z
proof assume that
A1: X c= Y and
A2: Y c< Z;
Y c= Z by A2,Def9;
hence X c= Z & X <> Z by A1,Th29,A2,Def8;
end;
theorem
X c< Y & Y c< Z implies X c< Z
proof assume that
A1: X c< Y and
A2: Y c< Z;
X c= Y by Def9,A1;
hence thesis by A2,Th122;
end;
theorem
X <> {} implies {} c< X
proof assume
A1: X <> {};
thus {} c= X by Th27;
thus thesis by A1;
end;
theorem
not ex X st X c< {}
proof given X such that
A1: X c< {};
X c= {} by A1,Def9;
hence contradiction by A1,Th30;
end;
theorem
not ex X,Y st X c< Y & Y c< X
proof given X,Y such that
A1: X c< Y & Y c< X;
X c= Y & Y c= X by A1,Def9;
hence contradiction by A1,Def8;
end;
theorem
X c= Y implies not Y c< X
proof assume X c= Y & Y c= X & X <> Y;
hence contradiction by Def8;
end;