• Axioms
• Subsets
• Union of Sets
• Intersection of Sets

                 :::::::::::::::::::::::::::::::::::::
                 :: Written by Michal Trybulec 2007 ::
                 :::::::::::::::::::::::::::::::::::::

environ

:: Everything is a set:
type set;

:: A set is an element of another set:
pred set in set;
:: A set is a subset of another set:
pred set subset_of set;
:: A set is the union of two other sets:
pred set union_of set, set;
:: A set is the intersection of two other sets:
pred set inter_of set, set;

reserve x, y, z, A, B, C for set;

:: The empty set is a set with no elements in it:
given empty being set such that
AxEmpty:
  not ex x st x in empty;

:: Two sets are equal if exactly the same elements are in both sets:
AxEquality:
for A, B holds
  A = B iff
    for x holds x in A iff x in B;

:: A set is a subset of another set
:: if all its elements are also in the other set:
AxSubset:
for A, B holds
  A subset_of B iff
    for x st x in A holds x in B;

:: A set is the union of two sets if each of its elements
:: is in one of those two sets:
AxUnion:
for A, B, C holds
  A union_of B, C iff
    for x holds x in A iff x in B or x in C;

:: A set is the intersection of two sets if each of its elements
:: is in both of those two sets:
AxInter:
for A, B, C holds
  A inter_of B, C iff
    for x holds x in A iff x in B & x in C;

begin

                 :::::::::::::::::::::::::::::::::::::
                 ::             Subsets             ::
                 :::::::::::::::::::::::::::::::::::::
                 
:: The empty set is a subset of all sets.
:: {} c= A;
ThSubset10:
for A holds empty subset_of A
proof
  let A;
  now
    let x;
    assume x in empty;
    hence x in A by AxEmpty;
  end;
  hence thesis by AxSubset;
end;

:: A set is a subset of itself (reflexivity of the subset relation).
:: A c= A;
ThSubset20:
for A holds A subset_of A
proof
  let A;
  now
    let x;
    assume x in A;
    hence x in A;
  end;
  hence thesis by AxSubset;
end;

:: If B is a subset of A, and C is a subset of B,
:: then C is a subset of A (transitivity of the subset relation).
:: A c= B & B c= C implies A c= C;
ThSubset30:
for A, B, C st C subset_of B & B subset_of A holds C subset_of A
proof
  let A, B, C;
  assume
A:  C subset_of B & B subset_of A;
BA:
  for x st x in B holds x in A by A, AxSubset;
CB:
  for x st x in C holds x in B by A, AxSubset;
  now
    let x;
    assume x in C;
    then x in B by CB, AxSubset;
    hence x in A by BA, AxSubset;
  end;
  hence thesis by AxSubset;
end;

:: If two sets are each other's subsets, then they are equal
:: (antisymmetry of the subset relation).
:: A c= B & B c= A iff A = B;
ThSubset40:
for A, B holds A subset_of B & B subset_of A iff A = B
proof
  let A, B;
  thus A subset_of B & B subset_of A implies A = B
  proof
    assume
A:    A subset_of B & B subset_of A;
BA: for x st x in B holds x in A by A, AxSubset;
AB: for x st x in A holds x in B by A, AxSubset;
    now
      let x;
      thus x in A iff x in B by AB, BA;
    end;
    hence thesis by AxEquality;
  end;
  assume A = B;
  then
A:  for x holds x in A iff x in B by AxEquality;
AB:
  now
    let x;
    thus x in A implies x in B by A;
  end;
BA:
  now
    let x;
    thus x in B implies x in A by A;
  end;
  thus thesis by AB, BA, AxSubset;
end;

:: If a set is a subset of the empty set, it is itself empty.
:: A c= {} implies A = {};
ThSubset50:
for A st A subset_of empty holds A = empty
proof
  let A;
  assume
A:  A subset_of empty;
  empty subset_of A by ThSubset10;
  hence thesis by A, ThSubset40;
end;

                 :::::::::::::::::::::::::::::::::::::
                 ::              Union              ::
                 :::::::::::::::::::::::::::::::::::::

:: The union of a set with itself is the set itself.
:: A \/ A = A;
ThUnion10:
for A holds A union_of A, A
proof
  let A;
  now
    let x;
    thus x in A iff x in A or x in A;
  end;
  hence thesis by AxUnion;
end;

:: The order of the sets in the union is irrelevant
:: (commutativity of the union function).
:: A \/ B = B \/ A;
ThUnion20:
for A, B, C st C union_of A, B holds C union_of B, A
proof
  let A, B, C;
  assume C union_of A, B;
  then
