:: Enumerated Sets
:: by Andrzej Trybulec
::
:: Received January 8, 1989
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
for x, X, y being set holds
( x in union {X,{y}} iff ( x in X or x = y ) )
definition
let x1,
x2,
x3 be
set ;
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
ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 ) ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines { ENUMSET1:def 1 :
for
x1,
x2,
x3,
b4 being
set holds
(
b4 = {x1,x2,x3} iff for
x being
set holds
(
x in b4 iff (
x = x1 or
x = x2 or
x = x3 ) ) );
definition
let x1,
x2,
x3,
x4 be
set ;
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
ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines { ENUMSET1:def 2 :
for
x1,
x2,
x3,
x4,
b5 being
set holds
(
b5 = {x1,x2,x3,x4} iff for
x being
set holds
(
x in b5 iff (
x = x1 or
x = x2 or
x = x3 or
x = x4 ) ) );
definition
let x1,
x2,
x3,
x4,
x5 be
set ;
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
ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) holds
b1 = b2
end;
:: deftheorem Def3 defines { ENUMSET1:def 3 :
for
x1,
x2,
x3,
x4,
x5,
b6 being
set holds
(
b6 = {x1,x2,x3,x4,x5} iff for
x being
set holds
(
x in b6 iff (
x = x1 or
x = x2 or
x = x3 or
x = x4 or
x = x5 ) ) );
definition
let x1,
x2,
x3,
x4,
x5,
x6 be
set ;
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
ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 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 b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ) holds
b1 = b2
end;
:: deftheorem Def4 defines { ENUMSET1:def 4 :
for
x1,
x2,
x3,
x4,
x5,
x6,
b7 being
set holds
(
b7 = {x1,x2,x3,x4,x5,x6} iff for
x being
set holds
(
x in b7 iff (
x = x1 or
x = x2 or
x = x3 or
x = x4 or
x = x5 or
x = x6 ) ) );
definition
let x1,
x2,
x3,
x4,
x5,
x6,
x7 be
set ;
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
ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 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 b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ) holds
b1 = b2
end;
:: deftheorem Def5 defines { ENUMSET1:def 5 :
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
b8 being
set holds
(
b8 = {x1,x2,x3,x4,x5,x6,x7} iff for
x being
set holds
(
x in b8 iff (
x = x1 or
x = x2 or
x = x3 or
x = x4 or
x = x5 or
x = x6 or
x = x7 ) ) );
definition
let x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 be
set ;
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
ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 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 b2 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
b1 = b2
end;
:: deftheorem Def6 defines { ENUMSET1:def 6 :
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
b9 being
set holds
(
b9 = {x1,x2,x3,x4,x5,x6,x7,x8} iff for
x being
set holds
(
x in b9 iff (
x = x1 or
x = x2 or
x = x3 or
x = x4 or
x = x5 or
x = x6 or
x = x7 or
x = x8 ) ) );
definition
let x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 be
set ;
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
ex b1 being set st
for x being set holds
( x in b1 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 ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 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 b2 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
b1 = b2
end;
:: deftheorem Def7 defines { ENUMSET1:def 7 :
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
b10 being
set holds
(
b10 = {x1,x2,x3,x4,x5,x6,x7,x8,x9} iff for
x being
set holds
(
x in b10 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 ) ) );
definition
let x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
x10 be
set ;
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
ex b1 being set st
for x being set holds
( x in b1 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 ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 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 b2 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
b1 = b2
end;
:: deftheorem Def8 defines { ENUMSET1:def 8 :
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
x10,
b11 being
set holds
(
b11 = {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} iff for
x being
set holds
(
x in b11 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 ) ) );
theorem :: ENUMSET1:1
canceled;
theorem :: ENUMSET1:2
canceled;
theorem :: ENUMSET1:3
canceled;
theorem :: ENUMSET1:4
canceled;
theorem :: ENUMSET1:5
canceled;
theorem :: ENUMSET1:6
canceled;
theorem :: ENUMSET1:7
canceled;
theorem :: ENUMSET1:8
canceled;
theorem :: ENUMSET1:9
canceled;
theorem :: ENUMSET1:10
canceled;
theorem :: ENUMSET1:11
canceled;
theorem :: ENUMSET1:12
canceled;
theorem :: ENUMSET1:13
canceled;
theorem :: ENUMSET1:14
canceled;
theorem :: ENUMSET1:15
canceled;
theorem :: ENUMSET1:16
canceled;
theorem :: ENUMSET1:17
canceled;
theorem :: ENUMSET1:18
canceled;
theorem :: ENUMSET1:19
canceled;
theorem :: ENUMSET1:20
canceled;
theorem :: ENUMSET1:21
canceled;
theorem :: ENUMSET1:22
canceled;
theorem :: ENUMSET1:23
canceled;
theorem :: ENUMSET1:24
canceled;
theorem :: ENUMSET1:25
canceled;
theorem :: ENUMSET1:26
canceled;
theorem :: ENUMSET1:27
canceled;
theorem :: ENUMSET1:28
canceled;
theorem :: ENUMSET1:29
canceled;
theorem :: ENUMSET1:30
canceled;
theorem :: ENUMSET1:31
canceled;
theorem :: ENUMSET1:32
canceled;
theorem :: ENUMSET1:33
canceled;
theorem :: ENUMSET1:34
canceled;
theorem :: ENUMSET1:35
canceled;
theorem :: ENUMSET1:36
canceled;
theorem :: ENUMSET1:37
canceled;
theorem :: ENUMSET1:38
canceled;
theorem :: ENUMSET1:39
canceled;
theorem :: ENUMSET1:40
canceled;
theorem Th41: :: ENUMSET1:41
theorem Th42: :: ENUMSET1:42
theorem Th43: :: ENUMSET1:43
Lm2:
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4}
theorem Th44: :: ENUMSET1:44
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x1} \/ {x2,x3,x4}
theorem :: ENUMSET1:45
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x1,x2} \/ {x3,x4} by Lm2;
theorem Th46: :: ENUMSET1:46
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x1,x2,x3} \/ {x4}
Lm3:
for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5}
theorem Th47: :: ENUMSET1:47
for
x1,
x2,
x3,
x4,
x5 being
set holds
{x1,x2,x3,x4,x5} = {x1} \/ {x2,x3,x4,x5}
theorem Th48: :: ENUMSET1:48
for
x1,
x2,
x3,
x4,
x5 being
set holds
{x1,x2,x3,x4,x5} = {x1,x2} \/ {x3,x4,x5}
theorem :: ENUMSET1:49
for
x1,
x2,
x3,
x4,
x5 being
set holds
{x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5} by Lm3;
theorem Th50: :: ENUMSET1:50
for
x1,
x2,
x3,
x4,
x5 being
set holds
{x1,x2,x3,x4,x5} = {x1,x2,x3,x4} \/ {x5}
Lm4:
for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6}
theorem Th51: :: ENUMSET1:51
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x2,x3,x4,x5,x6} = {x1} \/ {x2,x3,x4,x5,x6}
theorem Th52: :: ENUMSET1:52
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x2,x3,x4,x5,x6} = {x1,x2} \/ {x3,x4,x5,x6}
theorem :: ENUMSET1:53
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} by Lm4;
theorem Th54: :: ENUMSET1:54
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4} \/ {x5,x6}
theorem :: ENUMSET1:55
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5} \/ {x6}
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}
theorem Th56: :: ENUMSET1:56
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}
theorem Th57: :: ENUMSET1:57
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}
theorem Th58: :: ENUMSET1:58
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}
theorem :: ENUMSET1:59
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} by Lm5;
theorem :: ENUMSET1:60
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}
theorem :: ENUMSET1:61
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}
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}
theorem :: ENUMSET1:62
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}
theorem Th63: :: ENUMSET1:63
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}
theorem Th64: :: ENUMSET1:64
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}
theorem :: ENUMSET1:65
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} by Lm6;
theorem :: ENUMSET1:66
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}
theorem :: ENUMSET1:67
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}
theorem :: ENUMSET1:68
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}
theorem Th69: :: ENUMSET1:69
theorem Th70: :: ENUMSET1:70
for
x1,
x2 being
set holds
{x1,x1,x2} = {x1,x2}
theorem Th71: :: ENUMSET1:71
for
x1,
x2,
x3 being
set holds
{x1,x1,x2,x3} = {x1,x2,x3}
theorem Th72: :: ENUMSET1:72
for
x1,
x2,
x3,
x4 being
set holds
{x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
theorem Th73: :: ENUMSET1:73
for
x1,
x2,
x3,
x4,
x5 being
set holds
{x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
theorem Th74: :: ENUMSET1:74
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5,x6}
theorem Th75: :: ENUMSET1:75
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
{x1,x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6,x7}
theorem :: ENUMSET1:76
for
x1 being
set holds
{x1,x1,x1} = {x1}
theorem Th77: :: ENUMSET1:77
for
x1,
x2 being
set holds
{x1,x1,x1,x2} = {x1,x2}
theorem Th78: :: ENUMSET1:78
for
x1,
x2,
x3 being
set holds
{x1,x1,x1,x2,x3} = {x1,x2,x3}
theorem Th79: :: ENUMSET1:79
for
x1,
x2,
x3,
x4 being
set holds
{x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
theorem Th80: :: ENUMSET1:80
for
x1,
x2,
x3,
x4,
x5 being
set holds
{x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
theorem Th81: :: ENUMSET1:81
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x1,x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5,x6}
theorem :: ENUMSET1:82
for
x1 being
set holds
{x1,x1,x1,x1} = {x1}
theorem Th83: :: ENUMSET1:83
for
x1,
x2 being
set holds
{x1,x1,x1,x1,x2} = {x1,x2}
theorem Th84: :: ENUMSET1:84
for
x1,
x2,
x3 being
set holds
{x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
theorem Th85: :: ENUMSET1:85
for
x1,
x2,
x3,
x4 being
set holds
{x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
theorem Th86: :: ENUMSET1:86
for
x1,
x2,
x3,
x4,
x5 being
set holds
{x1,x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
theorem :: ENUMSET1:87
for
x1 being
set holds
{x1,x1,x1,x1,x1} = {x1}
theorem Th88: :: ENUMSET1:88
for
x1,
x2 being
set holds
{x1,x1,x1,x1,x1,x2} = {x1,x2}
theorem Th89: :: ENUMSET1:89
for
x1,
x2,
x3 being
set holds
{x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
theorem Th90: :: ENUMSET1:90
for
x1,
x2,
x3,
x4 being
set holds
{x1,x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
theorem :: ENUMSET1:91
for
x1 being
set holds
{x1,x1,x1,x1,x1,x1} = {x1}
theorem Th92: :: ENUMSET1:92
for
x1,
x2 being
set holds
{x1,x1,x1,x1,x1,x1,x2} = {x1,x2}
theorem Th93: :: ENUMSET1:93
for
x1,
x2,
x3 being
set holds
{x1,x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
theorem :: ENUMSET1:94
for
x1 being
set holds
{x1,x1,x1,x1,x1,x1,x1} = {x1}
theorem Th95: :: ENUMSET1:95
for
x1,
x2 being
set holds
{x1,x1,x1,x1,x1,x1,x1,x2} = {x1,x2}
theorem :: ENUMSET1:96
for
x1 being
set holds
{x1,x1,x1,x1,x1,x1,x1,x1} = {x1}
theorem :: ENUMSET1:97
canceled;
theorem Th98: :: ENUMSET1:98
for
x1,
x2,
x3 being
set holds
{x1,x2,x3} = {x1,x3,x2}
theorem Th99: :: ENUMSET1:99
for
x1,
x2,
x3 being
set holds
{x1,x2,x3} = {x2,x1,x3}
theorem Th100: :: ENUMSET1:100
for
x1,
x2,
x3 being
set holds
{x1,x2,x3} = {x2,x3,x1}
theorem :: ENUMSET1:101
canceled;
theorem Th102: :: ENUMSET1:102
for
x1,
x2,
x3 being
set holds
{x1,x2,x3} = {x3,x2,x1}
theorem Th103: :: ENUMSET1:103
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x1,x2,x4,x3}
theorem :: ENUMSET1:104
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x1,x3,x2,x4}
theorem Th105: :: ENUMSET1:105
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x1,x3,x4,x2}
theorem :: ENUMSET1:106
canceled;
theorem Th107: :: ENUMSET1:107
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x1,x4,x3,x2}
theorem Th108: :: ENUMSET1:108
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x2,x1,x3,x4}
Lm7:
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x3,x1,x4}
theorem :: ENUMSET1:109
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x2,x1,x4,x3}
theorem :: ENUMSET1:110
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x2,x3,x1,x4} by Lm7;
theorem :: ENUMSET1:111
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x2,x3,x4,x1}
theorem Th112: :: ENUMSET1:112
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x2,x4,x1,x3}
theorem :: ENUMSET1:113
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x2,x4,x3,x1}
Lm8:
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x2,x1,x4}
theorem :: ENUMSET1:114
canceled;
theorem :: ENUMSET1:115
canceled;
theorem :: ENUMSET1:116
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x3,x2,x1,x4} by Lm8;
theorem :: ENUMSET1:117
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x3,x2,x4,x1}
theorem :: ENUMSET1:118
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x3,x4,x1,x2}
theorem Th119: :: ENUMSET1:119
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x3,x4,x2,x1}
theorem :: ENUMSET1:120
canceled;
theorem :: ENUMSET1:121
canceled;
theorem :: ENUMSET1:122
canceled;
theorem :: ENUMSET1:123
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x4,x2,x3,x1}
theorem :: ENUMSET1:124
canceled;
theorem :: ENUMSET1:125
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x4,x3,x2,x1}
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}
theorem :: ENUMSET1:126
canceled;
theorem :: ENUMSET1:127
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}
theorem :: ENUMSET1:128
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}
theorem :: ENUMSET1:129
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}
theorem :: ENUMSET1:130
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} by Lm9;
theorem :: ENUMSET1:131
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}
theorem :: ENUMSET1:132
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}
theorem :: ENUMSET1:133
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}
theorem :: ENUMSET1:134
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}
theorem :: ENUMSET1:135
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}
theorem :: ENUMSET1:136
theorem :: ENUMSET1:137
for
x1,
x2,
x3 being
set holds
{x2,x1} \/ {x3,x1} = {x1,x2,x3}