:: by Andrzej Trybulec

::

:: Received January 8, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

Lm1: for x, X, y being set holds

( x in union {X,{y}} iff ( x in X or x = y ) )

proof end;

definition

let x1, x2, x3 be set ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 ) ) ) & ( for x being set holds

( x in b_{2} iff ( x = x1 or x = x2 or x = x3 ) ) ) holds

b_{1} = b_{2}

end;
func {x1,x2,x3} -> set means :Def1: :: ENUMSET1:def 1

for x being set holds

( x in it iff ( x = x1 or x = x2 or x = x3 ) );

existence for x being set holds

( x in it iff ( x = x1 or x = x2 or x = x3 ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines { ENUMSET1:def 1 :

for x1, x2, x3, b_{4} being set holds

( b_{4} = {x1,x2,x3} iff for x being set holds

( x in b_{4} iff ( x = x1 or x = x2 or x = x3 ) ) );

for x1, x2, x3, b

( b

( x in b

definition

let x1, x2, x3, x4 be set ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) & ( for x being set holds

( x in b_{2} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) holds

b_{1} = b_{2}

end;
func {x1,x2,x3,x4} -> set means :Def2: :: ENUMSET1:def 2

for x being set holds

( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 ) );

existence for x being set holds

( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def2 defines { ENUMSET1:def 2 :

for x1, x2, x3, x4, b_{5} being set holds

( b_{5} = {x1,x2,x3,x4} iff for x being set holds

( x in b_{5} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) );

for x1, x2, x3, x4, b

( b

( x in b

definition

let x1, x2, x3, x4, x5 be set ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) & ( for x being set holds

( x in b_{2} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) holds

b_{1} = b_{2}

end;
func {x1,x2,x3,x4,x5} -> set means :Def3: :: ENUMSET1:def 3

for x being set holds

( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) );

existence for x being set holds

( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def3 defines { ENUMSET1:def 3 :

for x1, x2, x3, x4, x5, b_{6} being set holds

( b_{6} = {x1,x2,x3,x4,x5} iff for x being set holds

( x in b_{6} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) );

for x1, x2, x3, x4, x5, b

( b

( x in b

definition

let x1, x2, x3, x4, x5, x6 be set ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ) & ( for x being set holds

( x in b_{2} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ) holds

b_{1} = b_{2}

end;
func {x1,x2,x3,x4,x5,x6} -> set means :Def4: :: ENUMSET1:def 4

for x being set holds

( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) );

existence for x being set holds

( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def4 defines { ENUMSET1:def 4 :

for x1, x2, x3, x4, x5, x6, b_{7} being set holds

( b_{7} = {x1,x2,x3,x4,x5,x6} iff for x being set holds

( x in b_{7} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) );

for x1, x2, x3, x4, x5, x6, b

( b

( x in b

definition

let x1, x2, x3, x4, x5, x6, x7 be set ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ) & ( for x being set holds

( x in b_{2} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ) holds

b_{1} = b_{2}

end;
func {x1,x2,x3,x4,x5,x6,x7} -> set means :Def5: :: ENUMSET1:def 5

for x being set holds

( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) );

existence for x being set holds

( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def5 defines { ENUMSET1:def 5 :

for x1, x2, x3, x4, x5, x6, x7, b_{8} being set holds

( b_{8} = {x1,x2,x3,x4,x5,x6,x7} iff for x being set holds

( x in b_{8} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) );

for x1, x2, x3, x4, x5, x6, x7, b

( b

( x in b

definition

let x1, x2, x3, x4, x5, x6, x7, x8 be set ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) ) & ( for x being set holds

( x in b_{2} 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

b_{1} = b_{2}

end;
func {x1,x2,x3,x4,x5,x6,x7,x8} -> set means :Def6: :: ENUMSET1:def 6

for x being set holds

( 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 ) );

existence for x being set holds

( 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 ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def6 defines { ENUMSET1:def 6 :

for x1, x2, x3, x4, x5, x6, x7, x8, b_{9} being set holds

( b_{9} = {x1,x2,x3,x4,x5,x6,x7,x8} iff for x being set holds

( x in b_{9} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) );

for x1, x2, x3, x4, x5, x6, x7, x8, b

( b

( x in b

definition

let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) ) & ( for x being set holds

( x in b_{2} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) ) holds

b_{1} = b_{2}

end;
func {x1,x2,x3,x4,x5,x6,x7,x8,x9} -> set means :Def7: :: ENUMSET1:def 7

for x being set holds

( 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 or x = x9 ) );

existence for x being set holds

( 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 or x = x9 ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def7 defines { ENUMSET1:def 7 :

for x1, x2, x3, x4, x5, x6, x7, x8, x9, b_{10} being set holds

( b_{10} = {x1,x2,x3,x4,x5,x6,x7,x8,x9} iff for x being set holds

( x in b_{10} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) );

for x1, x2, x3, x4, x5, x6, x7, x8, x9, b

( b

( x in b

definition

let x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 be set ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) ) & ( for x being set holds

( x in b_{2} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) ) holds

b_{1} = b_{2}

end;
func {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} -> set means :Def8: :: ENUMSET1:def 8

for x being set holds

( 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 or x = x9 or x = x10 ) );

existence for x being set holds

( 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 or x = x9 or x = x10 ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def8 defines { ENUMSET1:def 8 :

for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, b_{11} being set holds

( b_{11} = {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} iff for x being set holds

( x in b_{11} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) );

for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, b

( b

( x in b

Lm2: for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4}

proof end;

Lm3: for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5}

proof end;

theorem :: ENUMSET1:9

Lm4: for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6}

proof end;

theorem :: ENUMSET1:13

Lm5: for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7}

proof end;

theorem :: ENUMSET1:19

Lm6: for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8}

proof end;

theorem :: ENUMSET1:22

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8}

proof end;

theorem Th23: :: ENUMSET1:23

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2} \/ {x3,x4,x5,x6,x7,x8}

proof end;

theorem Th24: :: ENUMSET1:24

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3} \/ {x4,x5,x6,x7,x8}

proof end;

theorem :: ENUMSET1:25

theorem :: ENUMSET1:26

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8}

proof end;

theorem :: ENUMSET1:27

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5,x6} \/ {x7,x8}

proof end;

theorem :: ENUMSET1:28

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5,x6,x7} \/ {x8}

proof end;

Lm7: for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x3,x1,x4}

proof end;

Lm8: for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x2,x1,x4}

proof end;

Lm9: for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9}

proof end;

theorem :: ENUMSET1:77

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8,x9}

proof end;

theorem :: ENUMSET1:78

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2} \/ {x3,x4,x5,x6,x7,x8,x9}

proof end;

theorem :: ENUMSET1:79

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3} \/ {x4,x5,x6,x7,x8,x9}

proof end;

theorem :: ENUMSET1:80

theorem :: ENUMSET1:81

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9}

proof end;

theorem :: ENUMSET1:82

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6} \/ {x7,x8,x9}

proof end;

theorem :: ENUMSET1:83

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6,x7} \/ {x8,x9}

proof end;

theorem :: ENUMSET1:84

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6,x7,x8} \/ {x9}

proof end;

theorem :: ENUMSET1:85

for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} = {x1,x2,x3,x4,x5,x6,x7,x8,x9} \/ {x10}

proof end;

begin

:: from SCMBSORT, 2007.07.26, A.T.