:: Properties of Subsets
::  by Zinaida Trybulec
::
:: Received March 4, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies ZFMISC_1, XBOOLE_0, TARSKI, SUBSET_1, FUNCT_7;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1;
 constructors TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1;
 registrations XBOOLE_0, ZFMISC_1;
 requirements BOOLE;


begin

reserve E,X,Y,x for set;

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

registration
  let x1, x2, x3 be object;
  cluster { x1, x2, x3 } -> non empty;
  let x4 be object;
  cluster { x1, x2, x3, x4 } -> non empty;
  let x5 be object;
  cluster { x1, x2, x3, x4, x5 } -> non empty;
  let x6 be object;
  cluster { x1, x2, x3, x4, x5, x6 } -> non empty;
  let x7 be object;
  cluster { x1, x2, x3, x4, x5, x6, x7 } -> non empty;
  let x8 be object;
  cluster { x1, x2, x3, x4, x5, x6, x7, x8 } -> non empty;
  let x9 be object;
  cluster { x1, x2, x3, x4, x5, x6, x7, x8, x9 } -> non empty;
  let x10 be object;
  cluster { x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 } -> non empty;
end;

definition
  let X;
  mode Element of X -> set means
:: SUBSET_1:def 1
  it in X if X is non empty otherwise it is empty;
  sethood;
end;

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

registration
  let X be non empty set;
  cluster non empty for Subset of X;
end;

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

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

registration
  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;

registration
  let E;
  cluster empty for Subset of E;
end;

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

registration
  let E;
  cluster {}E -> empty;
end;

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

reserve A,B,C for Subset of E;

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

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

theorem :: SUBSET_1:4
  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 4
  E \ A;
  involutiveness;
  let B;
  redefine func A \/ B -> Subset of E;
  redefine func A \+\ B -> Subset of E;
end;

definition
  let X,Y be set;
  redefine func X \ Y -> Subset of X;
end;

definition
  let E,A,X;
  redefine func A \ X -> Subset of E;
end;

definition
  let E,A,X;
  redefine func A /\ X -> Subset of E;
end;

definition
  let E,X,A;
  redefine func X /\ A -> Subset of E;
end;

theorem :: SUBSET_1:5
  (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:6
  (for x being Element of E holds x in A iff x in B & x in C) implies A
  = B /\ C;

theorem :: SUBSET_1:7
  (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:8
  (for x being Element of E holds x in A iff not(x in B iff x in C))
  implies A = B \+\ C;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

::
::                 ADDITIONAL THEOREMS
::

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

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

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

theorem :: SUBSET_1:30
  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:31
  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:32
  for A,B st for x being Element of E holds not(x in A iff x in B) holds A = B`
;

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

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

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

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

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

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

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

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

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

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

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

scheme :: SUBSET_1:sch 2
  SubsetEq {X() -> set, X1,X2()-> Subset of X(), P[set]}: X1() = X2()
provided
 for y being Element of X() holds y in X1() iff P[y] and
 for y being Element of X() holds y in X2() iff P[y];

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

definition
  let X, Y be non empty set;
  redefine pred X meets Y;
  reflexivity;
end;

definition
::$CD
end;

begin

:: from SETWISEO, 2005.6.11 , A.T.

scheme :: SUBSET_1:sch 3
  SubsetEx { A() -> non empty set, P[object] } :
ex B being Subset of A() st for
  x being Element of A() holds x in B iff P[x];

:: from GROUP_2, 2005.6.14 , A.T.

scheme :: SUBSET_1:sch 4
  SubComp{A() -> set, F1,F2() -> Subset of A(), P[set]}: F1() = F2()
provided
 for X being Element of A() holds X in F1() iff P[X] and
 for X being Element of A() holds X in F2() iff P[X];

:: from FIN_TOPO, 2006.11.07. A.T.

theorem :: SUBSET_1:42
  A` = B` implies A = B;

:: from SGRAPH1, 2008.06.02

registration
  let X be empty set;
  cluster -> empty for Subset of X;
end;

:: from TEX_2, 2006.06.18, A.T. (simplified)

definition
  let E be set;
  let A be Subset of E;
  attr A is proper means
:: SUBSET_1:def 6
  A <> E;
end;

registration
  let E be set;
  cluster [#]E -> non proper;
end;

registration
  let E be set;
  cluster non proper for Subset of E;
end;

registration
  let E be non empty set;
  cluster non proper -> non empty for Subset of E;
  cluster empty -> proper for Subset of E;
end;

registration
  let E be non empty set;
  cluster proper for Subset of E;
end;

registration
  let E be empty set;
  cluster -> non proper for Subset of E;
end;

:: from GRCAT_1, 2010.02.18, A.T.

theorem :: SUBSET_1:43
  for X,Y,A being set, z being set st z in A & A c= [:X,Y:] ex x
  being Element of X, y being Element of Y st z = [x,y];

:: from BORSUK_4, 2011.03.04, A.T.

theorem :: SUBSET_1:44
  for X being non empty set, A, B being non empty Subset of X st A c< B
   ex p being Element of X st p in B & A c= B \ {p};

definition
  let X be set;
  redefine attr X is trivial means
:: SUBSET_1:def 7
  for x,y being Element of X holds x = y;
end;

registration let X be non empty set;
 cluster non empty trivial for Subset of X;
end;

registration
  let X be trivial set;
  cluster -> trivial for Subset of X;
end;

registration
  let X be non trivial set;
  cluster non trivial for Subset of X;
end;

theorem :: SUBSET_1:45
  for D being set, A being Subset of D st A is non trivial
    ex d1,d2 being Element of D st d1 in A & d2 in A & d1 <> d2;

theorem :: SUBSET_1:46
 for X being trivial non empty set
  ex x being Element of X st X = {x};

:: from BORSUK_4, 2011.07.31, A.T.

theorem :: SUBSET_1:47
  for X being non empty set, A being non empty Subset of X holds A
  is trivial implies ex x being Element of X st A = {x};

theorem :: SUBSET_1:48
  for X be non trivial set, x being Element of X
   ex y be object st y in X & x <> y;

:: from FUNCT_7, 3.20.2012, A.T.

reserve x for object;

definition
  let x,X;
  assume
 x in X;
  func In(x,X) -> Element of X equals
:: SUBSET_1:def 8
 x;
end;

registration
  let X be non empty set, x be Element of X;
  reduce In(x,X) to x;
end;

theorem :: SUBSET_1:49
  x in X /\ Y implies In(x,X) = In(x,Y);

:: from BORSUK_4, 2012.08.12, A.T.

theorem :: SUBSET_1:50
  for X being non trivial set, p being set ex q being Element of X st q <> p;

theorem :: SUBSET_1:51
  for T being non trivial set, X being non trivial Subset of T, p
  being set ex q being Element of T st q in X & q <> p;

:: 2012.12.16, A.T.

scheme :: SUBSET_1:sch 5
 Union1 { A()-> set, a()-> Element of A(), F(object) -> set }:
  union { F(j) where j is Element of A() : j in {a()}} = F(a());

scheme :: SUBSET_1:sch 6
 Union2 { A()-> set, a,b()-> Element of A(), F(object) -> set }:
  union { F(j) where j is Element of A() : j in {a(),b()}} = F(a()) \/ F(b());

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

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