A:  for x holds x in C iff x in A or x in B by AxUnion;
  now
    let x;
    thus x in C iff x in B or x in A by A;
  end;
  hence thesis by AxUnion;
end;

:: The union of a set with its subset is the set itself.
:: A c= B implies A \/ B = B;
ThUnion30:
for A, B st A subset_of B holds B union_of A, B
proof
  let A, B;
  assume A subset_of B;
  then
A:  for x st x in A holds x in B by AxSubset;
  now
    let x;
    thus x in B iff x in A or x in B by A;
  end;
  hence thesis by AxUnion;
end;

:: The union of a set and the empty set is the set itself.
:: {} \/ A = A;
ThUnion40:
for A holds A union_of empty, A
proof
  let A;
  empty subset_of A by ThSubset10;
  hence thesis by ThUnion30;
end;

:: If the union of two sets is empty, then both sets are empty.
:: {} = A \/ B implies A = {};
ThUnion50:
for A, B st empty union_of A, B holds A = empty
proof
  let A, B;
  assume empty union_of A, B;
  then
A:  for x holds x in empty iff x in A or x in B by AxUnion;
  now
    let x;
    assume x in A;
    hence x in empty by A;
  end;
  then
B:  A subset_of empty by AxSubset;
  empty subset_of A by ThSubset10;
  hence thesis by B, ThSubset40;
end;

:: Transitivity of the union function.
:: (A \/ B) \/ C = A \/ (B \/ C);
ThUnion60:
for A, B, C, AB, BC, D being set st
  AB union_of A, B & BC union_of B, C holds
    D union_of AB, C iff D union_of A, BC
proof
  let A, B, C, AB, BC, D be set;
  assume
A:  AB union_of A, B & BC union_of B, C;
AB:
  for x holds x in AB iff x in A or x in B by A, AxUnion;
BC:
  for x holds x in BC iff x in B or x in C by A, AxUnion;
  thus D union_of AB, C implies D union_of A, BC
  proof
    assume D union_of AB, C;
    then
DAB:  for x holds x in D iff x in AB or x in C by AxUnion;
    now
      let x;
      x in D iff x in AB or x in C by DAB;
      then x in D iff x in A or x in B or x in C by AB;
      hence x in D iff x in A or x in BC by BC;
    end;
    hence thesis by AxUnion;
  end;
  assume D union_of A, BC;
  then
DBC:
  for x holds x in D iff x in A or x in BC by AxUnion;
  now
    let x;
    x in D iff x in A or x in BC by DBC;
    then x in D iff x in A or x in B or x in C by BC;
    hence x in D iff x in AB or x in C by AB;
  end;
  hence thesis by AxUnion;
end;

:: A \/ B = A \/ (A \/ B):
ThUnion70:
for A, B, AB, AAB being set st
  AB union_of A, B & AAB union_of A, AB holds
    AB = AAB
proof
  let A, B, AB, AAB be set;
  assume
A:  AB union_of A, B & AAB union_of A, AB;
AB:
  for x holds x in AB iff x in A or x in B by A, AxUnion;
AAB:
  for x holds x in AAB iff x in A or x in AB by A, AxUnion;
  for x holds x in AB iff x in AAB
  proof
    let x;
    thus x in AB implies x in AAB by AAB;
    assume x in AAB;
    then x in A or x in AB by AAB;
    hence thesis by AB;
  end;
  hence thesis by AxEquality;
end;

:: Both arguments of the union function are subsets of the result.
:: A \/ B = C implies A c= C;
ThUnion80:
for A, B, C st C union_of A, B holds A subset_of C
proof
  let A, B, C;
  assume C union_of A, B;
  then
A:  for x holds x in C iff x in A or x in B by AxUnion;
  now
    let x;
    assume x in A;
    hence x in C by A;
  end;
  hence thesis by AxSubset;
end;

:: The union of two subsets of a set is too a subset of this set.
:: A c= C & B c= C implies A \/ B c= C;
ThUnion90:
for A, B, C, AB being set st
  AB union_of A, B & A subset_of C & B subset_of C holds
    AB subset_of C
proof
  let A, B, C, AB be set;
  assume
A:  AB union_of A, B & A subset_of C & B subset_of C;
AB:
  for x holds x in AB iff x in A or x in B by A, AxUnion;
AC:
  for x st x in A holds x in C by A, AxSubset;
