Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Enumerated Sets

by
Andrzej Trybulec

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 };
```