The Mizar abstract of PZFMISC1

Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users
The abstract of the Mizar article:: Some Basic Properties of Many Sorted Sets
by
Artur Kornilowicz
Received September 29, 1995
MML identifier: PZFMISC1
[ Mizar article, MML identifier index ]
environ

 vocabulary FUNCT_1, PBOOLE, RELAT_1, FUNCT_4, CAT_1, BOOLE, MATRIX_1,
      ZF_REFLE, PRE_CIRC, FINSET_1, CAT_4, TARSKI, PRALG_2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_4, FINSET_1,
      CQC_LANG, PBOOLE, PRE_CIRC, PRALG_2, MBOOLEAN;
 constructors CQC_LANG, PRE_CIRC, PRALG_2, MBOOLEAN;
 clusters FINSET_1, PBOOLE, CQC_LANG, XBOOLE_0;
 requirements BOOLE;


begin :: Preliminaries

 reserve i, I for set,
         f for Function,
         x, x1, x2, y, A, B, X, Y, Z for ManySortedSet of I,
         J for non empty set,
         NJ for ManySortedSet of J;

theorem :: PZFMISC1:1
for X be set for M be ManySortedSet of I st i in I
 holds dom (M +* (i .--> X)) = I;

theorem :: PZFMISC1:2
  f = {} implies f is ManySortedSet of {};

theorem :: PZFMISC1:3
  I is non empty implies
 not ex X st X is empty-yielding & X is non-empty;

begin :: Singelton and unordered pairs

definition let I, A;
 func {A} -> ManySortedSet of I means
:: PZFMISC1:def 1
  for i st i in I holds it.i = {A.i};
end;

definition let I, A;
 cluster {A} -> non-empty locally-finite;
end;

definition let I, A, B;
 func {A,B} -> ManySortedSet of I means
:: PZFMISC1:def 2
  for i st i in I holds it.i = {A.i,B.i};
 commutativity;
end;

definition let I, A, B;
 cluster {A,B} -> non-empty locally-finite;
end;

theorem :: PZFMISC1:4     :: Tarski:3
  X = { y } iff for x holds x in X iff x = y;

theorem :: PZFMISC1:5     :: Tarski:4 a
  (for x holds x in X iff x = x1 or x = x2) implies X = { x1,x2 };

theorem :: PZFMISC1:6     :: Tarski:4 b
  X = { x1,x2 } implies for x holds x = x1 or x = x2 implies x in X;

theorem :: PZFMISC1:7
  { NJ } <> [0]I;

theorem :: PZFMISC1:8     :: ENUMSET1:3
  x in { A } implies x = A;

theorem :: PZFMISC1:9     :: ENUMSET1:4
  x in { x };

theorem :: PZFMISC1:10     :: ENUMSET1:9
  x = A or x = B implies x in { A,B };

theorem :: PZFMISC1:11     ::ENUMSET1:41
  {A} \/ {B} = {A,B};

theorem :: PZFMISC1:12     :: ENUMSET1:69
  { x,x } = { x };

canceled;

theorem :: PZFMISC1:14     :: SETWISEO:1
  {A} c= {B} implies A = B;

theorem :: PZFMISC1:15     :: ZFMISC_1:6
  {x} = {y} implies x = y;

theorem :: PZFMISC1:16     :: ZFMISC_1:8
  {x} = {A,B} implies x = A & x = B;

theorem :: PZFMISC1:17     :: ZFMISC_1:9
  {x} = {A,B} implies A = B;

theorem :: PZFMISC1:18     :: ZFMISC_1:12
  {x} c= {x,y} & {y} c= {x,y};

theorem :: PZFMISC1:19     :: ZFMISC_1:13
  {x} \/ {y} = {x} or {x} \/ {y} = {y} implies x = y;

theorem :: PZFMISC1:20     :: ZFMISC_1:14
  {x} \/ {x,y} = {x,y};

canceled;

theorem :: PZFMISC1:22     :: ZFMISC_1:16
  I is non empty & {x} /\ {y} = [0]I implies x <> y;

theorem :: PZFMISC1:23     :: ZFMISC_1:18
  {x} /\ {y} = {x} or {x} /\ {y} = {y} implies x = y;

theorem :: PZFMISC1:24     :: ZFMISC_1:19
  {x} /\ {x,y} = {x} & {y} /\ {x,y} = {y};

theorem :: PZFMISC1:25     :: ZFMISC_1:20
  I is non empty & {x} \ {y} = {x} implies x <> y;

