:: Enumerated Sets :: by Andrzej Trybulec :: :: Received January 8, 1989 :: Copyright (c) 1990-2017 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;