The abstract of the Mizar article:

Enumerated Sets

by

Andrzej Trybulec

Received January 8, 1989

MML identifier: ENUMSET1

[ Mizar article, MML identifier index ]

environ

 vocabulary TARSKI, BOOLE;
 notation TARSKI, XBOOLE_0;
 constructors TARSKI, XBOOLE_0;
 clusters XBOOLE_0;


begin

  reserve x,x1,x2,x3,x4,x5,x6,x7,x8,y,X,Z for set;

scheme UI1{x1()->set,P[set]}:
  P[x1()]
provided  for x1 holds P[x1];

scheme UI2{x1, x2()->set,P[set,set]}:
  P[x1(),x2()]
provided  for x1,x2 holds P[x1,x2];

scheme UI3{x1, x2, x3()->set,P[set,set,set]}:
  P[x1(),x2(),x3()]
provided  for x1,x2,x3 holds P[x1,x2,x3];

scheme UI4{x1, x2, x3, x4()->set,P[set,set,set,set]}:
  P[x1(),x2(),x3(),x4()]
provided  for x1,x2,x3,x4 holds P[x1,x2,x3,x4];

scheme UI5
  {x1, x2, x3, x4, x5()->set, P[set,set,set,set,set]}:
  P[x1(),x2(),x3(),x4(),x5()]
provided  for x1,x2,x3,x4,x5 holds P[x1,x2,x3,x4,x5];

scheme UI6
  {x1, x2, x3, x4, x5, x6()->set,
   P[set,set,set,set,set,set]}:
  P[x1(),x2(),x3(),x4(),x5(),x6()]
provided  for x1,x2,x3,x4,x5,x6 holds P[x1,x2,x3,x4,x5,x6];

scheme UI7
  {x1, x2, x3, x4, x5, x6, x7()->set,
   P[set,set,set,set,set,set,set]}:
  P[x1(),x2(),x3(),x4(),x5(),x6(),x7()]
provided  for x1,x2,x3,x4,x5,x6,x7 holds P[x1,x2,x3,x4,x5,x6,x7];

scheme UI8
  {x1, x2, x3, x4, x5, x6, x7, x8()->set,
   P[set,set,set,set,set,set,set,set]}:
  P[x1(),x2(),x3(),x4(),x5(),x6(),x7(),x8()]
provided  for x1,x2,x3,x4,x5,x6,x7,x8 holds P[x1,x2,x3,x4,x5,x6,x7,x8]
;

scheme UI9
  {x1, x2, x3, x4, x5, x6, x7, x8, x9()->set,
   P[set,set,set,set,set,set,set,set,set]}:
  P[x1(),x2(),x3(),x4(),x5(),x6(),x7(),x8(),x9()]
provided
  for x1,x2,x3,x4,x5,x6,x7,x8,x9 being set
         holds P[x1,x2,x3,x4,x5,x6,x7,x8,x9];

definition let x1,x2,x3;
    func { x1,x2,x3 } -> set means
:: ENUMSET1:def 1
 x in it iff x=x1 or x=x2 or x=x3;
end;

canceled 12;

theorem :: ENUMSET1:13
     x in { x1,x2,x3 } implies x=x1 or x=x2 or x=x3;

theorem :: ENUMSET1:14
     x=x1 or x=x2 or x=x3 implies x in { x1,x2,x3 };

theorem :: ENUMSET1:15
    for x1,x2,x3,X st
   for x holds x in X iff x=x1 or x=x2 or x=x3
    holds X = { x1,x2,x3 };

definition
   let x1,x2,x3,x4;
    func { x1,x2,x3,x4 } -> set means
:: ENUMSET1:def 2
 x in it iff x=x1 or x=x2 or x=x3 or x=x4;
end;

canceled 2;

theorem :: ENUMSET1:18
  x in { x1,x2,x3,x4 } implies x=x1 or x=x2 or x=x3 or x = x4;

theorem :: ENUMSET1:19
  x=x1 or x=x2 or x=x3 or x = x4 implies x in { x1,x2,x3,x4 };

