The Mizar article:

Boolean Properties of Sets --- Definitions

by
Library Committee

Received April 6, 2002

Copyright (c) 2002 Association of Mizar Users

MML identifier: XBOOLE_0
[ MML identifier index ]


environ

 vocabulary TARSKI, BOOLE, ZFMISC_1;
 notation TARSKI;
 constructors TARSKI;
 theorems TARSKI;
 schemes TARSKI;

begin

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

scheme Separation { A()-> set, P[set] } :
   ex X being set st for x being set holds x in X iff x in A() & P[x]
 proof
   defpred Q[set,set] means $1 = $2 & P[$2];
A1: for x,y,z st Q[x,y] & Q[x,z] holds y = z;
   consider X such that
A2: for x holds x in X iff ex y st y in A() & Q[y,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 being set st x in it;
  existence
    proof
      consider X;
      defpred P[set] means contradiction;
      consider Y such that
A1:    x in Y iff x in X & P[x] from Separation;
     take Y;
     thus thesis by A1;
    end;
  uniqueness
    proof
     let X,Y;
     assume (not ex x st x in X) & (not ex x st x in Y);
      then x in Y iff x in X;
     hence thesis by TARSKI:2;
    end;

 let X,Y be set;
  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
A2:   X0 = X or X0 = Y and
A3:   x in X0;
       X0 in {X,Y} by A2,TARSKI:def 2;
    hence x in union {X,Y} by A3,TARSKI:def 4;
   end;
  uniqueness
   proof
    let A1, A2 be set such that
A4:  x in A1 iff x in X or x in Y and
A5:  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 A4;
      hence x in A1 iff x in A2 by A5;
     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
   proof defpred P[set] means $1 in Y;
     thus ex Z being set st for x holds x in Z iff x in X & P[x]
       from Separation;
   end;
  uniqueness
   proof
    let A1, A2 be set such that
A6:  x in A1 iff x in X & x in Y and
A7:  x in A2 iff x in X & x in Y;
       now
      let x;
         x in A1 iff x in X & 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
:Def4:   x in it iff x in X & not x in Y;
  existence
   proof defpred P[set] means not $1 in Y;
     thus ex Z being set st for x holds x in Z iff x in X & P[x]
       from Separation;
   end;
  uniqueness
   proof
    let A1, A2 be set such that
A8: x in A1 iff x in X & not x in Y and
A9: 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 A8;
      hence x in A1 iff x in A2 by A9;
     end;
    hence A1 = A2 by TARSKI:2;
   end;
end;

definition let X be set;
 attr X is empty means
:Def5:    X = {};

 let Y be set;
 func X \+\ Y -> set equals
:Def6:  (X \ Y) \/ (Y \ X);
 correctness;
 commutativity;

 pred X misses Y means :Def7:
   X /\ Y = {};
  symmetry;
  antonym X meets Y;

 pred X c< Y means
    X c= Y & X <> Y;
 irreflexivity;

 pred X,Y are_c=-comparable means
    X c= Y or Y c= X;
 reflexivity;
 symmetry;
 redefine pred X = Y means
    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
    x in X \+\ Y iff not (x in X iff x in Y)
proof
    X \+\ Y = (X \ Y) \/ (Y \ X) by Def6;
  then x in X \+\ Y iff x in X \ Y or x in Y \ X by Def2;
  hence thesis by Def4;
end;

theorem :: BOOLE'25:
    (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 Def6;
  end;
  hence thesis by TARSKI:2;
end;



definition
 cluster {} -> empty;
  coherence by Def5;
 cluster empty set;
  existence
   proof {} is empty by Def5; hence thesis; end;
 cluster non empty set;
  existence
   proof consider x;
      x in {x} by TARSKI:def 1;
    then {x} <> {} by Def1;
    then {x} is non empty by Def5;
    hence thesis;
   end;
end;

definition let D be non empty set, X be set;
  cluster D \/ X -> non empty;
  coherence
  proof
    consider x being set such that
A1: x in D by Def1;
      x in D \/ X by A1,Def2;
    then D \/ X <> {} by Def1;
    hence thesis by Def5;
  end;
  cluster X \/ D -> non empty;
  coherence
  proof
    consider x being set such that
A2: x in D by Def1;
      x in X \/ D by A2,Def2;
    then X \/ D <> {} by Def1;
    hence thesis by Def5;
  end;
end;

theorem Th3: :: BOOLE'1:
  X meets Y iff ex x st x in X & x in Y
proof
 hereby assume X meets Y;
  then X /\ Y <> {} by Def7;
  then consider x such that
A1: x in X /\ Y by Def1;
  take x;
  thus x in X & x in Y by A1,Def3;
 end;
 given x such that
A2: x in X & x in Y;
    x in X /\ Y by A2,Def3;
  then X /\ Y <> {} by Def1;
 hence thesis by Def7;
end;

theorem :: BOOLE'2:
    X meets Y iff ex x st x in X /\ Y
proof
 hereby assume X meets Y;
  then X /\ Y <> {} by Def7;
  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 Def7;
end;

theorem :: SYSREL'1:
    X misses Y & x in X \/ Y implies
    ((x in X & not x in Y) or (x in Y & not x in X))
      by Def2,Th3;

scheme Extensionality { X,Y() -> set, P[set] } :
  X() = Y() provided
A1:  for x holds x in X() iff P[x] and
A2:  for x holds x in Y() iff P[x]
  proof
A3:  x in X() implies x in Y()
     proof assume x in X(); then P[x] by A1; hence x in Y() by A2; end;
      x in Y() implies x in X()
     proof assume x in Y(); then P[x] by A2; hence x in X() by A1; end;
   hence thesis by A3,TARSKI:2;
  end;

scheme SetEq { P[set] } :
  for X1,X2 being set st
   (for x being set holds x in X1 iff P[x]) &
   (for x being set holds x in X2 iff P[x]) holds X1 = X2
proof defpred p[set] means P[$1];
  let X1,X2 be set such that
  A1: for x being set holds x in X1 iff p[x] and
  A2: for x being set holds x in X2 iff p[x];
  thus thesis from Extensionality(A1,A2);
end;


Back to top