The Mizar article:

Boolean Properties of Sets

by
Zinaida Trybulec, and
Halina Swieczkowska

Received January 6, 1989

Copyright (c) 1989 Association of Mizar Users

MML identifier: BOOLE
[ MML identifier index ]


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;

Back to top