theorem :: ENUMSET1:20
    for x1,x2,x3,x4,X st
     for x holds x in X iff x=x1 or x=x2 or x=x3 or x = x4
    holds X = { x1,x2,x3,x4 };

definition
  let x1,x2,x3,x4,x5;
    func { x1,x2,x3,x4,x5 } -> set means
:: ENUMSET1:def 3
 x in it iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5;
end;

canceled 2;

theorem :: ENUMSET1:23
    x in { x1,x2,x3,x4,x5 } implies x=x1 or x=x2 or x=x3 or x=x4 or x=x5;

theorem :: ENUMSET1:24
  x=x1 or x=x2 or x=x3 or x=x4 or x=x5 implies x in
    { x1,x2,x3,x4,x5 };

theorem :: ENUMSET1:25
   for X being set st
   for x holds x in X iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5
    holds X = { x1,x2,x3,x4,x5 };

definition
   let x1,x2,x3,x4,x5,x6;
    func { x1,x2,x3,x4,x5,x6 } -> set means
:: ENUMSET1:def 4
 x in it iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6;
end;

canceled 2;

theorem :: ENUMSET1:28
       x in { x1,x2,x3,x4,x5,x6 } implies
        x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6;

theorem :: ENUMSET1:29
     x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 implies
        x in { x1,x2,x3,x4,x5,x6 };

theorem :: ENUMSET1:30
     for X being set st
     for x holds x in X iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6
      holds X = { x1,x2,x3,x4,x5,x6 };

definition
   let x1,x2,x3,x4,x5,x6,x7;
    func { x1,x2,x3,x4,x5,x6,x7 } -> set means
:: ENUMSET1:def 5
 x in it iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7;
end;

canceled 2;

theorem :: ENUMSET1:33
      x in { x1,x2,x3,x4,x5,x6,x7 } implies
      x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7;

theorem :: ENUMSET1:34
     x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 implies
    x in { x1,x2,x3,x4,x5,x6,x7 };

theorem :: ENUMSET1:35
     for X being set st
    for x holds x in X iff
        x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7
    holds X = { x1,x2,x3,x4,x5,x6,x7 };

definition
   let x1,x2,x3,x4,x5,x6,x7,x8;
    func { x1,x2,x3,x4,x5,x6,x7,x8 } -> set means
:: ENUMSET1:def 6
 x in
 it iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8;
end;

canceled 2;

theorem :: ENUMSET1:38
  x in { x1,x2,x3,x4,x5,x6,x7,x8 } implies
    x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8;

theorem :: ENUMSET1:39
  x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8 implies
     x in { x1,x2,x3,x4,x5,x6,x7,x8 };

theorem :: ENUMSET1:40
    for X being set st
     for x holds x in X iff
        x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8
    holds X = { x1,x2,x3,x4,x5,x6,x7,x8 };

theorem :: ENUMSET1:41
 { x1,x2 } = { x1 } \/ { x2 };

theorem :: ENUMSET1:42
 { x1,x2,x3 } = { x1 } \/ { x2,x3 };

theorem :: ENUMSET1:43
 { x1,x2,x3 } = { x1,x2 } \/ { x3 };

theorem :: ENUMSET1:44
 { x1,x2,x3,x4 } = { x1 } \/ { x2,x3,x4 };

theorem :: ENUMSET1:45
   { x1,x2,x3,x4 } = { x1,x2 } \/ { x3,x4 };

theorem :: ENUMSET1:46
 { x1,x2,x3,x4 } = { x1,x2,x3 } \/ { x4 };

theorem :: ENUMSET1:47
 { x1,x2,x3,x4,x5 } = { x1 } \/ { x2,x3,x4,x5 };

theorem :: ENUMSET1:48
 { x1,x2,x3,x4,x5 } = { x1,x2 } \/ { x3,x4,x5 };

theorem :: ENUMSET1:49
   { x1,x2,x3,x4,x5 } = { x1,x2,x3 } \/ { x4,x5 };