theorem :: PZFMISC1:26     :: ZFMISC_1:21
  {x} \ {y} = [0]I implies x = y;

theorem :: PZFMISC1:27     :: ZFMISC_1:22
  {x} \ {x,y} = [0]I & {y} \ {x,y} = [0]I;

theorem :: PZFMISC1:28     :: ZFMISC_1:24
  {x} c= {y} implies {x} = {y};

theorem :: PZFMISC1:29     :: ZFMISC_1:26
  {x,y} c= {A} implies x = A & y = A;

theorem :: PZFMISC1:30     :: ZFMISC_1:27
  {x,y} c= {A} implies {x,y} = {A};

theorem :: PZFMISC1:31     :: ZFMISC_1:30
  bool { x } = { [0]I, {x} };

theorem :: PZFMISC1:32     :: ZFMISC_1:80
  { A } c= bool A;

theorem :: PZFMISC1:33     :: ZFMISC_1:31
  union { x } = x;

theorem :: PZFMISC1:34     :: ZFMISC_1:32
  union { {x},{y} } = {x,y};

theorem :: PZFMISC1:35     :: ZFMISC_1:93
  union { A,B } = A \/ B;

theorem :: PZFMISC1:36     :: ZFMISC_1:37
  {x} c= X iff x in X;

theorem :: PZFMISC1:37     :: ZFMISC_1:38
  {x1,x2} c= X iff x1 in X & x2 in X;

theorem :: PZFMISC1:38     :: ZFMISC_1:42
  A = [0]I or A = {x1} or A = {x2} or A = {x1,x2} implies A c= {x1,x2};

begin :: Sum of an unordered pairs (or a singelton) and a set

theorem :: PZFMISC1:39     :: SETWISEO:6
  x in A or x = B implies x in A \/ {B};

theorem :: PZFMISC1:40     :: SETWISEO:8
  A \/ {x} c= B iff x in B & A c= B;

theorem :: PZFMISC1:41     :: ZFMISC_1:45
  {x} \/ X = X implies x in X;

theorem :: PZFMISC1:42     :: ZFMISC_1:46
  x in X implies {x} \/ X = X;

theorem :: PZFMISC1:43     :: ZFMISC_1:47, 48
  {x,y} \/ A = A iff x in A & y in A;

theorem :: PZFMISC1:44     :: ZFMISC_1:49
  I is non empty implies {x} \/ X <> [0]I;

theorem :: PZFMISC1:45     :: ZFMISC_1:50
  I is non empty implies {x,y} \/ X <> [0]I;

begin :: Intersection of an unordered pairs (or a singelton) and a set

theorem :: PZFMISC1:46     :: ZFMISC_1:51
  X /\ {x} = {x} implies x in X;

theorem :: PZFMISC1:47     :: ZFMISC_1:52
  x in X implies X /\ {x} = {x};

theorem :: PZFMISC1:48     :: ZFMISC_1:53, 63
  x in X & y in X iff {x,y} /\ X = {x,y};

theorem :: PZFMISC1:49     :: ZFMISC_1:54
  I is non empty & {x} /\ X = [0]I implies not x in X;

theorem :: PZFMISC1:50     :: ZFMISC_1:55
  I is non empty & {x,y} /\ X = [0]I implies not x in X & not y in X;

begin :: Difference of an unordered pairs (or a singelton) and a set

theorem :: PZFMISC1:51     :: ZFMISC_1:64 a
  y in X \ {x} implies y in X;

theorem :: PZFMISC1:52     :: ZFMISC_1:64 b
  I is non empty & y in X \ {x} implies y <> x;

theorem :: PZFMISC1:53     :: ZFMISC_1:65
  I is non empty & X \ {x} = X implies not x in X;

theorem :: PZFMISC1:54     :: ZFMISC_1:67
  I is non empty & {x} \ X = {x} implies not x in X;

theorem :: PZFMISC1:55     :: ZFMISC_1:68
  {x} \ X = [0]I iff x in X;

theorem :: PZFMISC1:56     :: ZFMISC_1:70
  I is non empty & {x,y} \ X = {x} implies not x in X;

canceled;

theorem :: PZFMISC1:58     :: ZFMISC_1:72
  I is non empty & {x,y} \ X = {x,y} implies not x in X & not y in X;

theorem :: PZFMISC1:59     :: ZFMISC_1:73
  {x,y} \ X = [0]I iff x in X & y in X;

theorem :: PZFMISC1:60     :: ZFMISC_1:75
  X = [0]I or X = {x} or X = {y} or X = {x,y} implies X \ {x,y} = [0]I;

