Copyright (c) 1989 Association of Mizar Users
environ
vocabulary TARSKI, BOOLE;
notation TARSKI, XBOOLE_0;
constructors TARSKI, XBOOLE_0;
clusters XBOOLE_0;
theorems TARSKI, XBOOLE_0, XBOOLE_1;
schemes 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 A1: for x1 holds P[x1] by A1;
scheme UI2{x1, x2()->set,P[set,set]}:
P[x1(),x2()]
provided A1: for x1,x2 holds P[x1,x2] by A1;
scheme UI3{x1, x2, x3()->set,P[set,set,set]}:
P[x1(),x2(),x3()]
provided A1: for x1,x2,x3 holds P[x1,x2,x3] by A1;
scheme UI4{x1, x2, x3, x4()->set,P[set,set,set,set]}:
P[x1(),x2(),x3(),x4()]
provided A1: for x1,x2,x3,x4 holds P[x1,x2,x3,x4] by A1;
scheme UI5
{x1, x2, x3, x4, x5()->set, P[set,set,set,set,set]}:
P[x1(),x2(),x3(),x4(),x5()]
provided A1: for x1,x2,x3,x4,x5 holds P[x1,x2,x3,x4,x5] by A1;
scheme UI6
{x1, x2, x3, x4, x5, x6()->set,
P[set,set,set,set,set,set]}:
P[x1(),x2(),x3(),x4(),x5(),x6()]
provided A1: for x1,x2,x3,x4,x5,x6 holds P[x1,x2,x3,x4,x5,x6] by A1;
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 A1: for x1,x2,x3,x4,x5,x6,x7 holds P[x1,x2,x3,x4,x5,x6,x7] by A1;
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 A1: for x1,x2,x3,x4,x5,x6,x7,x8 holds P[x1,x2,x3,x4,x5,x6,x7,x8] by A1
;
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
A1: for x1,x2,x3,x4,x5,x6,x7,x8,x9 being set
holds P[x1,x2,x3,x4,x5,x6,x7,x8,x9] by A1;
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 {X,{y}} & {y} in {X,{y}} by TARSKI:def 2;
x in {y} iff x=y by TARSKI:def 1;
hence thesis by A1,A2,TARSKI:def 4;
end;
definition let x1,x2,x3;
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[set] means $1=x1 or $1=x2 or $1=x3;
for X1,X2 being set st
(for x being set holds x in X1 iff P[x]) &
(for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
hence thesis;
end;
end;
canceled 12;
theorem
x in { x1,x2,x3 } implies x=x1 or x=x2 or x=x3 by Def1;
theorem
x=x1 or x=x2 or x=x3 implies x in { x1,x2,x3 } by Def1;
theorem
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 } by Def1;
definition
let x1,x2,x3,x4;
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[set] means $1=x1 or $1=x2 or $1=x3 or $1=x4;
for X1,X2 being set st
(for x being set holds x in X1 iff P[x]) &
(for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
hence thesis;
end;
end;
Lm2:
x in { x1,x2,x3,x4 } iff x=x1 or x=x2 or x=x3 or x = x4 by Def2;
canceled 2;
theorem
x in { x1,x2,x3,x4 } implies x=x1 or x=x2 or x=x3 or x = x4 by Def2;
theorem
x=x1 or x=x2 or x=x3 or x = x4 implies x in { x1,x2,x3,x4 } by Def2;
theorem
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 } by Def2;
definition
let x1,x2,x3,x4,x5;
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 Lm2;
hence thesis by Lm1;
end;
uniqueness
proof
defpred P[set] means $1=x1 or $1=x2 or $1=x3 or $1=x4 or $1=x5;
for X1,X2 being set st
(for x being set holds x in X1 iff P[x]) &
(for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
hence thesis;
end;
end;
Lm3:
x in { x1,x2,x3,x4,x5 } iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5
proof
defpred P[set,set,set,set,set] means
for X being set holds X = { $1,$2,$3,$4,$5 } iff
for x holds x in
X iff x=$1 or x=$2 or x=$3 or x=$4 or x=$5;
A1: for x1,x2,x3,x4,x5 holds P[x1,x2,x3,x4,x5] by Def3;
P[x1,x2,x3,x4,x5] from UI5(A1);
hence thesis;
end;
canceled 2;
theorem
x in { x1,x2,x3,x4,x5 } implies x=x1 or x=x2 or x=x3 or x=x4 or x=x5
by Lm3;
theorem
x=x1 or x=x2 or x=x3 or x=x4 or x=x5 implies x in
{ x1,x2,x3,x4,x5 } by Def3;
theorem
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 } by Def3;
definition
let x1,x2,x3,x4,x5,x6;
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 Lm3;
hence thesis by Lm1;
end;
uniqueness
proof
defpred P[set] means $1=x1 or $1=x2 or $1=x3 or $1=x4 or $1=x5 or $1=x6;
for X1,X2 being set st
(for x being set holds x in X1 iff P[x]) &
(for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
hence thesis;
end;
end;
Lm4:
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
proof
defpred P[set,set,set,set,set,set] means
for X being set holds X = { $1,$2,$3,$4,$5,$6 } iff
for x holds x in
X iff x=$1 or x=$2 or x=$3 or x=$4 or x=$5 or x = $6;
A1: for x1,x2,x3,x4,x5,x6 holds P[x1,x2,x3,x4,x5,x6] by Def4;
P[x1,x2,x3,x4,x5,x6] from UI6(A1);
hence thesis;
end;
canceled 2;
theorem
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
proof
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 Lm4;
hence thesis;
end;
theorem
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 } by Lm4;
theorem
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 } by Def4;
definition
let x1,x2,x3,x4,x5,x6,x7;
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 Lm4;
hence thesis by Lm1;
end;
uniqueness
proof
defpred P[set] means $1=x1 or $1=x2 or $1=x3 or
$1=x4 or $1=x5 or $1=x6 or $1=x7;
for X1,X2 being set st
(for x being set holds x in X1 iff P[x]) &
(for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
hence thesis;
end;
end;
Lm5:
for x1,x2,x3,x4,x5,x6,x7 for X being set holds
X = { x1,x2,x3,x4,x5,x6,x7 } iff
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
proof
defpred P[set,set,set,set,set,set,set] means
for X being set holds X = { $1,$2,$3,$4,$5,$6,$7 } iff
for x holds x in
X iff x=$1 or x=$2 or x=$3 or x=$4 or x=$5 or x = $6 or x = $7;
A1: for x1,x2,x3,x4,x5,x6,x7 holds P[x1,x2,x3,x4,x5,x6,x7] by Def5;
let x1,x2,x3,x4,x5,x6,x7;
P[x1,x2,x3,x4,x5,x6,x7] from UI7(A1);
hence thesis;
end;
Lm6:
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
proof
defpred P[set,set,set,set,set,set,set] means
for X being set holds X = { $1,$2,$3,$4,$5,$6,$7 } iff
for x holds x in
X iff x=$1 or x=$2 or x=$3 or x=$4 or x=$5 or x = $6 or x = $7;
A1: for x1,x2,x3,x4,x5,x6,x7 holds P[x1,x2,x3,x4,x5,x6,x7] by Def5;
P[x1,x2,x3,x4,x5,x6,x7] from UI7(A1);
hence thesis;
end;
canceled 2;
theorem
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
proof
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 Lm6;
hence thesis;
end;
theorem
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 } by Lm6;
theorem
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 } by Lm5;
definition
let x1,x2,x3,x4,x5,x6,x7,x8;
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 Lm6;
hence thesis by Lm1;
end;
uniqueness
proof
defpred P[set] 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 being set st
(for x being set holds x in X1 iff P[x]) &
(for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
hence thesis;
end;
end;
Lm7:
for x1,x2,x3,x4,x5,x6,x7,x8 for X being set holds
X = { x1,x2,x3,x4,x5,x6,x7,x8 } iff
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
proof
defpred P[set,set,set,set,set,set,set,set] means
for X being set holds X = { $1,$2,$3,$4,$5,$6,$7,$8 } iff
for x holds x in
X iff x=$1 or x=$2 or x=$3 or x=$4 or x=$5 or x = $6 or x = $7 or x = $8;
A1: for x1,x2,x3,x4,x5,x6,x7,x8 holds P[x1,x2,x3,x4,x5,x6,x7,x8] by Def6;
let x1,x2,x3,x4,x5,x6,x7,x8;
P[x1,x2,x3,x4,x5,x6,x7,x8] from UI8(A1);
hence thesis;
end;
Lm8:
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
proof
defpred P[set,set,set,set,set,set,set,set] means
for X being set holds X = { $1,$2,$3,$4,$5,$6,$7,$8 } iff
for x holds x in
X iff x=$1 or x=$2 or x=$3 or x=$4 or x=$5 or x = $6 or x = $7 or x = $8;
A1: for x1,x2,x3,x4,x5,x6,x7,x8 holds P[x1,x2,x3,x4,x5,x6,x7,x8] by Def6;
P[x1,x2,x3,x4,x5,x6,x7,x8] from UI8(A1);
hence thesis;
end;
canceled 2;
theorem
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
proof
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 Lm8;
hence thesis;
end;
theorem
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 } by Lm8;
theorem
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 } by Lm7;
theorem Th41:
{ x1,x2 } = { x1 } \/ { x2 }
proof
now let x;
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 2;
end;
hence thesis by TARSKI:2;
end;
theorem Th42:
{ x1,x2,x3 } = { x1 } \/ { x2,x3 }
proof
now let x;
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,
def 2;
hence x in { x1,x2,x3 } iff x in { x1 } \/ { x2,x3 } by XBOOLE_0:def 2;
end;
hence thesis by TARSKI:2;
end;
theorem Th43:
{ x1,x2,x3 } = { x1,x2 } \/ { x3 }
proof
thus { x1,x2,x3 } = { x1 } \/ { x2,x3 } by Th42
.= { x1 } \/ ({ x2 } \/ { x3 }) by Th41
.= { x1 } \/ { x2 } \/ { x3 } by XBOOLE_1:4
.= { x1,x2 } \/ { x3 } by Th41;
end;
Lm9: { x1,x2,x3,x4 } = { x1,x2 } \/ { x3,x4 }
proof
now let x;
x in { x1,x2,x3,x4 } iff
x=x1 or x=x2 or x=x3 or x=x4 by Lm2;
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 2;
end;
hence thesis by TARSKI:2;
end;
theorem Th44:
{ x1,x2,x3,x4 } = { x1 } \/ { x2,x3,x4 }
proof
thus { x1,x2,x3,x4 } = { x1,x2 } \/ { x3,x4 } by Lm9
.= { x1 } \/ { x2 } \/ { x3,x4 } by Th41
.= { x1 } \/ ({ x2 } \/ { x3,x4 }) by XBOOLE_1:4
.= { x1 } \/ { x2,x3,x4 } by Th42;
end;
theorem
{ x1,x2,x3,x4 } = { x1,x2 } \/ { x3,x4 } by Lm9;
theorem Th46:
{ x1,x2,x3,x4 } = { x1,x2,x3 } \/ { x4 }
proof
thus { x1,x2,x3,x4 } = { x1,x2 } \/ { x3,x4 } by Lm9
.= { x1,x2 } \/ ({ x3 } \/ { x4 }) by Th41
.= { x1,x2 } \/ { x3 } \/ { x4 } by XBOOLE_1:4
.= { x1,x2,x3 } \/ { x4 } by Th43;
end;
Lm10: { x1,x2,x3,x4,x5 } = { x1,x2,x3 } \/ { x4,x5 }
proof
now 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 Lm3;
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 2;
end;
hence thesis by TARSKI:2;
end;
theorem Th47:
{ x1,x2,x3,x4,x5 } = { x1 } \/ { x2,x3,x4,x5 }
proof
thus { x1,x2,x3,x4,x5 } = { x1,x2,x3 } \/ { x4,x5 } by Lm10
.= { x1 } \/ { x2,x3 } \/ { x4,x5 } by Th42
.= { x1 } \/ ({ x2,x3 } \/ { x4,x5 }) by XBOOLE_1:4
.= { x1 } \/ { x2,x3,x4,x5 } by Lm9;
end;
theorem Th48:
{ x1,x2,x3,x4,x5 } = { x1,x2 } \/ { x3,x4,x5 }
proof
thus { x1,x2,x3,x4,x5 } = { x1,x2,x3 } \/ { x4,x5 } by Lm10
.= { x1,x2 } \/ { x3 } \/ { x4,x5 } by Th43
.= { x1,x2 } \/ ({ x3 } \/ { x4,x5 }) by XBOOLE_1:4
.= { x1,x2 } \/ { x3,x4,x5 } by Th42;
end;
theorem
{ x1,x2,x3,x4,x5 } = { x1,x2,x3 } \/ { x4,x5 } by Lm10;
theorem Th50:
{ x1,x2,x3,x4,x5 } = { x1,x2,x3,x4 } \/ { x5 }
proof
thus { x1,x2,x3,x4,x5 } = { x1,x2,x3 } \/ { x4,x5 } by Lm10
.= { x1,x2,x3 } \/ ({ x4 } \/ { x5 }) by Th41
.= { x1,x2,x3 } \/ { x4 } \/ { x5 } by XBOOLE_1:4
.= { x1,x2,x3,x4 } \/ { x5 } by Th46;
end;
Lm11: { x1,x2,x3,x4,x5,x6 } = { x1,x2,x3 } \/ { x4,x5,x6 }
proof
now 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 Lm4;
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 2;
end;
hence thesis by TARSKI:2;
end;
theorem Th51:
{ 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 Lm11
.= { x1 } \/ { x2,x3 } \/ { x4,x5,x6 } by Th42
.= { x1 } \/ ({ x2,x3 } \/
{ x4,x5,x6 }) by XBOOLE_1:4
.= { x1 } \/ { x2,x3,x4,x5,x6 } by Th48;
end;
theorem Th52:
{ 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 Lm11
.= { x1,x2 } \/ { x3 } \/ { x4,x5,x6 } by Th43
.= { x1,x2 } \/ ({ x3 } \/
{ x4,x5,x6 }) by XBOOLE_1:4
.= { x1,x2 } \/ { x3,x4,x5,x6 } by Th44;
end;
theorem
{ x1,x2,x3,x4,x5,x6 } = { x1,x2,x3 } \/ { x4,x5,x6 } by Lm11;
theorem Th54:
{ 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 Lm11
.= { x1,x2,x3 } \/ ({ x4 } \/ { x5,x6 }) by Th42
.= { x1,x2,x3 } \/ { x4 } \/ { x5,x6 }
by XBOOLE_1:4
.= { x1,x2,x3,x4 } \/ { x5,x6 } by Th46;
end;
theorem
{ 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 Lm11
.= { x1,x2,x3 } \/ ({ x4,x5 } \/ { x6 }) by Th43
.= { x1,x2,x3 } \/ { x4,x5 } \/ { x6 }
by XBOOLE_1:4
.= { x1,x2,x3,x4,x5 } \/ { x6 } by Lm10;
end;
Lm12: { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4 } \/ { x5,x6,x7 }
proof
now let x;
A1: x in { x1,x2,x3,x4 } iff x=x1 or x=x2 or x=x3 or x=x4 by Lm2;
A2: x in { x5,x6,x7 } iff x=x5 or x=x6 or x=x7 by Def1;
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 Lm6;
hence x in { x1,x2,x3,x4,x5,x6,x7 } iff
x in { x1,x2,x3,x4 } \/ { x5,x6,x7 } by A1,A2,XBOOLE_0:def 2;
end;
hence thesis by TARSKI:2;
end;
theorem Th56:
{ 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 Lm12
.= { x1 } \/ { x2,x3,x4 } \/ { x5,x6,x7 } by Th44
.= { x1 } \/ ({ x2,x3,x4 } \/ { x5,x6,x7 })
by XBOOLE_1:4
.= { x1 } \/ { x2,x3,x4,x5,x6,x7 } by Lm11;
end;
theorem Th57:
{ 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 Lm12
.= { x1,x2 } \/ { x3,x4 } \/ { x5,x6,x7 } by Lm9
.= { x1,x2 } \/ ({ x3,x4 } \/ { x5,x6,x7 })
by XBOOLE_1:4
.= { x1,x2 } \/ { x3,x4,x5,x6,x7 } by Th48;
end;
theorem Th58:
{ 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 Lm12
.= { x1,x2,x3 } \/ { x4 } \/ { x5,x6,x7 } by Th46
.= { x1,x2,x3 } \/ ({ x4 } \/ { x5,x6,x7 })
by XBOOLE_1:4
.= { x1,x2,x3 } \/ { x4,x5,x6,x7 } by Th44;
end;
theorem
{ x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4 } \/ { x5,x6,x7 } by Lm12;
theorem
{ 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 Lm12
.= { x1,x2,x3,x4 } \/ ({ x5 } \/ { x6,x7 }) by Th42
.= { x1,x2,x3,x4 } \/ { x5 } \/ { x6,x7 } by XBOOLE_1:4
.= { x1,x2,x3,x4,x5 } \/ { x6,x7 } by Th50;
end;
theorem
{ 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 Lm12
.= { x1,x2,x3,x4 } \/ ({ x5,x6 } \/ { x7 }) by Th43
.= { x1,x2,x3,x4 } \/ { x5,x6 } \/ { x7 } by XBOOLE_1:4
.= { x1,x2,x3,x4,x5,x6 } \/ { x7 } by Th54;
end;
Lm13: { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8 }
proof
now let x;
A1: x in { x1,x2,x3,x4 } iff x=x1 or x=x2 or x=x3 or x=x4 by Lm2;
A2: x in { x5,x6,x7,x8 } iff x=x5 or x=x6 or x=x7 or x=x8 by Lm2;
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 Lm8;
hence x in { x1,x2,x3,x4,x5,x6,x7,x8 } iff
x in { x1,x2,x3,x4 } \/ { x5,x6,x7,x8 } by A1,A2,XBOOLE_0:def 2;
end;
hence thesis by TARSKI:2;
end;
theorem
{ 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 Lm13
.= { x1 } \/ { x2,x3,x4 } \/ { x5,x6,x7,x8 } by Th44
.= { x1 } \/ ({ x2,x3,x4 } \/ { x5,x6,x7,x8 }) by XBOOLE_1:4
.= { x1 } \/ { x2,x3,x4,x5,x6,x7,x8 } by Th58;
end;
theorem Th63:
{ 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 Lm13
.= { x1,x2 } \/ { x3,x4 } \/ { x5,x6,x7,x8 } by Lm9
.= { x1,x2 } \/ ({ x3,x4 } \/ { x5,x6,x7,x8 }) by XBOOLE_1:4
.= { x1,x2 } \/ { x3,x4,x5,x6,x7,x8 } by Th52;
end;
theorem
{ 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 Lm13
.= { x1,x2,x3 } \/ { x4 } \/ { x5,x6,x7,x8 } by Th46
.= { x1,x2,x3 } \/ ({ x4 } \/ { x5,x6,x7,x8 }) by XBOOLE_1:4
.= { x1,x2,x3 } \/ { x4,x5,x6,x7,x8 } by Th47;
end;
theorem
{ x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8 } by Lm13;
theorem
{ 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 Lm13
.= { x1,x2,x3,x4 } \/ ({x5 } \/ { x6,x7,x8 }) by Th44
.= { x1,x2,x3,x4 } \/ {x5 } \/ { x6,x7,x8 } by XBOOLE_1:4
.= { x1,x2,x3,x4,x5 } \/ { x6,x7,x8 } by Th50;
end;
theorem
{ 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 Lm13
.= { x1,x2,x3,x4 } \/ ({ x5,x6 } \/ { x7,x8 }) by Lm9
.= { x1,x2,x3,x4 } \/ { x5,x6 } \/ { x7,x8 } by XBOOLE_1:4
.= { x1,x2,x3,x4,x5,x6 } \/ { x7,x8 } by Th54;
end;
theorem
{ 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 Lm13
.= { x1,x2,x3,x4 } \/ ({ x5,x6,x7 } \/ { x8 }) by Th46
.= { x1,x2,x3,x4 } \/ { x5,x6,x7 } \/ { x8 } by XBOOLE_1:4
.= { x1,x2,x3,x4,x5,x6,x7 } \/ { x8 } by Lm12;
end;
theorem Th69:
{ x1,x1 } = { x1 }
proof
now let x;
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 Th70:
{ x1,x1,x2 } = { x1,x2 }
proof
thus { x1,x1,x2 } = { x1,x1 } \/ { x2 } by Th43
.= { x1 } \/ { x2 } by Th69
.= { x1,x2 } by Th41;
end;
theorem Th71:
{ x1,x1,x2,x3 } = { x1,x2,x3 }
proof
thus { x1,x1,x2,x3 } = { x1,x1 } \/ { x2,x3 } by Lm9
.= { x1 } \/ { x2,x3 } by Th69
.= { x1,x2,x3 } by Th42;
end;
theorem Th72:
{ x1,x1,x2,x3,x4 } = { x1,x2,x3,x4 }
proof
thus { x1,x1,x2,x3,x4 } = { x1,x1 } \/ { x2,x3,x4 } by Th48
.= { x1 } \/ { x2,x3,x4 } by Th69
.= { x1,x2,x3,x4 } by Th44;
end;
theorem Th73:
{ 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 Th52
.= { x1 } \/ { x2,x3,x4,x5 } by Th69
.= { x1,x2,x3,x4,x5 } by Th47;
end;
theorem Th74:
{ 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 Th57
.= { x1 } \/ { x2,x3,x4,x5,x6 } by Th69
.= { x1,x2,x3,x4,x5,x6 } by Th51;
end;
theorem Th75:
{ 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 Th63
.= { x1 } \/ { x2,x3,x4,x5,x6,x7 } by Th69
.= { x1,x2,x3,x4,x5,x6,x7 } by Th56;
end;
theorem
{ x1,x1,x1 } = { x1 }
proof thus { x1,x1,x1 } = { x1,x1 } by Th70 .= { x1 } by Th69; end;
theorem Th77:
{ x1,x1,x1,x2 } = { x1,x2 }
proof
thus { x1,x1,x1,x2 } = { x1,x1,x2 } by Th71
.= { x1,x2 } by Th70;
end;
theorem Th78:
{ x1,x1,x1,x2,x3 } = { x1,x2,x3 }
proof
thus { x1,x1,x1,x2,x3 } = { x1,x1,x2,x3 } by Th72
.= { x1,x2,x3 } by Th71;
end;
theorem Th79:
{ x1,x1,x1,x2,x3,x4 } = { x1,x2,x3,x4 }
proof
thus { x1,x1,x1,x2,x3,x4 } = { x1,x1,x2,x3,x4 } by Th73
.= { x1,x2,x3,x4 } by Th72;
end;
theorem Th80:
{ 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 Th74
.= { x1,x2,x3,x4,x5 } by Th73;
end;
theorem Th81:
{ 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 Th75
.= { x1,x2,x3,x4,x5,x6 } by Th74;
end;
theorem
{ x1,x1,x1,x1 } = { x1 }
proof
thus { x1,x1,x1,x1 } = { x1,x1 } by Th77
.= { x1 } by Th69;
end;
theorem Th83:
{ x1,x1,x1,x1,x2 } = { x1,x2 }
proof
thus { x1,x1,x1,x1,x2 } = { x1,x1,x2 } by Th78
.= { x1,x2 } by Th70;
end;
theorem Th84:
{ x1,x1,x1,x1,x2,x3 } = { x1,x2,x3 }
proof
thus { x1,x1,x1,x1,x2,x3 } = { x1,x1,x2,x3 } by Th79
.= { x1,x2,x3 } by Th71;
end;
theorem Th85:
{ 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 Th80
.= { x1,x2,x3,x4 } by Th72;
end;
theorem Th86:
{ 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 Th81
.= { x1,x2,x3,x4,x5 } by Th73;
end;
theorem
{ x1,x1,x1,x1,x1 } = { x1 }
proof
thus { x1,x1,x1,x1,x1 } = { x1,x1 } by Th83
.= { x1 } by Th69;
end;
theorem Th88:
{ x1,x1,x1,x1,x1,x2 } = { x1,x2 }
proof
thus { x1,x1,x1,x1,x1,x2 } = { x1,x1,x2 } by Th84
.= { x1,x2 } by Th70;
end;
theorem Th89:
{ x1,x1,x1,x1,x1,x2,x3 } = { x1,x2,x3 }
proof
thus { x1,x1,x1,x1,x1,x2,x3 } = { x1,x1,x2,x3 } by Th85
.= { x1,x2,x3 } by Th71;
end;
theorem Th90:
{ 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 Th86
.= { x1,x2,x3,x4 } by Th72;
end;
theorem
{ x1,x1,x1,x1,x1,x1 } = { x1 }
proof
thus { x1,x1,x1,x1,x1,x1 } = { x1,x1 } by Th88
.= { x1 } by Th69;
end;
theorem Th92:
{ x1,x1,x1,x1,x1,x1,x2 } = { x1,x2 }
proof
thus { x1,x1,x1,x1,x1,x1,x2 } = { x1,x1,x2 } by Th89
.= { x1,x2 } by Th70;
end;
theorem Th93:
{ 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 Th90
.= { x1,x2,x3 } by Th71;
end;
theorem
{ x1,x1,x1,x1,x1,x1,x1 } = { x1 }
proof
thus { x1,x1,x1,x1,x1,x1,x1 } = { x1,x1 } by Th92
.= { x1 } by Th69;
end;
theorem Th95:
{ x1,x1,x1,x1,x1,x1,x1,x2 } = { x1,x2 }
proof
thus { x1,x1,x1,x1,x1,x1,x1,x2 } = { x1,x1,x2 } by Th93
.= { x1,x2 } by Th70;
end;
theorem
{ x1,x1,x1,x1,x1,x1,x1,x1 } = { x1 }
proof
thus { x1,x1,x1,x1,x1,x1,x1,x1 } = { x1,x1 } by Th95
.= { x1 } by Th69;
end;
canceled;
theorem Th98:
{ x1,x2,x3 } = { x1,x3,x2 }
proof
thus { x1,x2,x3 } = { x1 } \/ { x2,x3 } by Th42
.= { x1,x3,x2 } by Th42;
end;
theorem Th99:
{ x1,x2,x3 } = { x2,x1,x3 }
proof
thus { x1,x2,x3 } = { x1,x2 } \/ { x3 } by Th43
.= { x2,x1,x3 } by Th43;
end;
theorem Th100:
{ x1,x2,x3 } = { x2,x3,x1 }
proof
thus { x1,x2,x3 } = { x2,x3 } \/ { x1 } by Th42
.= { x2,x3,x1 } by Th43;
end;
canceled;
theorem Th102:
{ x1,x2,x3 } = { x3,x2,x1 }
proof
thus { x1,x2,x3 } = { x3,x1,x2 } by Th100
.= { x3,x2,x1 } by Th98;
end;
theorem Th103:
{ x1,x2,x3,x4 } = { x1,x2,x4,x3 }
proof
thus { x1,x2,x3,x4 } = { x1 } \/ { x2,x3,x4 } by Th44
.= { x1 } \/ { x2,x4,x3 } by Th98
.= { x1,x2,x4,x3 } by Th44;
end;
theorem
{ x1,x2,x3,x4 } = { x1,x3,x2,x4 }
proof
thus { x1,x2,x3,x4 } = { x1 } \/ { x2,x3,x4 } by Th44
.= { x1 } \/ { x3,x2,x4 } by Th99
.= { x1,x3,x2,x4 } by Th44;
end;
theorem Th105:
{ x1,x2,x3,x4 } = { x1,x3,x4,x2 }
proof
thus { x1,x2,x3,x4 } = { x1 } \/ { x2,x3,x4 } by Th44
.= { x1 } \/ { x3,x4,x2 } by Th100
.= { x1,x3,x4,x2 } by Th44;
end;
canceled;
theorem Th107:
{ x1,x2,x3,x4 } = { x1,x4,x3,x2 }
proof
thus { x1,x2,x3,x4 } = { x1 } \/ { x2,x3,x4 } by Th44
.= { x1 } \/ { x4,x3,x2 } by Th102
.= { x1,x4,x3,x2 } by Th44;
end;
theorem Th108:
{ x1,x2,x3,x4 } = { x2,x1,x3,x4 }
proof
thus { x1,x2,x3,x4 } = { x1,x2,x3 } \/ { x4 } by Th46
.= { x2,x1,x3 } \/ { x4 } by Th99
.= { x2,x1,x3,x4 } by Th46;
end;
Lm14: { x1,x2,x3,x4 } = { x2,x3,x1,x4 }
proof
thus { x1,x2,x3,x4 } = { x1,x2,x3 } \/ { x4 } by Th46
.= { x2,x3,x1 } \/ { x4 } by Th100
.= { x2,x3,x1,x4 } by Th46;
end;
theorem
{ x1,x2,x3,x4 } = { x2,x1,x4,x3 }
proof
thus { x1,x2,x3,x4 } = { x2,x3,x1,x4 } by Lm14
.= { x2,x1,x4,x3 } by Th105;
end;
theorem
{ x1,x2,x3,x4 } = { x2,x3,x1,x4 } by Lm14;
theorem
{ x1,x2,x3,x4 } = { x2,x3,x4,x1 }
proof
thus { x1,x2,x3,x4 } = { x2,x3,x1,x4 } by Lm14
.= { x2,x3,x4,x1 } by Th103;
end;
theorem
{ x1,x2,x3,x4 } = { x2,x4,x1,x3 }
proof
thus { x1,x2,x3,x4 } = { x2,x3,x1,x4 } by Lm14
.= { x2,x4,x1,x3 } by Th107;
end;
theorem
{ x1,x2,x3,x4 } = { x2,x4,x3,x1 }
proof
thus { x1,x2,x3,x4 } = { x2,x3,x1,x4 } by Lm14
.= { x2,x4,x3,x1 } by Th105;
end;
Lm15: { x1,x2,x3,x4 } = { x3,x2,x1,x4 }
proof
thus { x1,x2,x3,x4 } = { x1,x2,x3 } \/ { x4 } by Th46
.= { x3,x2,x1 } \/ { x4 } by Th102
.= { x3,x2,x1,x4 } by Th46;
end;
canceled 2;
theorem
{ x1,x2,x3,x4 } = { x3,x2,x1,x4 } by Lm15;
theorem
{ x1,x2,x3,x4 } = { x3,x2,x4,x1 }
proof
thus { x1,x2,x3,x4 } = { x3,x2,x1,x4 } by Lm15
.= { x3,x2,x4,x1 } by Th103;
end;
theorem
{ x1,x2,x3,x4 } = { x3,x4,x1,x2 }
proof
thus { x1,x2,x3,x4 } = { x3,x2,x1,x4 } by Lm15
.= { x3,x4,x1,x2 } by Th107;
end;
theorem Th119:
{ x1,x2,x3,x4 } = { x3,x4,x2,x1 }
proof
thus { x1,x2,x3,x4 } = { x3,x2,x1,x4 } by Lm15
.= { x3,x4,x2,x1 } by Th105;
end;
canceled 3;
theorem
{ x1,x2,x3,x4 } = { x4,x2,x3,x1 }
proof
thus { x1,x2,x3,x4 } = { x3,x4,x2,x1 } by Th119
.= { x4,x2,x3,x1 } by Lm14;
end;
canceled;
theorem
{ x1,x2,x3,x4 } = { x4,x3,x2,x1 }
proof
thus { x1,x2,x3,x4 } = { x3,x4,x2,x1 } by Th119
.= { x4,x3,x2,x1 } by Th108;
end;