theorem :: ENUMSET1:50
 { x1,x2,x3,x4,x5 } = { x1,x2,x3,x4 } \/ { x5 };

theorem :: ENUMSET1:51
 { x1,x2,x3,x4,x5,x6 } = { x1 } \/ { x2,x3,x4,x5,x6 };

theorem :: ENUMSET1:52
 { x1,x2,x3,x4,x5,x6 } = { x1,x2 } \/ { x3,x4,x5,x6 };

theorem :: ENUMSET1:53
   { x1,x2,x3,x4,x5,x6 } = { x1,x2,x3 } \/ { x4,x5,x6 };

theorem :: ENUMSET1:54
 { x1,x2,x3,x4,x5,x6 } = { x1,x2,x3,x4 } \/ { x5,x6 };

theorem :: ENUMSET1:55
   { x1,x2,x3,x4,x5,x6 } = { x1,x2,x3,x4,x5 } \/ { x6 };

theorem :: ENUMSET1:56
 { x1,x2,x3,x4,x5,x6,x7 } = { x1 } \/ { x2,x3,x4,x5,x6,x7 };

theorem :: ENUMSET1:57
 { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2 } \/ { x3,x4,x5,x6,x7 };

theorem :: ENUMSET1:58
 { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3 } \/ { x4,x5,x6,x7 };

theorem :: ENUMSET1:59
   { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4 } \/ { x5,x6,x7 };

theorem :: ENUMSET1:60
   { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4,x5 } \/ { x6,x7 };

theorem :: ENUMSET1:61
   { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4,x5,x6 } \/ { x7 };

theorem :: ENUMSET1:62
   { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1 } \/ { x2,x3,x4,x5,x6,x7,x8 };

theorem :: ENUMSET1:63
 { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2 } \/ { x3,x4,x5,x6,x7,x8 };

theorem :: ENUMSET1:64
   { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3 } \/ { x4,x5,x6,x7,x8 };

theorem :: ENUMSET1:65
   { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8 };

theorem :: ENUMSET1:66
   { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4,x5 } \/ { x6,x7,x8 };

theorem :: ENUMSET1:67
   { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4,x5,x6 } \/ { x7,x8 };

theorem :: ENUMSET1:68
   { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4,x5,x6,x7 } \/ { x8 };

theorem :: ENUMSET1:69
 { x1,x1 } = { x1 };

theorem :: ENUMSET1:70
 { x1,x1,x2 } = { x1,x2 };

theorem :: ENUMSET1:71
 { x1,x1,x2,x3 } = { x1,x2,x3 };

theorem :: ENUMSET1:72
 { x1,x1,x2,x3,x4 } = { x1,x2,x3,x4 };

theorem :: ENUMSET1:73
 { x1,x1,x2,x3,x4,x5 } = { x1,x2,x3,x4,x5 };

theorem :: ENUMSET1:74
 { x1,x1,x2,x3,x4,x5,x6 } = { x1,x2,x3,x4,x5,x6 };

theorem :: ENUMSET1:75
 { x1,x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4,x5,x6,x7 };

theorem :: ENUMSET1:76
   { x1,x1,x1 } = { x1 };

theorem :: ENUMSET1:77
 { x1,x1,x1,x2 } = { x1,x2 };

theorem :: ENUMSET1:78
 { x1,x1,x1,x2,x3 } = { x1,x2,x3 };

theorem :: ENUMSET1:79
 { x1,x1,x1,x2,x3,x4 } = { x1,x2,x3,x4 };

theorem :: ENUMSET1:80
 { x1,x1,x1,x2,x3,x4,x5 } = { x1,x2,x3,x4,x5 };

theorem :: ENUMSET1:81
 { x1,x1,x1,x2,x3,x4,x5,x6 } = { x1,x2,x3,x4,x5,x6 };

theorem :: ENUMSET1:82
   { x1,x1,x1,x1 } = { x1 };

theorem :: ENUMSET1:83
 { x1,x1,x1,x1,x2 } = { x1,x2 };

