enumset1.miz
begin
reserve x,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,y for
object,
X,Z for
set;
Lm1: x
in (
union
{X,
{y}}) iff x
in X or x
= y
proof
A1: x
in (
union
{X,
{y}}) implies x
in X or x
in
{y}
proof
assume x
in (
union
{X,
{y}});
then ex Z st x
in Z & Z
in
{X,
{y}} by
TARSKI:def 4;
hence thesis by
TARSKI:def 2;
end;
A2: x
in
{y} iff x
= y by
TARSKI:def 1;
X
in
{X,
{y}} &
{y}
in
{X,
{y}} by
TARSKI:def 2;
hence thesis by
A1,
A2,
TARSKI:def 4;
end;
definition
let x1,x2,x3 be
object;
::
ENUMSET1:def1
func
{x1,x2,x3} ->
set means
:
Def1: x
in it iff x
= x1 or x
= x2 or x
= x3;
existence
proof
take (
union
{
{x1, x2},
{x3}});
let x;
x
in
{x1, x2} iff x
= x1 or x
= x2 by
TARSKI:def 2;
hence thesis by
Lm1;
end;
uniqueness
proof
defpred
P[
object] means $1
= x1 or $1
= x2 or $1
= x3;
for X1,X2 be
set st (for x be
object holds x
in X1 iff
P[x]) & (for x be
object holds x
in X2 iff
P[x]) holds X1
= X2 from
XBOOLE_0:sch 3;
hence thesis;
end;
end
definition
let x1,x2,x3,x4 be
object;
::
ENUMSET1:def2
func
{x1,x2,x3,x4} ->
set means
:
Def2: x
in it iff x
= x1 or x
= x2 or x
= x3 or x
= x4;
existence
proof
take (
union
{
{x1, x2, x3},
{x4}});
let x;
x
in
{x1, x2, x3} iff x
= x1 or x
= x2 or x
= x3 by
Def1;
hence thesis by
Lm1;
end;
uniqueness
proof
defpred
P[
object] means $1
= x1 or $1
= x2 or $1
= x3 or $1
= x4;
for X1,X2 be
set st (for x be
object holds x
in X1 iff
P[x]) & (for x be
object holds x
in X2 iff
P[x]) holds X1
= X2 from
XBOOLE_0:sch 3;
hence thesis;
end;
end
definition
let x1,x2,x3,x4,x5 be
object;
::
ENUMSET1:def3
func
{x1,x2,x3,x4,x5} ->
set means
:
Def3: x
in it iff x
= x1 or x
= x2 or x
= x3 or x
= x4 or x
= x5;
existence
proof
take (
union
{
{x1, x2, x3, x4},
{x5}});
let x;
x
in
{x1, x2, x3, x4} iff x
= x1 or x
= x2 or x
= x3 or x
= x4 by
Def2;
hence thesis by
Lm1;
end;
uniqueness
proof
defpred
P[
object] means $1
= x1 or $1
= x2 or $1
= x3 or $1
= x4 or $1
= x5;
for X1,X2 be
set st (for x be
object holds x
in X1 iff
P[x]) & (for x be
object holds x
in X2 iff
P[x]) holds X1
= X2 from
XBOOLE_0:sch 3;
hence thesis;
end;
end
definition
let x1,x2,x3,x4,x5,x6 be
object;
::
ENUMSET1:def4
func
{x1,x2,x3,x4,x5,x6} ->
set means
:
Def4: x
in it iff x
= x1 or x
= x2 or x
= x3 or x
= x4 or x
= x5 or x
= x6;
existence
proof
take (
union
{
{x1, x2, x3, x4, x5},
{x6}});
let x;
x
in
{x1, x2, x3, x4, x5} iff x
= x1 or x
= x2 or x
= x3 or x
= x4 or x
= x5 by
Def3;
hence thesis by
Lm1;
end;
uniqueness
proof
defpred
P[
object] means $1
= x1 or $1
= x2 or $1
= x3 or $1
= x4 or $1
= x5 or $1
= x6;
for X1,X2 be
set st (for x be
object holds x
in X1 iff
P[x]) & (for x be
object holds x
in X2 iff
P[x]) holds X1
= X2 from
XBOOLE_0:sch 3;
hence thesis;
end;
end
definition
let x1,x2,x3,x4,x5,x6,x7 be
object;
::
ENUMSET1:def5
func
{x1,x2,x3,x4,x5,x6,x7} ->
set means
:
Def5: 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
proof
take (
union
{
{x1, x2, x3, x4, x5, x6},
{x7}});
let x;
x
in
{x1, x2, x3, x4, x5, x6} iff x
= x1 or x
= x2 or x
= x3 or x
= x4 or x
= x5 or x
= x6 by
Def4;
hence thesis by
Lm1;
end;
uniqueness
proof
defpred
P[
object] means $1
= x1 or $1
= x2 or $1
= x3 or $1
= x4 or $1
= x5 or $1
= x6 or $1
= x7;
for X1,X2 be
set st (for x be
object holds x
in X1 iff
P[x]) & (for x be
object holds x
in X2 iff
P[x]) holds X1
= X2 from
XBOOLE_0:sch 3;
hence thesis;
end;
end
definition
let x1,x2,x3,x4,x5,x6,x7,x8 be
object;
::
ENUMSET1:def6
func
{x1,x2,x3,x4,x5,x6,x7,x8} ->
set means
:
Def6: 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
proof
take (
union
{
{x1, x2, x3, x4, x5, x6, x7},
{x8}});
let x;
x
in
{x1, x2, x3, x4, x5, x6, x7} iff x
= x1 or x
= x2 or x
= x3 or x
= x4 or x
= x5 or x
= x6 or x
= x7 by
Def5;
hence thesis by
Lm1;
end;
uniqueness
proof
defpred
P[
object] means $1
= x1 or $1
= x2 or $1
= x3 or $1
= x4 or $1
= x5 or $1
= x6 or $1
= x7 or $1
= x8;
for X1,X2 be
set st (for x be
object holds x
in X1 iff
P[x]) & (for x be
object holds x
in X2 iff
P[x]) holds X1
= X2 from
XBOOLE_0:sch 3;
hence thesis;
end;
end
definition
let x1,x2,x3,x4,x5,x6,x7,x8,x9 be
object;
::
ENUMSET1:def7
func
{x1,x2,x3,x4,x5,x6,x7,x8,x9} ->
set means
:
Def7: 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
proof
take (
union
{
{x1, x2, x3, x4, x5, x6, x7, x8},
{x9}});
let x;
x
in
{x1, x2, x3, x4, x5, x6, x7, x8} iff x
= x1 or x
= x2 or x
= x3 or x
= x4 or x
= x5 or x
= x6 or x
= x7 or x
= x8 by
Def6;
hence thesis by
Lm1;
end;
uniqueness
proof
defpred
P[
object] means $1
= x1 or $1
= x2 or $1
= x3 or $1
= x4 or $1
= x5 or $1
= x6 or $1
= x7 or $1
= x8 or $1
= x9;
thus for X,Y be
set st (for x be
object holds x
in X iff
P[x]) & (for x be
object holds x
in Y iff
P[x]) holds X
= Y from
XBOOLE_0:sch 3;
end;
end
definition
let x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 be
object;
::
ENUMSET1:def8
func
{x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} ->
set means
:
Def8: 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
proof
take (
union
{
{x1, x2, x3, x4, x5, x6, x7, x8, x9},
{x10}});
let x;
x
in
{x1, x2, x3, x4, x5, x6, x7, x8, x9} 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 by
Def7;
hence thesis by
Lm1;
end;
uniqueness
proof
defpred
P[
object] means $1
= x1 or $1
= x2 or $1
= x3 or $1
= x4 or $1
= x5 or $1
= x6 or $1
= x7 or $1
= x8 or $1
= x9 or $1
= x10;
thus for X,Y be
set st (for x be
object holds x
in X iff
P[x]) & (for x be
object holds x
in Y iff
P[x]) holds X
= Y from
XBOOLE_0:sch 3;
end;
end
theorem ::
ENUMSET1:1
Th1:
{x1, x2}
= (
{x1}
\/
{x2})
proof
now
let x be
object;
x
in
{x1, x2} iff x
= x1 or x
= x2 by
TARSKI:def 2;
then x
in
{x1, x2} iff x
in
{x1} or x
in
{x2} by
TARSKI:def 1;
hence x
in
{x1, x2} iff x
in (
{x1}
\/
{x2}) by
XBOOLE_0:def 3;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ENUMSET1:2
Th2:
{x1, x2, x3}
= (
{x1}
\/
{x2, x3})
proof
now
let x be
object;
x
in
{x1, x2, x3} iff x
= x1 or x
= x2 or x
= x3 by
Def1;
then x
in
{x1, x2, x3} iff x
in
{x1} or x
in
{x2, x3} by
TARSKI:def 1,
TARSKI:def 2;
hence x
in
{x1, x2, x3} iff x
in (
{x1}
\/
{x2, x3}) by
XBOOLE_0:def 3;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ENUMSET1:3
Th3:
{x1, x2, x3}
= (
{x1, x2}
\/
{x3})
proof
thus
{x1, x2, x3}
= (
{x1}
\/
{x2, x3}) by
Th2
.= (
{x1}
\/ (
{x2}
\/
{x3})) by
Th1
.= ((
{x1}
\/
{x2})
\/
{x3}) by
XBOOLE_1: 4
.= (
{x1, x2}
\/
{x3}) by
Th1;
end;
Lm2:
{x1, x2, x3, x4}
= (
{x1, x2}
\/
{x3, x4})
proof
now
let x be
object;
x
in
{x1, x2, x3, x4} iff x
= x1 or x
= x2 or x
= x3 or x
= x4 by
Def2;
then x
in
{x1, x2, x3, x4} iff x
in
{x1, x2} or x
in
{x3, x4} by
TARSKI:def 2;
hence x
in
{x1, x2, x3, x4} iff x
in (
{x1, x2}
\/
{x3, x4}) by
XBOOLE_0:def 3;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ENUMSET1:4
Th4:
{x1, x2, x3, x4}
= (
{x1}
\/
{x2, x3, x4})
proof
thus
{x1, x2, x3, x4}
= (
{x1, x2}
\/
{x3, x4}) by
Lm2
.= ((
{x1}
\/
{x2})
\/
{x3, x4}) by
Th1
.= (
{x1}
\/ (
{x2}
\/
{x3, x4})) by
XBOOLE_1: 4
.= (
{x1}
\/
{x2, x3, x4}) by
Th2;
end;
theorem ::
ENUMSET1:5
{x1, x2, x3, x4}
= (
{x1, x2}
\/
{x3, x4}) by
Lm2;
theorem ::
ENUMSET1:6
Th6:
{x1, x2, x3, x4}
= (
{x1, x2, x3}
\/
{x4})
proof
thus
{x1, x2, x3, x4}
= (
{x1, x2}
\/
{x3, x4}) by
Lm2
.= (
{x1, x2}
\/ (
{x3}
\/
{x4})) by
Th1
.= ((
{x1, x2}
\/
{x3})
\/
{x4}) by
XBOOLE_1: 4
.= (
{x1, x2, x3}
\/
{x4}) by
Th3;
end;
Lm3:
{x1, x2, x3, x4, x5}
= (
{x1, x2, x3}
\/
{x4, x5})
proof
now
let x be
object;
x
in
{x1, x2, x3, x4, x5} iff x
= x1 or x
= x2 or x
= x3 or x
= x4 or x
= x5 by
Def3;
then x
in
{x1, x2, x3, x4, x5} iff x
in
{x1, x2, x3} or x
in
{x4, x5} by
Def1,
TARSKI:def 2;
hence x
in
{x1, x2, x3, x4, x5} iff x
in (
{x1, x2, x3}
\/
{x4, x5}) by
XBOOLE_0:def 3;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ENUMSET1:7
Th7:
{x1, x2, x3, x4, x5}
= (
{x1}
\/
{x2, x3, x4, x5})
proof
thus
{x1, x2, x3, x4, x5}
= (
{x1, x2, x3}
\/
{x4, x5}) by
Lm3
.= ((
{x1}
\/
{x2, x3})
\/
{x4, x5}) by
Th2
.= (
{x1}
\/ (
{x2, x3}
\/
{x4, x5})) by
XBOOLE_1: 4
.= (
{x1}
\/
{x2, x3, x4, x5}) by
Lm2;
end;
theorem ::
ENUMSET1:8
Th8:
{x1, x2, x3, x4, x5}
= (
{x1, x2}
\/
{x3, x4, x5})
proof
thus
{x1, x2, x3, x4, x5}
= (
{x1, x2, x3}
\/
{x4, x5}) by
Lm3
.= ((
{x1, x2}
\/
{x3})
\/
{x4, x5}) by
Th3
.= (
{x1, x2}
\/ (
{x3}
\/
{x4, x5})) by
XBOOLE_1: 4
.= (
{x1, x2}
\/
{x3, x4, x5}) by
Th2;
end;
theorem ::
ENUMSET1:9
{x1, x2, x3, x4, x5}
= (
{x1, x2, x3}
\/
{x4, x5}) by
Lm3;
theorem ::
ENUMSET1:10
Th10:
{x1, x2, x3, x4, x5}
= (
{x1, x2, x3, x4}
\/
{x5})
proof
thus
{x1, x2, x3, x4, x5}
= (
{x1, x2, x3}
\/
{x4, x5}) by
Lm3
.= (
{x1, x2, x3}
\/ (
{x4}
\/
{x5})) by
Th1
.= ((
{x1, x2, x3}
\/
{x4})
\/
{x5}) by
XBOOLE_1: 4
.= (
{x1, x2, x3, x4}
\/
{x5}) by
Th6;
end;
Lm4:
{x1, x2, x3, x4, x5, x6}
= (
{x1, x2, x3}
\/
{x4, x5, x6})
proof
now
let x be
object;
x
in
{x1, x2, x3, x4, x5, x6} iff x
= x1 or x
= x2 or x
= x3 or x
= x4 or x
= x5 or x
= x6 by
Def4;
then x
in
{x1, x2, x3, x4, x5, x6} iff x
in
{x1, x2, x3} or x
in
{x4, x5, x6} by
Def1;
hence x
in
{x1, x2, x3, x4, x5, x6} iff x
in (
{x1, x2, x3}
\/
{x4, x5, x6}) by
XBOOLE_0:def 3;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ENUMSET1:11
Th11:
{x1, x2, x3, x4, x5, x6}
= (
{x1}
\/
{x2, x3, x4, x5, x6})
proof
thus
{x1, x2, x3, x4, x5, x6}
= (
{x1, x2, x3}
\/
{x4, x5, x6}) by
Lm4
.= ((
{x1}
\/
{x2, x3})
\/
{x4, x5, x6}) by
Th2
.= (
{x1}
\/ (
{x2, x3}
\/
{x4, x5, x6})) by
XBOOLE_1: 4
.= (
{x1}
\/
{x2, x3, x4, x5, x6}) by
Th8;
end;
theorem ::
ENUMSET1:12
Th12:
{x1, x2, x3, x4, x5, x6}
= (
{x1, x2}
\/
{x3, x4, x5, x6})
proof
thus
{x1, x2, x3, x4, x5, x6}
= (
{x1, x2, x3}
\/
{x4, x5, x6}) by
Lm4
.= ((
{x1, x2}
\/
{x3})
\/
{x4, x5, x6}) by
Th3
.= (
{x1, x2}
\/ (
{x3}
\/
{x4, x5, x6})) by
XBOOLE_1: 4
.= (
{x1, x2}
\/
{x3, x4, x5, x6}) by
Th4;
end;
theorem ::
ENUMSET1:13
{x1, x2, x3, x4, x5, x6}
= (
{x1, x2, x3}
\/
{x4, x5, x6}) by
Lm4;
theorem ::
ENUMSET1:14
Th14:
{x1, x2, x3, x4, x5, x6}
= (
{x1, x2, x3, x4}
\/
{x5, x6})
proof
thus
{x1, x2, x3, x4, x5, x6}
= (
{x1, x2, x3}
\/
{x4, x5, x6}) by
Lm4
.= (
{x1, x2, x3}
\/ (
{x4}
\/
{x5, x6})) by
Th2
.= ((
{x1, x2, x3}
\/
{x4})
\/
{x5, x6}) by
XBOOLE_1: 4
.= (
{x1, x2, x3, x4}
\/
{x5, x6}) by
Th6;
end;
theorem ::
ENUMSET1:15
{x1, x2, x3, x4, x5, x6}
= (
{x1, x2, x3, x4, x5}
\/
{x6})
proof
thus
{x1, x2, x3, x4, x5, x6}
= (
{x1, x2, x3}
\/
{x4, x5, x6}) by
Lm4
.= (
{x1, x2, x3}
\/ (
{x4, x5}
\/
{x6})) by
Th3
.= ((
{x1, x2, x3}
\/
{x4, x5})
\/
{x6}) by
XBOOLE_1: 4
.= (
{x1, x2, x3, x4, x5}
\/
{x6}) by
Lm3;
end;
Lm5:
{x1, x2, x3, x4, x5, x6, x7}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7})
proof
now
let x be
object;
A1: x
in
{x5, x6, x7} iff x
= x5 or x
= x6 or x
= x7 by
Def1;
x
in
{x1, x2, x3, x4} iff x
= x1 or x
= x2 or x
= x3 or x
= x4 by
Def2;
hence x
in
{x1, x2, x3, x4, x5, x6, x7} iff x
in (
{x1, x2, x3, x4}
\/
{x5, x6, x7}) by
A1,
Def5,
XBOOLE_0:def 3;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ENUMSET1:16
Th16:
{x1, x2, x3, x4, x5, x6, x7}
= (
{x1}
\/
{x2, x3, x4, x5, x6, x7})
proof
thus
{x1, x2, x3, x4, x5, x6, x7}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7}) by
Lm5
.= ((
{x1}
\/
{x2, x3, x4})
\/
{x5, x6, x7}) by
Th4
.= (
{x1}
\/ (
{x2, x3, x4}
\/
{x5, x6, x7})) by
XBOOLE_1: 4
.= (
{x1}
\/
{x2, x3, x4, x5, x6, x7}) by
Lm4;
end;
theorem ::
ENUMSET1:17
Th17:
{x1, x2, x3, x4, x5, x6, x7}
= (
{x1, x2}
\/
{x3, x4, x5, x6, x7})
proof
thus
{x1, x2, x3, x4, x5, x6, x7}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7}) by
Lm5
.= ((
{x1, x2}
\/
{x3, x4})
\/
{x5, x6, x7}) by
Lm2
.= (
{x1, x2}
\/ (
{x3, x4}
\/
{x5, x6, x7})) by
XBOOLE_1: 4
.= (
{x1, x2}
\/
{x3, x4, x5, x6, x7}) by
Th8;
end;
theorem ::
ENUMSET1:18
Th18:
{x1, x2, x3, x4, x5, x6, x7}
= (
{x1, x2, x3}
\/
{x4, x5, x6, x7})
proof
thus
{x1, x2, x3, x4, x5, x6, x7}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7}) by
Lm5
.= ((
{x1, x2, x3}
\/
{x4})
\/
{x5, x6, x7}) by
Th6
.= (
{x1, x2, x3}
\/ (
{x4}
\/
{x5, x6, x7})) by
XBOOLE_1: 4
.= (
{x1, x2, x3}
\/
{x4, x5, x6, x7}) by
Th4;
end;
theorem ::
ENUMSET1:19
{x1, x2, x3, x4, x5, x6, x7}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7}) by
Lm5;
theorem ::
ENUMSET1:20
{x1, x2, x3, x4, x5, x6, x7}
= (
{x1, x2, x3, x4, x5}
\/
{x6, x7})
proof
thus
{x1, x2, x3, x4, x5, x6, x7}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7}) by
Lm5
.= (
{x1, x2, x3, x4}
\/ (
{x5}
\/
{x6, x7})) by
Th2
.= ((
{x1, x2, x3, x4}
\/
{x5})
\/
{x6, x7}) by
XBOOLE_1: 4
.= (
{x1, x2, x3, x4, x5}
\/
{x6, x7}) by
Th10;
end;
theorem ::
ENUMSET1:21
{x1, x2, x3, x4, x5, x6, x7}
= (
{x1, x2, x3, x4, x5, x6}
\/
{x7})
proof
thus
{x1, x2, x3, x4, x5, x6, x7}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7}) by
Lm5
.= (
{x1, x2, x3, x4}
\/ (
{x5, x6}
\/
{x7})) by
Th3
.= ((
{x1, x2, x3, x4}
\/
{x5, x6})
\/
{x7}) by
XBOOLE_1: 4
.= (
{x1, x2, x3, x4, x5, x6}
\/
{x7}) by
Th14;
end;
Lm6:
{x1, x2, x3, x4, x5, x6, x7, x8}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8})
proof
now
let x be
object;
A1: x
in
{x5, x6, x7, x8} iff x
= x5 or x
= x6 or x
= x7 or x
= x8 by
Def2;
x
in
{x1, x2, x3, x4} iff x
= x1 or x
= x2 or x
= x3 or x
= x4 by
Def2;
hence x
in
{x1, x2, x3, x4, x5, x6, x7, x8} iff x
in (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8}) by
A1,
Def6,
XBOOLE_0:def 3;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ENUMSET1:22
{x1, x2, x3, x4, x5, x6, x7, x8}
= (
{x1}
\/
{x2, x3, x4, x5, x6, x7, x8})
proof
thus
{x1, x2, x3, x4, x5, x6, x7, x8}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8}) by
Lm6
.= ((
{x1}
\/
{x2, x3, x4})
\/
{x5, x6, x7, x8}) by
Th4
.= (
{x1}
\/ (
{x2, x3, x4}
\/
{x5, x6, x7, x8})) by
XBOOLE_1: 4
.= (
{x1}
\/
{x2, x3, x4, x5, x6, x7, x8}) by
Th18;
end;
theorem ::
ENUMSET1:23
Th23:
{x1, x2, x3, x4, x5, x6, x7, x8}
= (
{x1, x2}
\/
{x3, x4, x5, x6, x7, x8})
proof
thus
{x1, x2, x3, x4, x5, x6, x7, x8}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8}) by
Lm6
.= ((
{x1, x2}
\/
{x3, x4})
\/
{x5, x6, x7, x8}) by
Lm2
.= (
{x1, x2}
\/ (
{x3, x4}
\/
{x5, x6, x7, x8})) by
XBOOLE_1: 4
.= (
{x1, x2}
\/
{x3, x4, x5, x6, x7, x8}) by
Th12;
end;
theorem ::
ENUMSET1:24
Th24:
{x1, x2, x3, x4, x5, x6, x7, x8}
= (
{x1, x2, x3}
\/
{x4, x5, x6, x7, x8})
proof
thus
{x1, x2, x3, x4, x5, x6, x7, x8}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8}) by
Lm6
.= ((
{x1, x2, x3}
\/
{x4})
\/
{x5, x6, x7, x8}) by
Th6
.= (
{x1, x2, x3}
\/ (
{x4}
\/
{x5, x6, x7, x8})) by
XBOOLE_1: 4
.= (
{x1, x2, x3}
\/
{x4, x5, x6, x7, x8}) by
Th7;
end;
theorem ::
ENUMSET1:25
{x1, x2, x3, x4, x5, x6, x7, x8}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8}) by
Lm6;
theorem ::
ENUMSET1:26
{x1, x2, x3, x4, x5, x6, x7, x8}
= (
{x1, x2, x3, x4, x5}
\/
{x6, x7, x8})
proof
thus
{x1, x2, x3, x4, x5, x6, x7, x8}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8}) by
Lm6
.= (
{x1, x2, x3, x4}
\/ (
{x5}
\/
{x6, x7, x8})) by
Th4
.= ((
{x1, x2, x3, x4}
\/
{x5})
\/
{x6, x7, x8}) by
XBOOLE_1: 4
.= (
{x1, x2, x3, x4, x5}
\/
{x6, x7, x8}) by
Th10;
end;
theorem ::
ENUMSET1:27
{x1, x2, x3, x4, x5, x6, x7, x8}
= (
{x1, x2, x3, x4, x5, x6}
\/
{x7, x8})
proof
thus
{x1, x2, x3, x4, x5, x6, x7, x8}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8}) by
Lm6
.= (
{x1, x2, x3, x4}
\/ (
{x5, x6}
\/
{x7, x8})) by
Lm2
.= ((
{x1, x2, x3, x4}
\/
{x5, x6})
\/
{x7, x8}) by
XBOOLE_1: 4
.= (
{x1, x2, x3, x4, x5, x6}
\/
{x7, x8}) by
Th14;
end;
theorem ::
ENUMSET1:28
{x1, x2, x3, x4, x5, x6, x7, x8}
= (
{x1, x2, x3, x4, x5, x6, x7}
\/
{x8})
proof
thus
{x1, x2, x3, x4, x5, x6, x7, x8}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8}) by
Lm6
.= (
{x1, x2, x3, x4}
\/ (
{x5, x6, x7}
\/
{x8})) by
Th6
.= ((
{x1, x2, x3, x4}
\/
{x5, x6, x7})
\/
{x8}) by
XBOOLE_1: 4
.= (
{x1, x2, x3, x4, x5, x6, x7}
\/
{x8}) by
Lm5;
end;
theorem ::
ENUMSET1:29
Th29:
{x1, x1}
=
{x1}
proof
now
let x be
object;
x
in
{x1, x1} iff x
= x1 by
TARSKI:def 2;
hence x
in
{x1, x1} iff x
in
{x1} by
TARSKI:def 1;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ENUMSET1:30
Th30:
{x1, x1, x2}
=
{x1, x2}
proof
thus
{x1, x1, x2}
= (
{x1, x1}
\/
{x2}) by
Th3
.= (
{x1}
\/
{x2}) by
Th29
.=
{x1, x2} by
Th1;
end;
theorem ::
ENUMSET1:31
Th31:
{x1, x1, x2, x3}
=
{x1, x2, x3}
proof
thus
{x1, x1, x2, x3}
= (
{x1, x1}
\/
{x2, x3}) by
Lm2
.= (
{x1}
\/
{x2, x3}) by
Th29
.=
{x1, x2, x3} by
Th2;
end;
theorem ::
ENUMSET1:32
Th32:
{x1, x1, x2, x3, x4}
=
{x1, x2, x3, x4}
proof
thus
{x1, x1, x2, x3, x4}
= (
{x1, x1}
\/
{x2, x3, x4}) by
Th8
.= (
{x1}
\/
{x2, x3, x4}) by
Th29
.=
{x1, x2, x3, x4} by
Th4;
end;
theorem ::
ENUMSET1:33
Th33:
{x1, x1, x2, x3, x4, x5}
=
{x1, x2, x3, x4, x5}
proof
thus
{x1, x1, x2, x3, x4, x5}
= (
{x1, x1}
\/
{x2, x3, x4, x5}) by
Th12
.= (
{x1}
\/
{x2, x3, x4, x5}) by
Th29
.=
{x1, x2, x3, x4, x5} by
Th7;
end;
theorem ::
ENUMSET1:34
Th34:
{x1, x1, x2, x3, x4, x5, x6}
=
{x1, x2, x3, x4, x5, x6}
proof
thus
{x1, x1, x2, x3, x4, x5, x6}
= (
{x1, x1}
\/
{x2, x3, x4, x5, x6}) by
Th17
.= (
{x1}
\/
{x2, x3, x4, x5, x6}) by
Th29
.=
{x1, x2, x3, x4, x5, x6} by
Th11;
end;
theorem ::
ENUMSET1:35
Th35:
{x1, x1, x2, x3, x4, x5, x6, x7}
=
{x1, x2, x3, x4, x5, x6, x7}
proof
thus
{x1, x1, x2, x3, x4, x5, x6, x7}
= (
{x1, x1}
\/
{x2, x3, x4, x5, x6, x7}) by
Th23
.= (
{x1}
\/
{x2, x3, x4, x5, x6, x7}) by
Th29
.=
{x1, x2, x3, x4, x5, x6, x7} by
Th16;
end;
theorem ::
ENUMSET1:36
{x1, x1, x1}
=
{x1}
proof
thus
{x1, x1, x1}
=
{x1, x1} by
Th30
.=
{x1} by
Th29;
end;
theorem ::
ENUMSET1:37
Th37:
{x1, x1, x1, x2}
=
{x1, x2}
proof
thus
{x1, x1, x1, x2}
=
{x1, x1, x2} by
Th31
.=
{x1, x2} by
Th30;
end;
theorem ::
ENUMSET1:38
Th38:
{x1, x1, x1, x2, x3}
=
{x1, x2, x3}
proof
thus
{x1, x1, x1, x2, x3}
=
{x1, x1, x2, x3} by
Th32
.=
{x1, x2, x3} by
Th31;
end;
theorem ::
ENUMSET1:39
Th39:
{x1, x1, x1, x2, x3, x4}
=
{x1, x2, x3, x4}
proof
thus
{x1, x1, x1, x2, x3, x4}
=
{x1, x1, x2, x3, x4} by
Th33
.=
{x1, x2, x3, x4} by
Th32;
end;
theorem ::
ENUMSET1:40
Th40:
{x1, x1, x1, x2, x3, x4, x5}
=
{x1, x2, x3, x4, x5}
proof
thus
{x1, x1, x1, x2, x3, x4, x5}
=
{x1, x1, x2, x3, x4, x5} by
Th34
.=
{x1, x2, x3, x4, x5} by
Th33;
end;
theorem ::
ENUMSET1:41
Th41:
{x1, x1, x1, x2, x3, x4, x5, x6}
=
{x1, x2, x3, x4, x5, x6}
proof
thus
{x1, x1, x1, x2, x3, x4, x5, x6}
=
{x1, x1, x2, x3, x4, x5, x6} by
Th35
.=
{x1, x2, x3, x4, x5, x6} by
Th34;
end;
theorem ::
ENUMSET1:42
{x1, x1, x1, x1}
=
{x1}
proof
thus
{x1, x1, x1, x1}
=
{x1, x1} by
Th37
.=
{x1} by
Th29;
end;
theorem ::
ENUMSET1:43
Th43:
{x1, x1, x1, x1, x2}
=
{x1, x2}
proof
thus
{x1, x1, x1, x1, x2}
=
{x1, x1, x2} by
Th38
.=
{x1, x2} by
Th30;
end;
theorem ::
ENUMSET1:44
Th44:
{x1, x1, x1, x1, x2, x3}
=
{x1, x2, x3}
proof
thus
{x1, x1, x1, x1, x2, x3}
=
{x1, x1, x2, x3} by
Th39
.=
{x1, x2, x3} by
Th31;
end;
theorem ::
ENUMSET1:45
Th45:
{x1, x1, x1, x1, x2, x3, x4}
=
{x1, x2, x3, x4}
proof
thus
{x1, x1, x1, x1, x2, x3, x4}
=
{x1, x1, x2, x3, x4} by
Th40
.=
{x1, x2, x3, x4} by
Th32;
end;
theorem ::
ENUMSET1:46
Th46:
{x1, x1, x1, x1, x2, x3, x4, x5}
=
{x1, x2, x3, x4, x5}
proof
thus
{x1, x1, x1, x1, x2, x3, x4, x5}
=
{x1, x1, x2, x3, x4, x5} by
Th41
.=
{x1, x2, x3, x4, x5} by
Th33;
end;
theorem ::
ENUMSET1:47
{x1, x1, x1, x1, x1}
=
{x1}
proof
thus
{x1, x1, x1, x1, x1}
=
{x1, x1} by
Th43
.=
{x1} by
Th29;
end;
theorem ::
ENUMSET1:48
Th48:
{x1, x1, x1, x1, x1, x2}
=
{x1, x2}
proof
thus
{x1, x1, x1, x1, x1, x2}
=
{x1, x1, x2} by
Th44
.=
{x1, x2} by
Th30;
end;
theorem ::
ENUMSET1:49
Th49:
{x1, x1, x1, x1, x1, x2, x3}
=
{x1, x2, x3}
proof
thus
{x1, x1, x1, x1, x1, x2, x3}
=
{x1, x1, x2, x3} by
Th45
.=
{x1, x2, x3} by
Th31;
end;
theorem ::
ENUMSET1:50
Th50:
{x1, x1, x1, x1, x1, x2, x3, x4}
=
{x1, x2, x3, x4}
proof
thus
{x1, x1, x1, x1, x1, x2, x3, x4}
=
{x1, x1, x2, x3, x4} by
Th46
.=
{x1, x2, x3, x4} by
Th32;
end;
theorem ::
ENUMSET1:51
{x1, x1, x1, x1, x1, x1}
=
{x1}
proof
thus
{x1, x1, x1, x1, x1, x1}
=
{x1, x1} by
Th48
.=
{x1} by
Th29;
end;
theorem ::
ENUMSET1:52
Th52:
{x1, x1, x1, x1, x1, x1, x2}
=
{x1, x2}
proof
thus
{x1, x1, x1, x1, x1, x1, x2}
=
{x1, x1, x2} by
Th49
.=
{x1, x2} by
Th30;
end;
theorem ::
ENUMSET1:53
Th53:
{x1, x1, x1, x1, x1, x1, x2, x3}
=
{x1, x2, x3}
proof
thus
{x1, x1, x1, x1, x1, x1, x2, x3}
=
{x1, x1, x2, x3} by
Th50
.=
{x1, x2, x3} by
Th31;
end;
theorem ::
ENUMSET1:54
{x1, x1, x1, x1, x1, x1, x1}
=
{x1}
proof
thus
{x1, x1, x1, x1, x1, x1, x1}
=
{x1, x1} by
Th52
.=
{x1} by
Th29;
end;
theorem ::
ENUMSET1:55
Th55:
{x1, x1, x1, x1, x1, x1, x1, x2}
=
{x1, x2}
proof
thus
{x1, x1, x1, x1, x1, x1, x1, x2}
=
{x1, x1, x2} by
Th53
.=
{x1, x2} by
Th30;
end;
theorem ::
ENUMSET1:56
{x1, x1, x1, x1, x1, x1, x1, x1}
=
{x1}
proof
thus
{x1, x1, x1, x1, x1, x1, x1, x1}
=
{x1, x1} by
Th55
.=
{x1} by
Th29;
end;
theorem ::
ENUMSET1:57
Th57:
{x1, x2, x3}
=
{x1, x3, x2}
proof
thus
{x1, x2, x3}
= (
{x1}
\/
{x2, x3}) by
Th2
.=
{x1, x3, x2} by
Th2;
end;
theorem ::
ENUMSET1:58
Th58:
{x1, x2, x3}
=
{x2, x1, x3}
proof
thus
{x1, x2, x3}
= (
{x1, x2}
\/
{x3}) by
Th3
.=
{x2, x1, x3} by
Th3;
end;
theorem ::
ENUMSET1:59
Th59:
{x1, x2, x3}
=
{x2, x3, x1}
proof
thus
{x1, x2, x3}
= (
{x2, x3}
\/
{x1}) by
Th2
.=
{x2, x3, x1} by
Th3;
end;
theorem ::
ENUMSET1:60
Th60:
{x1, x2, x3}
=
{x3, x2, x1}
proof
thus
{x1, x2, x3}
=
{x3, x1, x2} by
Th59
.=
{x3, x2, x1} by
Th57;
end;
theorem ::
ENUMSET1:61
Th61:
{x1, x2, x3, x4}
=
{x1, x2, x4, x3}
proof
thus
{x1, x2, x3, x4}
= (
{x1}
\/
{x2, x3, x4}) by
Th4
.= (
{x1}
\/
{x2, x4, x3}) by
Th57
.=
{x1, x2, x4, x3} by
Th4;
end;
theorem ::
ENUMSET1:62
{x1, x2, x3, x4}
=
{x1, x3, x2, x4}
proof
thus
{x1, x2, x3, x4}
= (
{x1}
\/
{x2, x3, x4}) by
Th4
.= (
{x1}
\/
{x3, x2, x4}) by
Th58
.=
{x1, x3, x2, x4} by
Th4;
end;
theorem ::
ENUMSET1:63
Th63:
{x1, x2, x3, x4}
=
{x1, x3, x4, x2}
proof
thus
{x1, x2, x3, x4}
= (
{x1}
\/
{x2, x3, x4}) by
Th4
.= (
{x1}
\/
{x3, x4, x2}) by
Th59
.=
{x1, x3, x4, x2} by
Th4;
end;
theorem ::
ENUMSET1:64
Th64:
{x1, x2, x3, x4}
=
{x1, x4, x3, x2}
proof
thus
{x1, x2, x3, x4}
= (
{x1}
\/
{x2, x3, x4}) by
Th4
.= (
{x1}
\/
{x4, x3, x2}) by
Th60
.=
{x1, x4, x3, x2} by
Th4;
end;
theorem ::
ENUMSET1:65
Th65:
{x1, x2, x3, x4}
=
{x2, x1, x3, x4}
proof
thus
{x1, x2, x3, x4}
= (
{x1, x2, x3}
\/
{x4}) by
Th6
.= (
{x2, x1, x3}
\/
{x4}) by
Th58
.=
{x2, x1, x3, x4} by
Th6;
end;
Lm7:
{x1, x2, x3, x4}
=
{x2, x3, x1, x4}
proof
thus
{x1, x2, x3, x4}
= (
{x1, x2, x3}
\/
{x4}) by
Th6
.= (
{x2, x3, x1}
\/
{x4}) by
Th59
.=
{x2, x3, x1, x4} by
Th6;
end;
theorem ::
ENUMSET1:66
{x1, x2, x3, x4}
=
{x2, x1, x4, x3}
proof
thus
{x1, x2, x3, x4}
=
{x2, x3, x1, x4} by
Lm7
.=
{x2, x1, x4, x3} by
Th63;
end;
theorem ::
ENUMSET1:67
{x1, x2, x3, x4}
=
{x2, x3, x1, x4} by
Lm7;
theorem ::
ENUMSET1:68
{x1, x2, x3, x4}
=
{x2, x3, x4, x1}
proof
thus
{x1, x2, x3, x4}
=
{x2, x3, x1, x4} by
Lm7
.=
{x2, x3, x4, x1} by
Th61;
end;
theorem ::
ENUMSET1:69
Th69:
{x1, x2, x3, x4}
=
{x2, x4, x1, x3}
proof
thus
{x1, x2, x3, x4}
=
{x2, x3, x1, x4} by
Lm7
.=
{x2, x4, x1, x3} by
Th64;
end;
theorem ::
ENUMSET1:70
{x1, x2, x3, x4}
=
{x2, x4, x3, x1}
proof
thus
{x1, x2, x3, x4}
=
{x2, x3, x1, x4} by
Lm7
.=
{x2, x4, x3, x1} by
Th63;
end;
Lm8:
{x1, x2, x3, x4}
=
{x3, x2, x1, x4}
proof
thus
{x1, x2, x3, x4}
= (
{x1, x2, x3}
\/
{x4}) by
Th6
.= (
{x3, x2, x1}
\/
{x4}) by
Th60
.=
{x3, x2, x1, x4} by
Th6;
end;
theorem ::
ENUMSET1:71
{x1, x2, x3, x4}
=
{x3, x2, x1, x4} by
Lm8;
theorem ::
ENUMSET1:72
{x1, x2, x3, x4}
=
{x3, x2, x4, x1}
proof
thus
{x1, x2, x3, x4}
=
{x3, x2, x1, x4} by
Lm8
.=
{x3, x2, x4, x1} by
Th61;
end;
theorem ::
ENUMSET1:73
{x1, x2, x3, x4}
=
{x3, x4, x1, x2}
proof
thus
{x1, x2, x3, x4}
=
{x3, x2, x1, x4} by
Lm8
.=
{x3, x4, x1, x2} by
Th64;
end;
theorem ::
ENUMSET1:74
Th74:
{x1, x2, x3, x4}
=
{x3, x4, x2, x1}
proof
thus
{x1, x2, x3, x4}
=
{x3, x2, x1, x4} by
Lm8
.=
{x3, x4, x2, x1} by
Th63;
end;
theorem ::
ENUMSET1:75
{x1, x2, x3, x4}
=
{x4, x2, x3, x1}
proof
thus
{x1, x2, x3, x4}
=
{x3, x4, x2, x1} by
Th74
.=
{x4, x2, x3, x1} by
Lm7;
end;
theorem ::
ENUMSET1:76
{x1, x2, x3, x4}
=
{x4, x3, x2, x1}
proof
thus
{x1, x2, x3, x4}
=
{x3, x4, x2, x1} by
Th74
.=
{x4, x3, x2, x1} by
Th65;
end;
Lm9:
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8, x9})
proof
now
let x be
object;
A1: x
in
{x5, x6, x7, x8, x9} iff x
= x5 or x
= x6 or x
= x7 or x
= x8 or x
= x9 by
Def3;
x
in
{x1, x2, x3, x4} iff x
= x1 or x
= x2 or x
= x3 or x
= x4 by
Def2;
hence x
in
{x1, x2, x3, x4, x5, x6, x7, x8, x9} iff x
in (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8, x9}) by
A1,
Def7,
XBOOLE_0:def 3;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ENUMSET1:77
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
= (
{x1}
\/
{x2, x3, x4, x5, x6, x7, x8, x9})
proof
thus
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8, x9}) by
Lm9
.= ((
{x1}
\/
{x2, x3, x4})
\/
{x5, x6, x7, x8, x9}) by
Th4
.= (
{x1}
\/ (
{x2, x3, x4}
\/
{x5, x6, x7, x8, x9})) by
XBOOLE_1: 4
.= (
{x1}
\/
{x2, x3, x4, x5, x6, x7, x8, x9}) by
Th24;
end;
theorem ::
ENUMSET1:78
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
= (
{x1, x2}
\/
{x3, x4, x5, x6, x7, x8, x9})
proof
thus
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8, x9}) by
Lm9
.= ((
{x1, x2}
\/
{x3, x4})
\/
{x5, x6, x7, x8, x9}) by
Lm2
.= (
{x1, x2}
\/ (
{x3, x4}
\/
{x5, x6, x7, x8, x9})) by
XBOOLE_1: 4
.= (
{x1, x2}
\/
{x3, x4, x5, x6, x7, x8, x9}) by
Th17;
end;
theorem ::
ENUMSET1:79
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
= (
{x1, x2, x3}
\/
{x4, x5, x6, x7, x8, x9})
proof
thus
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8, x9}) by
Lm9
.= ((
{x1, x2, x3}
\/
{x4})
\/
{x5, x6, x7, x8, x9}) by
Th6
.= (
{x1, x2, x3}
\/ (
{x4}
\/
{x5, x6, x7, x8, x9})) by
XBOOLE_1: 4
.= (
{x1, x2, x3}
\/
{x4, x5, x6, x7, x8, x9}) by
Th11;
end;
theorem ::
ENUMSET1:80
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8, x9}) by
Lm9;
theorem ::
ENUMSET1:81
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
= (
{x1, x2, x3, x4, x5}
\/
{x6, x7, x8, x9})
proof
thus
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8, x9}) by
Lm9
.= (
{x1, x2, x3, x4}
\/ (
{x5}
\/
{x6, x7, x8, x9})) by
Th7
.= ((
{x1, x2, x3, x4}
\/
{x5})
\/
{x6, x7, x8, x9}) by
XBOOLE_1: 4
.= (
{x1, x2, x3, x4, x5}
\/
{x6, x7, x8, x9}) by
Th10;
end;
theorem ::
ENUMSET1:82
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
= (
{x1, x2, x3, x4, x5, x6}
\/
{x7, x8, x9})
proof
thus
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8, x9}) by
Lm9
.= (
{x1, x2, x3, x4}
\/ (
{x5, x6}
\/
{x7, x8, x9})) by
Th8
.= ((
{x1, x2, x3, x4}
\/
{x5, x6})
\/
{x7, x8, x9}) by
XBOOLE_1: 4
.= (
{x1, x2, x3, x4, x5, x6}
\/
{x7, x8, x9}) by
Th14;
end;
theorem ::
ENUMSET1:83
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
= (
{x1, x2, x3, x4, x5, x6, x7}
\/
{x8, x9})
proof
thus
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8, x9}) by
Lm9
.= (
{x1, x2, x3, x4}
\/ (
{x5, x6, x7}
\/
{x8, x9})) by
Lm3
.= ((
{x1, x2, x3, x4}
\/
{x5, x6, x7})
\/
{x8, x9}) by
XBOOLE_1: 4
.= (
{x1, x2, x3, x4, x5, x6, x7}
\/
{x8, x9}) by
Lm5;
end;
theorem ::
ENUMSET1:84
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
= (
{x1, x2, x3, x4, x5, x6, x7, x8}
\/
{x9})
proof
thus
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
= (
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8, x9}) by
Lm9
.= (
{x1, x2, x3, x4}
\/ (
{x5, x6, x7, x8}
\/
{x9})) by
Th10
.= ((
{x1, x2, x3, x4}
\/
{x5, x6, x7, x8})
\/
{x9}) by
XBOOLE_1: 4
.= (
{x1, x2, x3, x4, x5, x6, x7, x8}
\/
{x9}) by
Lm6;
end;
theorem ::
ENUMSET1:85
{x1, x2, x3, x4, x5, x6, x7, x8, x9, x10}
= (
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
\/
{x10})
proof
now
let x be
object;
A1: x
in
{x10} iff x
= x10 by
TARSKI:def 1;
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 iff x
in
{x1, x2, x3, x4, x5, x6, x7, x8, x9} or x
= x10 by
Def7;
hence x
in
{x1, x2, x3, x4, x5, x6, x7, x8, x9, x10} iff x
in (
{x1, x2, x3, x4, x5, x6, x7, x8, x9}
\/
{x10}) by
A1,
Def8,
XBOOLE_0:def 3;
end;
hence thesis by
TARSKI: 2;
end;
begin
theorem ::
ENUMSET1:86
for x,y,z be
set st x
<> y & x
<> z holds (
{x, y, z}
\
{x})
=
{y, z}
proof
let x,y,z be
set such that
A1: x
<> y & x
<> z;
hereby
let a be
object;
assume
A2: a
in (
{x, y, z}
\
{x});
then a
in
{x, y, z} by
XBOOLE_0:def 5;
then
A3: a
= x or a
= y or a
= z by
Def1;
not a
in
{x} by
A2,
XBOOLE_0:def 5;
hence a
in
{y, z} by
A3,
TARSKI:def 1,
TARSKI:def 2;
end;
let a be
object;
assume a
in
{y, z};
then
A4: a
= y or a
= z by
TARSKI:def 2;
then
A5: not a
in
{x} by
A1,
TARSKI:def 1;
a
in
{x, y, z} by
A4,
Def1;
hence thesis by
A5,
XBOOLE_0:def 5;
end;
theorem ::
ENUMSET1:87
for x1,x2,x3 be
set holds (
{x2, x1}
\/
{x3, x1})
=
{x1, x2, x3}
proof
let x1,x2,x3 be
set;
thus (
{x2, x1}
\/
{x3, x1})
=
{x2, x1, x3, x1} by
Lm2
.=
{x1, x1, x2, x3} by
Th69
.=
{x1, x2, x3} by
Th31;
end;