:: Enumerated Sets
:: by Andrzej Trybulec
::
:: Received January 8, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies TARSKI, XBOOLE_0;
notations TARSKI, XBOOLE_0;
constructors TARSKI, XBOOLE_0;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, XBOOLE_0, XBOOLE_1;
schemes XBOOLE_0;
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;
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 being set st
(for x being object holds x in X1 iff P[x]) & (for
x being 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;
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 being set st
(for x being object holds x in X1 iff P[x]) & (for
x being 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;
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 being set st
(for x being object holds x in X1 iff P[x]) & (for
x being 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;
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 being set st
(for x being object holds x in X1 iff P[x]) & (for
x being 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;
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 being set st
(for x being object holds x in X1 iff P[x]) & (for
x being 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;
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 being set st
(for x being object holds x in X1 iff P[x]) & (for
x being 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;
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 being set st
(for x being object holds x in X iff P[x]) & (for
x being 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;
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 being set st
(for x being object holds x in X iff P[x]) & (for
x being object holds x in Y iff P[x]) holds X = Y from XBOOLE_0:sch 3;
end;
end;
theorem 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 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
,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 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 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
{ x1,x2,x3,x4 } = { x1,x2 } \/ { x3,x4 } by Lm2;
theorem 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 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 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
{ x1,x2,x3,x4,x5 } = { x1,x2,x3 } \/ { x4,x5 } by Lm3;
theorem 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 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 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
{ x1,x2,x3,x4,x5,x6 } = { x1,x2,x3 } \/ { x4,x5,x6 } by Lm4;
theorem 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
{ 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 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 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 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
{ x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4 } \/ { x5,x6,x7 } by Lm5;
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 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
{ 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
{ 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 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 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
{ x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8 } by Lm6;
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 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
{ 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
{ 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 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 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 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 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 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 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 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
{ x1,x1,x1 } = { x1 }
proof
thus { x1,x1,x1 } = { x1,x1 } by Th30
.= { x1 } by Th29;
end;
theorem Th37:
{ x1,x1,x1,x2 } = { x1,x2 }
proof
thus { x1,x1,x1,x2 } = { x1,x1,x2 } by Th31
.= { x1,x2 } by Th30;
end;
theorem 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 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 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 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
{ x1,x1,x1,x1 } = { x1 }
proof
thus { x1,x1,x1,x1 } = { x1,x1 } by Th37
.= { x1 } by Th29;
end;
theorem 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 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 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 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
{ x1,x1,x1,x1,x1 } = { x1 }
proof
thus { x1,x1,x1,x1,x1 } = { x1,x1 } by Th43
.= { x1 } by Th29;
end;
theorem 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 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 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
{ x1,x1,x1,x1,x1,x1 } = { x1 }
proof
thus { x1,x1,x1,x1,x1,x1 } = { x1,x1 } by Th48
.= { x1 } by Th29;
end;
theorem 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 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
{ 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 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
{ 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 Th57:
{ x1,x2,x3 } = { x1,x3,x2 }
proof
thus { x1,x2,x3 } = { x1 } \/ { x2,x3 } by Th2
.= { x1,x3,x2 } by Th2;
end;
theorem Th58:
{ x1,x2,x3 } = { x2,x1,x3 }
proof
thus { x1,x2,x3 } = { x1,x2 } \/ { x3 } by Th3
.= { x2,x1,x3 } by Th3;
end;
theorem Th59:
{ x1,x2,x3 } = { x2,x3,x1 }
proof
thus { x1,x2,x3 } = { x2,x3 } \/ { x1 } by Th2
.= { x2,x3,x1 } by Th3;
end;
theorem Th60:
{ x1,x2,x3 } = { x3,x2,x1 }
proof
thus { x1,x2,x3 } = { x3,x1,x2 } by Th59
.= { x3,x2,x1 } by Th57;
end;
theorem 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
{ 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 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 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 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
{ 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
{ x1,x2,x3,x4 } = { x2,x3,x1,x4 } by Lm7;
theorem
{ 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 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
{ 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
{ x1,x2,x3,x4 } = { x3,x2,x1,x4 } by Lm8;
theorem
{ 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
{ 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 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
{ 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
{ 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
{ 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
{ 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
{ 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
{ x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 }
by Lm9;
theorem
{ 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
{ 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
{ 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
{ 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
{ 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 :: Addenda
theorem :: from AMI_7, 2006.03.15, A.T.
for x, y, z being 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,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;
:: from SCMBSORT, 2007.07.26, A.T.
theorem
for x1,x2,x3 being 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;