BC:
  for x st x in B holds x in C by A, AxSubset;
  now
    let x;
    assume x in AB;
    then x in A or x in B by AB;
    hence x in C by AC, BC;
  end;
  hence thesis by AxSubset;
end;

                 :::::::::::::::::::::::::::::::::::::
                 ::          Intersection           ::
                 :::::::::::::::::::::::::::::::::::::


:: The intersection of a set with itself is the set itself.
:: A /\ A = A;
ThInter10:
for A holds A inter_of A, A
proof
  let A;
  now
    let x;
    thus x in A iff x in A & x in A;
  end;
  hence thesis by AxInter;
end;

:: The order of the sets in the intersection is irrelevant
:: (commutativity of the intersection function).
:: A /\ B = B /\ A;
ThInter20:
for A, B, C st C inter_of A, B holds C inter_of B, A
proof
  let A, B, C;
  assume C inter_of A, B;
  then
A:  for x holds x in C iff x in A & x in B by AxInter;
  now
    let x;
    thus x in C iff x in B & x in A by A;
  end;
  hence thesis by AxInter;
end;

:: The intersection of a set with its subset is the subset.
:: A c= B implies A /\ B = A;
ThInter30:
for A, B st A subset_of B holds A inter_of A, B
proof
  let A, B;
  assume A subset_of B;
  then
A:  for x st x in A holds x in B by AxSubset;
  now
    let x;
    thus x in A iff x in A & x in B by A;
  end;
  hence thesis by AxInter;
end;

:: The intersection of a set and the empty set is empty.
:: {} /\ A = {};
ThInter40:
for A holds empty inter_of empty, A
proof
  let A;
  empty subset_of A by ThSubset10;
  hence thesis by ThInter30;
end;

:: Transitivity of the intersection function.
:: (A /\ B) /\ C = A /\ (B /\ C);
ThInter60:
for A, B, C, AB, BC, D being set st
  AB inter_of A, B & BC inter_of B, C holds
    D inter_of AB, C iff D inter_of A, BC
proof
  let A, B, C, AB, BC, D be set;
  assume
A:  AB inter_of A, B & BC inter_of B, C;
AB:
  for x holds x in AB iff x in A & x in B by A, AxInter;
BC:
  for x holds x in BC iff x in B & x in C by A, AxInter;
  thus D inter_of AB, C implies D inter_of A, BC
  proof
    assume D inter_of AB, C;
    then
DAB:  for x holds x in D iff x in AB & x in C by AxInter;
    now
      let x;
      x in D iff x in AB & x in C by DAB;
      then x in D iff x in A & x in B & x in C by AB;
      hence x in D iff x in A & x in BC by BC;
    end;
    hence thesis by AxInter;
  end;
  assume D inter_of A, BC;
  then
DBC:
  for x holds x in D iff x in A & x in BC by AxInter;
  now
    let x;
    x in D iff x in A & x in BC by DBC;
    then x in D iff x in A & x in B & x in C by BC;
    hence x in D iff x in AB & x in C by AB;
  end;
  hence thesis by AxInter;
end;

:: A /\ B = A /\ (A /\ B):
ThInter70:
for A, B, AB, AAB being set st
  AB inter_of A, B & AAB inter_of A, AB holds
    AB = AAB
proof
  let A, B, AB, AAB be set;
  assume
A:  AB inter_of A, B & AAB inter_of A, AB;
AB:
  for x holds x in AB iff x in A & x in B by A, AxInter;
AAB:
  for x holds x in AAB iff x in A & x in AB by A, AxInter;
  for x holds x in AB iff x in AAB
  proof
    let x;
    thus x in AB implies x in AAB
    proof
      assume
C:      x in AB;
      then x in A & x in B by AB;
      hence thesis by C, AAB;
    end;
    assume x in AAB;
    then x in A & x in AB by AAB;
    hence thesis by AB;
  end;
  hence thesis by AxEquality;
end;

:: Both arguments of the intersection function are supersets of the result.
:: A /\ B = C implies C c= A;
ThInter80:
for A, B, C st C inter_of A, B holds C subset_of A
proof
  let A, B, C;
  assume C inter_of A, B;
  then
A:  for x holds x in C iff x in A & x in B by AxInter;
  now
    let x;
    assume x in C;
    hence x in A by A;
  end;
  hence thesis by AxSubset;
end;

:: The intersection of two supersets of a set is too a superset of this set.
:: C c= A & C c= B implies C c= A /\ B;
ThInter90:
for A, B, C, AB being set st
  AB inter_of A, B & C subset_of A & C subset_of B holds
    C subset_of AB
proof
  let A, B, C, AB be set;
  assume