begin :: Cartesian product

theorem :: PZFMISC1:61     :: ZFMISC_1:113
  X = [0]I or Y = [0]I implies [|X,Y|] = [0]I;

theorem :: PZFMISC1:62     :: ZFMISC_1:114
  X is non-empty & Y is non-empty & [|X,Y|] = [|Y,X|] implies X = Y;

theorem :: PZFMISC1:63     :: ZFMISC_1:115
  [|X,X|] = [|Y,Y|] implies X = Y;

theorem :: PZFMISC1:64     :: ZFMISC_1:117
  Z is non-empty & ([|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|]) implies X c= Y;

theorem :: PZFMISC1:65     :: ZFMISC_1:118
  X c= Y implies [|X,Z|] c= [|Y,Z|] & [|Z,X|] c= [|Z,Y|];

theorem :: PZFMISC1:66     :: ZFMISC_1:119
  x1 c= A & x2 c= B implies [|x1,x2|] c= [|A,B|];

theorem :: PZFMISC1:67     :: ZFMISC_1:120
  [|X \/ Y, Z|] = [|X, Z|] \/ [|Y, Z|]
  & [|Z, X \/ Y|] = [|Z, X|] \/ [|Z, Y|];

theorem :: PZFMISC1:68     :: ZFMISC_1:121
  [|x1 \/ x2, A \/ B|] = [|x1,A|] \/ [|x1,B|] \/ [|x2,A|] \/ [|x2,B|];

theorem :: PZFMISC1:69     :: ZFMISC_1:122
  [|X /\ Y, Z|] = [|X, Z|] /\ [|Y, Z|]
  & [|Z, X /\ Y|] = [|Z, X|] /\ [|Z, Y|];

theorem :: PZFMISC1:70     :: ZFMISC_1:123
  [|x1 /\ x2, A /\ B|] = [|x1,A|] /\ [|x2, B|];

theorem :: PZFMISC1:71     :: ZFMISC_1:124
  A c= X & B c= Y implies [|A,Y|] /\ [|X,B|] = [|A,B|];

theorem :: PZFMISC1:72     :: ZFMISC_1:125
  [|X \ Y, Z|] = [|X, Z|] \ [|Y, Z|]
  & [|Z, X \ Y|] = [|Z, X|] \ [|Z, Y|];

theorem :: PZFMISC1:73     :: ZFMISC_1:126
  [|x1,x2|] \ [|A,B|] = [|x1\A,x2|] \/ [|x1,x2\B|];

theorem :: PZFMISC1:74     :: ZFMISC_1:127
  x1 /\ x2 = [0]I or A /\ B = [0]I implies [|x1,A|] /\ [|x2,B|] = [0]I;

theorem :: PZFMISC1:75     :: ZFMISC_1:130
  X is non-empty implies [|{x},X|] is non-empty & [|X,{x}|] is non-empty;

theorem :: PZFMISC1:76     :: ZFMISC_1:132
  [|{x,y},X|] = [|{x},X|] \/ [|{y},X|]
  & [|X,{x,y}|] = [|X,{x}|] \/ [|X,{y}|];

theorem :: PZFMISC1:77     :: ZFMISC_1:134
  x1 is non-empty & A is non-empty & [|x1,A|] = [|x2,B|]
  implies x1 = x2 & A = B;

theorem :: PZFMISC1:78     :: ZFMISC_1:116, 135
  X c= [|X,Y|] or X c= [|Y,X|] implies X = [0]I;

theorem :: PZFMISC1:79     :: BORSUK_1:2
  A in [|x,y|] & A in [|X,Y|] implies A in [|x /\ X, y /\ Y|];

theorem :: PZFMISC1:80     :: BORSUK_1:7
  [|x,X|] c= [|y,Y|] & [|x,X|] is non-empty implies x c= y & X c= Y;

theorem :: PZFMISC1:81     :: REALSET1:4
  A c= X implies [|A,A|] c= [|X,X|];

theorem :: PZFMISC1:82     :: SYSREL:17
  X /\ Y = [0]I implies [|X,Y|] /\ [|Y,X|] = [0]I;

theorem :: PZFMISC1:83     :: ALTCAT_1:1
  A is non-empty & ([|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|]) implies B c= Y;

theorem :: PZFMISC1:84     :: PARTFUN1:1
  x c= [|A,B|] & y c= [|X,Y|] implies x \/ y c= [|A \/ X,B \/ Y|];
The abstract of the Mizar article:

Some Basic Properties of Many Sorted Sets
