The abstract of the Mizar article:

Properties of Subsets

by

Zinaida Trybulec

Received March 4, 1989

MML identifier: SUBSET_1

[ Mizar article, MML identifier index ]

environ

 vocabulary BOOLE, SUBSET_1, NEWTON;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1;
 constructors TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1;
 clusters XBOOLE_0;
 requirements BOOLE;


begin

reserve E,X,x,y for set;

definition let X be set;
 cluster bool X -> non empty;
end;

definition let x;
 cluster { x } -> non empty;
  let y;
 cluster { x, y } -> non empty;
end;

definition let X;
 canceled;

 mode Element of X means
:: SUBSET_1:def 2
 it in X if X is non empty
   otherwise it is empty;
end;

definition let X;
 mode Subset of X is Element of bool X;
end;

definition let X be non empty set;
  cluster non empty Subset of X;
end;

definition let X1,X2 be non empty set;
  cluster [: X1,X2 :] -> non empty;
end;

definition let X1,X2,X3 be non empty set;
  cluster [: X1,X2,X3 :] -> non empty;
end;

definition let X1,X2,X3,X4 be non empty set;
  cluster [: X1,X2,X3,X4 :] -> non empty;
end;

definition let D be non empty set, X be non empty Subset of D;
 redefine mode Element of X -> Element of D;
end;

definition let E;
   cluster empty Subset of E;
 end;

definition let E;
  func {} E -> empty Subset of E equals
:: SUBSET_1:def 3
   {};
   func [#] E -> Subset of E equals
:: SUBSET_1:def 4
E;
  end;

canceled 3;

theorem :: SUBSET_1:4
  {} is Subset of X;

 reserve A,B,C for Subset of E;

canceled 2;

theorem :: SUBSET_1:7
 (for x being Element of E holds x in A implies x in B) implies A c= B;

theorem :: SUBSET_1:8
(for x being Element of E holds x in A iff x in B) implies A = B;

canceled;

theorem :: SUBSET_1:10
    A <> {} implies ex x being Element of E st x in A;

definition let E,A;
  func A` -> Subset of E equals
:: SUBSET_1:def 5
E \ A;
   involutiveness;
  let B;
  redefine func A \/ B -> Subset of E;
  func A /\ B -> Subset of E;
  func A \ B -> Subset of E;
  func A \+\ B -> Subset of E;
 end;

canceled 4;

theorem :: SUBSET_1:15
  (for x being Element of E holds x in A iff x in B or x in C)
                                           implies A = B \/ C;

theorem :: SUBSET_1:16
  (for x being Element of E holds x in A iff x in B & x in C)
                                           implies A = B /\ C;

theorem :: SUBSET_1:17
  (for x being Element of E holds x in A iff x in B & not x in C)
                                           implies A = B \ C;

theorem :: SUBSET_1:18
  (for x being Element of E holds x in A iff not(x in B iff x in C))
                                     implies A = B \+\ C;

canceled 2;

theorem :: SUBSET_1:21
  {} E = ([#] E)`;

theorem :: SUBSET_1:22
  [#] E = ({} E)`;

canceled 2;

theorem :: SUBSET_1:25
 A \/ A` = [#]E;

theorem :: SUBSET_1:26
  A misses A`;

canceled;

theorem :: SUBSET_1:28
    A \/ [#]E = [#]E;

theorem :: SUBSET_1:29
    (A \/ B)` = A` /\ B`;

theorem :: SUBSET_1:30
    (A /\ B)` = A` \/ B`;

theorem :: SUBSET_1:31
 A c= B iff B` c= A`;

theorem :: SUBSET_1:32
   A \ B = A /\ B`;

theorem :: SUBSET_1:33
    (A \ B)` = A` \/ B;

theorem :: SUBSET_1:34
    (A \+\ B)` = A /\ B \/ A` /\ B`;

theorem :: SUBSET_1:35
   A c= B` implies B c= A`;

theorem :: SUBSET_1:36
   A` c= B implies B` c= A;

canceled;

theorem :: SUBSET_1:38
   A c= A` iff A = {}E;

theorem :: SUBSET_1:39
   A` c= A iff A = [#]E;

theorem :: SUBSET_1:40
   X c= A & X c= A` implies X = {};

theorem :: SUBSET_1:41
   (A \/ B)` c= A`;

theorem :: SUBSET_1:42
   A` c= (A /\ B)`;

theorem :: SUBSET_1:43
 A misses B iff A c= B`;

theorem :: SUBSET_1:44
   A misses B` iff A c= B;

canceled;

theorem :: SUBSET_1:46
   A misses B & A` misses B` implies A = B`;

theorem :: SUBSET_1:47
   A c= B & C misses B implies A c= C`;

 ::
 ::                 ADDITIONAL THEOREMS
 ::

theorem :: SUBSET_1:48
  (for a being Element of A holds a in B) implies A c= B;

theorem :: SUBSET_1:49
  (for x being Element of E holds x in A) implies E = A;

theorem :: SUBSET_1:50
  E <> {} implies for B for x being Element of E st not x in B holds x in B`;

theorem :: SUBSET_1:51
 for A,B st for x being Element of E holds x in A iff not x in B
  holds A = B`;

theorem :: SUBSET_1:52
   for A,B st for x being Element of E holds not x in A iff x in B
  holds A = B`;

theorem :: SUBSET_1:53
   for A,B st for x being Element of E holds not(x in A iff x in B)
  holds A = B`;

theorem :: SUBSET_1:54
    x in A` implies not x in A;

  reserve x1,x2,x3,x4,x5,x6,x7,x8 for Element of X;

theorem :: SUBSET_1:55
    X <> {} implies {x1} is Subset of X;

theorem :: SUBSET_1:56
    X <> {} implies {x1,x2} is Subset of X;

theorem :: SUBSET_1:57
    X <> {} implies {x1,x2,x3} is Subset of X;

theorem :: SUBSET_1:58
    X <> {} implies {x1,x2,x3,x4} is Subset of X;

theorem :: SUBSET_1:59
    X <> {} implies {x1,x2,x3,x4,x5} is Subset of X;

theorem :: SUBSET_1:60
    X <> {} implies {x1,x2,x3,x4,x5,x6} is Subset of X;

theorem :: SUBSET_1:61
    X <> {} implies {x1,x2,x3,x4,x5,x6,x7} is Subset of X;

theorem :: SUBSET_1:62
    X <> {} implies {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X;

theorem :: SUBSET_1:63
    x in X implies {x} is Subset of X;

 scheme Subset_Ex { A()-> set, P[set] } :
   ex X being Subset of A() st for x holds x in X iff x in A() & P[x];

scheme Subset_Eq {X() -> set, P[set]}:
 for X1,X2 being Subset of X() st
   (for y being Element of X() holds y in X1 iff P[y]) &
   (for y being Element of X() holds y in X2 iff P[y]) holds
  X1 = X2;

definition let X, Y be non empty set;
 redefine pred X misses Y;
 irreflexivity;
 antonym X meets Y;
end;

definition
   let S be set; assume
 contradiction;
 func choose S -> Element of S means
:: SUBSET_1:def 6
    not contradiction;
end;