theorem :: ENUMSET1:84
 { x1,x1,x1,x1,x2,x3 } = { x1,x2,x3 };

theorem :: ENUMSET1:85
 { x1,x1,x1,x1,x2,x3,x4 } = { x1,x2,x3,x4 };

theorem :: ENUMSET1:86
 { x1,x1,x1,x1,x2,x3,x4,x5 } = { x1,x2,x3,x4,x5 };

theorem :: ENUMSET1:87
   { x1,x1,x1,x1,x1 } = { x1 };

theorem :: ENUMSET1:88
 { x1,x1,x1,x1,x1,x2 } = { x1,x2 };

theorem :: ENUMSET1:89
 { x1,x1,x1,x1,x1,x2,x3 } = { x1,x2,x3 };

theorem :: ENUMSET1:90
 { x1,x1,x1,x1,x1,x2,x3,x4 } = { x1,x2,x3,x4 };

theorem :: ENUMSET1:91
   { x1,x1,x1,x1,x1,x1 } = { x1 };

theorem :: ENUMSET1:92
 { x1,x1,x1,x1,x1,x1,x2 } = { x1,x2 };

theorem :: ENUMSET1:93
 { x1,x1,x1,x1,x1,x1,x2,x3 } = { x1,x2,x3 };


theorem :: ENUMSET1:94
   { x1,x1,x1,x1,x1,x1,x1 } = { x1 };

theorem :: ENUMSET1:95
 { x1,x1,x1,x1,x1,x1,x1,x2 } = { x1,x2 };

theorem :: ENUMSET1:96
   { x1,x1,x1,x1,x1,x1,x1,x1 } = { x1 };

canceled;

theorem :: ENUMSET1:98
 { x1,x2,x3 } = { x1,x3,x2 };

theorem :: ENUMSET1:99
 { x1,x2,x3 } = { x2,x1,x3 };

theorem :: ENUMSET1:100
 { x1,x2,x3 } = { x2,x3,x1 };

canceled;

theorem :: ENUMSET1:102
 { x1,x2,x3 } = { x3,x2,x1 };

theorem :: ENUMSET1:103
 { x1,x2,x3,x4 } = { x1,x2,x4,x3 };

theorem :: ENUMSET1:104
   { x1,x2,x3,x4 } = { x1,x3,x2,x4 };

theorem :: ENUMSET1:105
 { x1,x2,x3,x4 } = { x1,x3,x4,x2 };

canceled;

theorem :: ENUMSET1:107
 { x1,x2,x3,x4 } = { x1,x4,x3,x2 };

theorem :: ENUMSET1:108
 { x1,x2,x3,x4 } = { x2,x1,x3,x4 };

theorem :: ENUMSET1:109
   { x1,x2,x3,x4 } = { x2,x1,x4,x3 };

theorem :: ENUMSET1:110
   { x1,x2,x3,x4 } = { x2,x3,x1,x4 };

theorem :: ENUMSET1:111
   { x1,x2,x3,x4 } = { x2,x3,x4,x1 };

theorem :: ENUMSET1:112
   { x1,x2,x3,x4 } = { x2,x4,x1,x3 };

theorem :: ENUMSET1:113
   { x1,x2,x3,x4 } = { x2,x4,x3,x1 };

canceled 2;

theorem :: ENUMSET1:116
   { x1,x2,x3,x4 } = { x3,x2,x1,x4 };

theorem :: ENUMSET1:117
   { x1,x2,x3,x4 } = { x3,x2,x4,x1 };

theorem :: ENUMSET1:118
   { x1,x2,x3,x4 } = { x3,x4,x1,x2 };

theorem :: ENUMSET1:119
 { x1,x2,x3,x4 } = { x3,x4,x2,x1 };

canceled 3;

theorem :: ENUMSET1:123
   { x1,x2,x3,x4 } = { x4,x2,x3,x1 };

canceled;

theorem :: ENUMSET1:125
   { x1,x2,x3,x4 } = { x4,x3,x2,x1 };