A:  AB inter_of A, B & C subset_of A & C subset_of B;
AB:
  for x holds x in AB iff x in A & x in B by A, AxInter;
AC:
  for x st x in C holds x in A by A, AxSubset;
BC:
  for x st x in C holds x in B by A, AxSubset;
  now
    let x;
    assume x in C;
    then x in A & x in B by AC, BC;
    hence x in AB by AB;
  end;
  hence thesis by AxSubset;
end;

:: Distributiveness of intersection over union:
:: A /\ (B \/ C) = (A /\ B) \/ (A /\ C);
for A, B, C, BuC, AiB, AiC, AiBuC, AuBiAuC being set st
  AiBuC inter_of A, BuC & BuC union_of B, C &
    AuBiAuC union_of AiB, AiC & AiB inter_of A, B & AiC inter_of A, C holds
      AiBuC = AuBiAuC
proof
  let A, B, C, BuC, AiB, AiC, AiBuC, AiBuAiC be set such that
A:  AiBuC inter_of A, BuC & BuC union_of B, C &
      AiBuAiC union_of AiB, AiC & AiB inter_of A, B & AiC inter_of A, C;

AiBuC:
  for x holds x in AiBuC iff x in A & x in BuC by A, AxInter;
BuC:
  for x holds x in BuC iff x in B or x in C by A, AxUnion;
AiBuAiC:
  for x holds x in AiBuAiC iff x in AiB or x in AiC by A, AxUnion;
AiB:
  for x holds x in AiB iff x in A & x in B by A, AxInter;
AiC:
  for x holds x in AiC iff x in A & x in C by A, AxInter;

  for x holds x in AiBuC iff x in AiBuAiC
  proof
    let x;
    thus x in AiBuC implies x in AiBuAiC
    proof
      assume x in AiBuC;
      then x in A & x in BuC by AiBuC;
      then x in A & (x in B or x in C) by BuC;
      then x in A & x in B or x in A & x in C;
      then x in AiB or x in A & x in C by AiB;
      then x in AiB or x in AiC by AiC;
      hence thesis by AiBuAiC;
    end;
    assume x in AiBuAiC;
    then x in AiB or x in AiC by AiBuAiC;
    then x in AiB or x in A & x in C by AiC;
    then x in A & x in B or x in A & x in C by AiB;
    then x in A & (x in B or x in C);
    then x in A & x in BuC by BuC;
    hence thesis by AiBuC;
  end;
  hence thesis by AxEquality;
end;

:: Distributiveness of union over intersection:
:: A \/ (B /\ C) = (A \/ B) /\ (A \/ C);
for A, B, C, BiC, AuB, AuC, AuBiC, AuBiAuC being set st
  AuBiC union_of A, BiC & BiC inter_of B, C &
    AuBiAuC inter_of AuB, AuC & AuB union_of A, B & AuC union_of A, C holds
      AuBiC = AuBiAuC
proof
  let A, B, C, BiC, AuB, AuC, AuBiC, AuBiAuC be set such that
A:  AuBiC union_of A, BiC & BiC inter_of B, C &
      AuBiAuC inter_of AuB, AuC & AuB union_of A, B & AuC union_of A, C;

AuBiC:
  for x holds x in AuBiC iff x in A or x in BiC by A, AxUnion;
BiC:
  for x holds x in BiC iff x in B & x in C by A, AxInter;
AuBiAuC:
  for x holds x in AuBiAuC iff x in AuB & x in AuC by A, AxInter;
AuB:
  for x holds x in AuB iff x in A or x in B by A, AxUnion;
AuC:
  for x holds x in AuC iff x in A or x in C by A, AxUnion;

  for x holds x in AuBiC iff x in AuBiAuC
  proof
    let x;
    thus x in AuBiC implies x in AuBiAuC
    proof
      assume x in AuBiC;
      then x in A or x in BiC by AuBiC;
      then x in A or (x in B & x in C) by BiC;
      then (x in A or x in B) & (x in A or x in C);
      then x in AuB & (x in A or x in C) by AuB;
      then x in AuB & x in AuC by AuC;
      hence thesis by AuBiAuC;
    end;
    assume x in AuBiAuC;
    then x in AuB & x in AuC by AuBiAuC;
    then x in AuB & (x in A or x in C) by AuC;
    then (x in A or x in B) & (x in A or x in C) by AuB;
    then x in A or (x in B & x in C);
    then x in A or x in BiC by BiC;
    hence thesis by AuBiC;
  end;
  hence thesis by AxEquality;
end;