Copyright (c) 2003 Association of Mizar Users
environ
vocabulary NECKLA_2, NECKLACE, CLASSES1, CLASSES2, ORDERS_1, RELAT_1,
REALSET1, FUNCT_1, PRE_TOPC, BOOLE, SETFAM_1, CANTOR_1, CARD_1, PROB_1,
SQUARE_1, ARYTM, FINSET_1, ORDINAL2, ORDINAL1;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, RELSET_1, FINSET_1,
CARD_1, ORDINAL1, ORDINAL2, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, STRUCT_0,
GROUP_1, REALSET1, SQUARE_1, ORDERS_1, RELAT_1, NECKLACE, PRE_TOPC,
FUNCT_1, FUNCT_2, CLASSES2, SETFAM_1, CANTOR_1, CLASSES1, PROB_1,
CARD_LAR;
constructors ENUMSET1, NECKLACE, NAT_1, CLASSES2, CANTOR_1, GROUP_1, PROB_1,
SQUARE_1, COHSP_1, CARD_LAR, REALSET1, MEMBERED;
clusters RELSET_1, ORDERS_1, STRUCT_0, FINSET_1, NAT_1, NECKLACE, ORDINAL1,
CLASSES2, YELLOW13, XREAL_0, COHSP_1, XBOOLE_0, CARD_1, MEMBERED,
NUMBERS, ORDINAL2;
requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM;
definitions TARSKI;
theorems FUNCT_1, FUNCT_2, ENUMSET1, RELSET_1, ZFMISC_1, XBOOLE_1, TARSKI,
ORDINAL1, PARTFUN1, NECKLACE, CLASSES2, CLASSES1, XBOOLE_0, SETFAM_1,
CANTOR_1, CARD_5, NAT_1, REALSET1, SQUARE_1, FINSEQ_2, AXIOMS, STRUCT_0,
RELAT_1, REAL_1, CQC_THE1, CARD_2, ORDINAL2, CARD_4, CARD_1, GROUP_1,
FINSET_1, SUBSET_1, CARD_3, XCMPLX_1;
schemes TARSKI, XBOOLE_0, RECDEF_1, NAT_1;
begin
reserve U for Universe;
theorem Th1:
for X,Y being set st X in U & Y in U
for R being Relation of X,Y holds R in U
proof
let X,Y being set;
assume X in U & Y in U;
then A1: [:X,Y:] in U by CLASSES2:67;
thus thesis by A1,CLASSES1:def 1;
end;
theorem Th2:
the InternalRel of Necklace 4 =
{[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]}
proof
set A = {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]},
B = the InternalRel of Necklace 4;
A1: B =
{[i,i+1] where i is Nat:i+1 < 4} \/ {[i+1,i] where i is Nat:i+1 < 4}
by NECKLACE:19;
A2: [0,0+1] in {[i,i+1] where i is Nat:i+1 < 4};
A3: [0+1,0] in {[i+1,i] where i is Nat:i+1 < 4};
A4: [0+1,1+1] in {[i,i+1] where i is Nat:i+1 < 4};
A5: [1+1,0+1] in {[i+1,i] where i is Nat:i+1 < 4};
A6: [1+1,2+1] in {[i,i+1] where i is Nat:i+1 < 4};
A7: [2+1,1+1] in {[i+1,i] where i is Nat:i+1 < 4};
A8: A c= B
proof
let x be set;
assume A9: x in A;
per cases by A9,ENUMSET1:28;
suppose x = [0,1];
hence thesis by A1,A2,XBOOLE_0:def 2;
suppose x=[1,0];
hence thesis by A1,A3,XBOOLE_0:def 2;
suppose x=[1,2];
hence thesis by A1,A4,XBOOLE_0:def 2;
suppose x=[2,1];
hence thesis by A1,A5,XBOOLE_0:def 2;
suppose x=[2,3];
hence thesis by A1,A6,XBOOLE_0:def 2;
suppose x=[3,2];
hence thesis by A1,A7,XBOOLE_0:def 2;
end;
B c= A
proof
let x be set;
assume A10: x in B;
then consider y,z being set such that
A11: x = [y,z] by RELAT_1:def 1;
per cases by A1,A10,XBOOLE_0:def 2;
suppose x in {[i,i+1] where i is Nat: i+1<4};
then consider i be Nat such that
A12: [y,z] = [i,i+1] & i+1 < 4 by A11;
A13: y = i & z = i+1 by A12,ZFMISC_1:33;
i + 1 < 1 + 3 by A12;
then i < 2+1 by REAL_1:55;
then i <= 2 by NAT_1:38;
then y = 0 or y = 1 or y = 2 by A13,CQC_THE1:3;
hence thesis by A11,A13,ENUMSET1:29;
suppose x in {[i+1,i] where i is Nat: i+1<4};
then consider i be Nat such that
A14: [y,z] = [i+1,i] & i+1 < 4 by A11;
A15: y = i+1 & z = i by A14,ZFMISC_1:33;
i + 1 < 1 + 3 by A14;
then i < 2+1 by REAL_1:55;
then i <= 2 by NAT_1:38;
then z = 0 or z = 1 or z = 2 by A15,CQC_THE1:3;
hence thesis by A11,A15,ENUMSET1:29;
end;
hence thesis by A8,XBOOLE_0:def 10;
end;
definition let n be natural number;
cluster -> finite Element of Rank n;
coherence
proof
let x be Element of Rank n;
defpred P[natural number] means
for x being set st x is Element of Rank $1
holds x is finite;
A1: P[0] by CLASSES1:33,SUBSET_1:def 2;
A2: for k being natural number st P[k] holds P[k + 1]
proof
let k being natural number such that P[k];
let x be set such that A3: x is Element of Rank (k+1);
consider m being Nat such that A4: m = k by CARD_1:54;
x is Element of Rank (succ m) by A3,A4,CARD_1:52;
then A5: x is Element of bool Rank m by CLASSES1:34;
Rank m is finite by CARD_3:57;
hence thesis by A5,FINSET_1:13;
end;
for k being natural number holds P[k] from Nat_Ind(A1,A2);
hence thesis;
end;
end;
theorem Th3:
for x be set st x in FinSETS holds x is finite
proof
let x be set such that A1: x in FinSETS;
omega is_limit_ordinal by ORDINAL2:def 5;
then consider n being Ordinal such that A2: n in omega &
x in Rank n by A1,CLASSES1:35,CLASSES2:71;
reconsider n as natural number by A2,ORDINAL2:def 21;
x is Element of Rank n by A2;
hence thesis;
end;
definition
cluster -> finite Element of FinSETS;
coherence by Th3;
end;
definition
cluster finite ordinal -> natural number;
coherence
proof
let n be number;
assume n is finite ordinal;
then n in omega by CARD_4:7;
hence n is natural by ORDINAL2:def 21;
end;
end;
definition let G be non empty RelStr;
attr G is N-free means
:Def1: not G embeds Necklace 4;
end;
definition
cluster strict finite N-free (non empty RelStr);
existence
proof
set X = {0,1},
Y = Necklace 4;
reconsider r = id X as Relation of X by RELSET_1:29;
take R = RelStr(#X,r#);
now let f being map of Y,R;
assume A1: f is one-to-one;
A2: dom f = the carrier of Y by FUNCT_2:def 1
.= {0,1,2,3} by NECKLACE:2,21;
then A3: 1 in dom f by ENUMSET1:19;
A4: 2 in dom f by A2,ENUMSET1:19;
A5: 3 in dom f by A2,ENUMSET1:19;
then A6: f.1 <> f.3 by A1,A3,FUNCT_1:def 8;
A7: f.2 <> f.3 by A1,A4,A5,FUNCT_1:def 8;
A8: f.1 in X by A3,PARTFUN1:27;
A9: f.2 in X by A4,PARTFUN1:27;
A10: f.3 in X by A5,PARTFUN1:27;
A11: f.1 = 0 or f.1 = 1 by A8,TARSKI:def 2;
f.2 = 0 or f.2 = 1 by A9,TARSKI:def 2;
hence ex x,y being Element of Y st
not ([x,y] in the InternalRel of Y
iff [f.x,f.y] in the InternalRel of R) by A1,A3,A4,A6,A7,A10,
A11,FUNCT_1:def 8,TARSKI:def 2;
end;
then A12: not R embeds Y by NECKLACE:def 2;
R is finite by GROUP_1:def 13;
hence thesis by A12,Def1;
end;
end;
definition let R,S be RelStr;
func union_of(R,S) -> strict RelStr means
:Def2: the carrier of it = (the carrier of R) \/ (the carrier of S) &
the InternalRel of it = (the InternalRel of R) \/ (the InternalRel of S);
existence
proof
set X = (the carrier of R) \/ (the carrier of S);
the carrier of R c= X & the carrier of S c= X by XBOOLE_1:7;
then reconsider IR = the InternalRel of R, IS = the InternalRel of S
as Relation of X by RELSET_1:17;
set D = IR \/ IS;
reconsider D as Relation of X;
take RelStr (# X, D #);
thus thesis;
end;
uniqueness;
end;
definition let R, S be RelStr;
func sum_of(R,S) -> strict RelStr means
:Def3: the carrier of it = (the carrier of R) \/ (the carrier of S) &
the InternalRel of it = (the InternalRel of R) \/ (the InternalRel of S)
\/ [:the carrier of R, the carrier of S:]
\/ [:the carrier of S, the carrier of R:];
existence
proof
set X = (the carrier of R) \/ (the carrier of S);
the carrier of R c= X & the carrier of S c= X by XBOOLE_1:7;
then reconsider IR = the InternalRel of R, IS = the InternalRel of S
as Relation of X by RELSET_1:17;
A1: the carrier of R c= X by XBOOLE_1:7;
A2: the carrier of S c= X by XBOOLE_1:7;
then [:the carrier of R, the carrier of S:] c= [:X,X:] by A1,ZFMISC_1:119
;
then reconsider IQ = [:the carrier of R, the carrier of S:]
as Relation of X by RELSET_1:def 1;
[:the carrier of S, the carrier of R:] c= [:X,X:] by A1,A2,ZFMISC_1:119;
then reconsider IP = [:the carrier of S, the carrier of R:]
as Relation of X by RELSET_1:def 1;
set D = IR \/ IS \/ IQ \/ IP;
take RelStr (# X, D #);
thus thesis;
end;
uniqueness;
end;
definition
func fin_RelStr means
:Def4: for X being set holds
X in it iff
ex R being strict RelStr st X = R & the carrier of R in FinSETS;
existence
proof
defpred P[set,set] means ex R being strict RelStr
st $1 = [the carrier of R,the InternalRel of R] &
$2 = R;
A1: for x,y,z being set st P[x,y] & P[x,z] holds y = z
proof
let x,y,z being set;
given R1 being strict RelStr such that
A2: x = [the carrier of R1,the InternalRel of R1] and
A3: y = R1;
given R2 being strict RelStr such that
A4: x = [the carrier of R2,the InternalRel of R2] and
A5: z = R2;
the carrier of R1 = the carrier of R2 &
the InternalRel of R1 = the InternalRel of R2 by A2,A4,ZFMISC_1:33;
hence thesis by A3,A5;
end;
consider X being set such that A6: for x being set holds x in X iff
ex y being set st y in FinSETS & P[y,x] from Fraenkel(A1);
take X;
for x being set holds x in X iff
ex R being strict RelStr st x = R &
the carrier of R in FinSETS
proof
let x being set;
thus x in X implies
ex R being strict RelStr st x = R &
the carrier of R in FinSETS
proof
assume x in X;
then consider y being set such that
A7: y in FinSETS & ex R being strict RelStr
st y = [the carrier of R,the InternalRel of R] & x = R by A6;
consider R being strict RelStr
such that A8: y = [the carrier of R,the InternalRel of R] & x = R
by A7;
A9: {{the carrier of R, the InternalRel of R}, {the carrier of R}} in
FinSETS by A7,A8,TARSKI:def 5;
A10: {the carrier of R} in
{{the carrier of R, the InternalRel of R}, {the carrier of R}}
by TARSKI:def 2;
{{the carrier of R, the InternalRel of R}, {the carrier of R}}
c= FinSETS by A9,ORDINAL1:def 2;
then A11: {the carrier of R} c= FinSETS by A10,ORDINAL1:def 2;
the carrier of R in {the carrier of R} by TARSKI:def 1;
hence thesis by A8,A11;
end;
given R being strict RelStr such that A12: x = R
& the carrier of R in FinSETS;
consider R being strict RelStr such that
A13: x = R & the carrier of R in FinSETS by A12;
the InternalRel of R in FinSETS by A13,Th1;
then [the carrier of R,the InternalRel of R] in FinSETS by A13,CLASSES2:
64;
hence x in X by A6,A13;
end;
hence thesis;
end;
uniqueness proof
defpred P[set] means
ex R being strict RelStr st $1 = R & the carrier of R in FinSETS;
thus 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;
end;
end;
definition
cluster fin_RelStr -> non empty;
correctness
proof
reconsider R = {}[:{},{}:] as Relation of {} by RELSET_1:25;
RelStr(#{},R#) in fin_RelStr
proof
set X = RelStr(#{},R#);
the carrier of X in FinSETS by CLASSES1:5,CLASSES2:def 2;
hence thesis by Def4;
end;
hence thesis;
end;
end;
definition
func fin_RelStr_sp -> Subset of fin_RelStr means
:Def5: (for R be strict RelStr st the carrier of R is non empty trivial
& the carrier of R in FinSETS holds R in it) &
(for H1,H2 be strict RelStr st
(the carrier of H1) misses (the carrier of H2) & H1 in it & H2 in it
holds union_of(H1,H2) in it & sum_of(H1,H2) in it)
&
for M be Subset of fin_RelStr st
( (for R be strict RelStr st the carrier of R is non empty trivial &
the carrier of R in FinSETS holds R in M) &
for H1,H2 be strict RelStr st
(the carrier of H1) misses (the carrier of H2) & H1 in M & H2 in M
holds union_of(H1,H2) in M & sum_of(H1,H2) in M )
holds it c= M;
existence
proof
defpred P[set] means
(for R being strict RelStr
st the carrier of R is non empty trivial
& the carrier of R in FinSETS holds
R in $1 ) & (for H1,H2 be strict RelStr st
(the carrier of H1) misses (the carrier of H2) & H1 in $1 & H2 in $1
holds union_of(H1,H2) in $1 & sum_of(H1,H2) in $1);
consider X being set such that A1: for x being set
holds x in X iff x in bool fin_RelStr & P[x] from Separation;
for x being set holds x in X implies x in bool fin_RelStr by A1;
then X c= bool fin_RelStr by TARSKI:def 3;
then reconsider X as Subset-Family of fin_RelStr by SETFAM_1:def 7;
take IT = Intersect X;
A2: fin_RelStr in bool fin_RelStr by ZFMISC_1:def 1;
P[fin_RelStr]
proof
set A = fin_RelStr;
for H1,H2 be strict RelStr st
(the carrier of H1) misses (the carrier of H2) & H1 in A & H2 in A
holds union_of(H1,H2) in A & sum_of(H1,H2) in A
proof
let H1,H2 be strict RelStr such that
(the carrier of H1) misses (the carrier of H2) and
A3: H1 in A and
A4: H2 in A;
consider S1 being strict RelStr such that A5: S1 = H1 and
A6: the carrier of S1 in FinSETS by A3,Def4;
consider S2 being strict RelStr such that A7: S2 = H2 and
A8: the carrier of S2 in FinSETS by A4,Def4;
A9: (the carrier of H1) \/ (the carrier of H2)
in FinSETS by A5,A6,A7,A8,CLASSES2:66;
reconsider RS = union_of(S1,S2) as strict RelStr;
the carrier of RS in FinSETS by A5,A7,A9,Def2;
hence union_of(H1,H2) in A by A5,A7,Def4;
reconsider RS' = sum_of(H1,H2) as strict RelStr;
the carrier of RS' in FinSETS by A9,Def3;
hence thesis by Def4;
end;
hence thesis by Def4;
end;
then A10: X <> {} by A1,A2;
then A11: IT = meet X by CANTOR_1:def 3;
P[IT] & for X be Subset of fin_RelStr st P[X] holds
IT c= X
proof
thus P[IT]
proof
A12: for R being strict RelStr st the carrier of R is non empty trivial
& the carrier of R in FinSETS holds R in IT
proof
let R being strict RelStr such that
A13: the carrier of R is non empty trivial and
A14: the carrier of R in FinSETS;
for Y being set holds Y in X implies R in Y by A1,A13,A14
;
hence thesis by A10,A11,SETFAM_1:def 1;
end;
for H1,H2 be strict RelStr st
(the carrier of H1) misses (the carrier of H2) & H1 in IT & H2 in IT
holds union_of(H1,H2) in IT & sum_of(H1,H2) in IT
proof
let H1,H2 be strict RelStr such that
A15: (the carrier of H1) misses (the carrier of H2) and
A16: H1 in IT and
A17: H2 in IT;
A18: for Y being set holds Y in X implies union_of(H1,H2) in Y
proof
let Y being set; assume A19: Y in X;
then A20: H1 in Y by A11,A16,SETFAM_1:def 1;
H2 in Y by A11,A17,A19,SETFAM_1:def 1;
hence thesis by A1,A15,A19,A20;
end;
sum_of(H1,H2) in IT
proof
for Y being set holds Y in X implies sum_of(H1,H2) in Y
proof
let Y being set; assume A21: Y in X;
then A22: H1 in Y by A11,A16,SETFAM_1:def 1;
H2 in Y by A11,A17,A21,SETFAM_1:def 1;
hence thesis by A1,A15,A21,A22;
end;
hence thesis by A10,A11,SETFAM_1:def 1;
end;
hence thesis by A10,A11,A18,SETFAM_1:def 1;
end;
hence thesis by A12;
end;
let Y be Subset of fin_RelStr such that A23: P[Y];
IT c= Y
proof
let x be set such that A24: x in IT;
Y in X by A1,A23;
hence thesis by A11,A24,SETFAM_1:def 1;
end;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let X1,X2 be Subset of fin_RelStr;
assume that
A25: (for R be strict RelStr st the carrier of R is non empty trivial &
the carrier of R in FinSETS
holds R in X1) and
A26: for H1,H2 be strict RelStr st
(the carrier of H1) misses (the carrier of H2) & H1 in X1 & H2 in X1
holds union_of(H1,H2) in X1 & sum_of(H1,H2) in X1
and
A27: for M be Subset of fin_RelStr st
( (for R be strict RelStr st the carrier of R is non empty trivial
& the carrier of R in FinSETS
holds R in M) &
for H1,H2 be strict RelStr st
(the carrier of H1) misses (the carrier of H2) & H1 in M & H2 in M
holds union_of(H1,H2) in M & sum_of(H1,H2) in M )
holds X1 c= M
and
A28: (for R be strict RelStr st the carrier of R is non empty trivial &
the carrier of R in FinSETS
holds R in X2) and
A29: for H1,H2 be strict RelStr st
(the carrier of H1) misses (the carrier of H2) & H1 in X2 & H2 in X2
holds union_of(H1,H2) in X2 & sum_of(H1,H2) in X2
and
A30: for M be Subset of fin_RelStr st
( (for R be strict RelStr st the carrier of R is non empty trivial &
the carrier of R in FinSETS
holds R in M) &
for H1,H2 be strict RelStr st
(the carrier of H1) misses (the carrier of H2) & H1 in M & H2 in M
holds union_of(H1,H2) in M & sum_of(H1,H2) in M )
holds X2 c= M;
X1 c= X2 & X2 c= X1 by A25,A26,A27,A28,A29,A30;
hence thesis by XBOOLE_0:def 10;
end;
end;
definition
cluster fin_RelStr_sp -> non empty;
correctness
proof
reconsider R = [:{0},{0}:] as Relation of {0} by RELSET_1:def 1;
RelStr(#{0},R#) in fin_RelStr_sp
proof
set X = RelStr(#{0},R#);
A1: the carrier of X is non empty trivial by REALSET1:def 12;
0 in Tarski-Class {} by CLASSES2:62;
then the carrier of X in FinSETS by CLASSES2:63,def 2;
hence thesis by A1,Def5;
end;
hence thesis;
end;
end;
theorem Th4:
for X being set st X in fin_RelStr_sp holds
X is finite strict non empty RelStr
proof
let X be set; assume A1: X in fin_RelStr_sp;
then consider R being strict RelStr such that A2: X = R &
the carrier of R in FinSETS by Def4;
reconsider R=X as strict RelStr by A2;
A3: now
assume A4: R is empty;
set M = fin_RelStr_sp \ {R},
F = fin_RelStr_sp;
reconsider M as Subset of fin_RelStr;
A5:
now let S be strict RelStr; assume
A6: the carrier of S is non empty trivial &
the carrier of S in FinSETS;
then A7: S in F by Def5;
S <> R by A4,A6,STRUCT_0:def 1;
then not S in {R} by TARSKI:def 1;
hence S in M by A7,XBOOLE_0:def 4;
end;
now let H1,H2 be strict RelStr;
assume that
A8: (the carrier of H1) misses (the carrier of H2) and
A9: H1 in M and A10: H2 in M;
H1 in F & H2 in F by A9,A10,XBOOLE_0:def 4;
then A11: union_of(H1,H2) in F & sum_of(H1,H2) in F by A8,Def5;
A12: not H1 in {R} by A9,XBOOLE_0:def 4;
the carrier of H1 <> {}
proof
per cases by A12,TARSKI:def 1;
suppose (the carrier of H1) <> (the carrier of R);
hence thesis by A4,STRUCT_0:def 1;
suppose
A13: (the InternalRel of H1) <> (the InternalRel of R);
set cR = the carrier of R,
Inter_H1 = the InternalRel of H1,
cH1 = the carrier of H1;
cR is empty by A4,STRUCT_0:def 1;
then Inter_H1 <> {} by A13,RELSET_1:26;
then consider x being set such that
A14:x in Inter_H1 by XBOOLE_0:def 1;
ex a,b being set st x=[a,b] &
a in cH1 & b in cH1 by A14,RELSET_1:6;
hence thesis;
end;
then reconsider A = (the carrier of H1) as non empty set;
A \/ (the carrier of H2) <> {};
then the carrier of union_of(H1,H2) <> {} by Def2;
then union_of(H1,H2) <> R by A4,STRUCT_0:def 1;
then not union_of(H1,H2) in {R} by TARSKI:def 1;
hence union_of(H1,H2) in M by A11,XBOOLE_0:def 4;
the carrier of sum_of(H1,H2) =
A \/ (the carrier of H2) by Def3;
then sum_of(H1,H2) <> R by A4,STRUCT_0:def 1;
then not sum_of(H1,H2) in {R} by TARSKI:def 1;
hence sum_of(H1,H2) in M by A11,XBOOLE_0:def 4;
end;
then A15: F c= M by A5,Def5;
R in {R} by TARSKI:def 1;
hence contradiction by A1,A15,XBOOLE_0:def 4;
end;
the carrier of R is finite by A2,Th3;
hence thesis by A3,GROUP_1:def 13;
end;
theorem
for R being RelStr st R in fin_RelStr_sp holds
(the carrier of R) in FinSETS
proof
let R be RelStr such that A1: R in fin_RelStr_sp;
consider S being strict RelStr such that A2: R = S &
the carrier of S in FinSETS by A1,Def4;
thus thesis by A2;
end;
theorem Th6:
for X being set st X in fin_RelStr_sp holds
X is strict non empty trivial RelStr or
ex H1,H2 being strict RelStr st
(the carrier of H1) misses (the carrier of H2) &
H1 in fin_RelStr_sp & H2 in fin_RelStr_sp &
(X = union_of(H1,H2) or X = sum_of(H1,H2) )
proof
set Y = fin_RelStr_sp;
let X be set such that A1: X in fin_RelStr_sp;
assume A2: not X is strict non empty trivial RelStr;
deffunc F(set,set) = $2 \/ {x where x is Element of fin_RelStr_sp:
ex R1,R2 being strict RelStr st
(the carrier of R1) misses (the carrier of R2) &
R1 in $2 & R2 in $2 &
(x = union_of(R1,R2) or x = sum_of(R1,R2) )};
consider f being Function such that A3:dom f = NAT and
A4: f.0 = {x where x is Element of fin_RelStr_sp: x is trivial RelStr} and
A5: for n being Element of NAT holds f.(n+1) = F(n,f.n) from LambdaRecEx;
A6: for i being Nat holds f.i c= f.(i+1)
proof
let i being Nat;
let x be set such that A7: x in f.i;
per cases by NAT_1:22;
suppose i = 0;
f.(i+1) = f.i \/ {b where b is Element of fin_RelStr_sp:
ex R1,R2 being strict RelStr st
(the carrier of R1) misses (the carrier of R2) &
R1 in f.i & R2 in f.i &
(b = union_of(R1,R2) or b = sum_of(R1,R2))} by A5;
hence thesis by A7,XBOOLE_0:def 2;
suppose ex n being Element of NAT st i = n+1;
f.(i+1) = f.i \/ {a where a is Element of fin_RelStr_sp:
ex R1,R2 being strict RelStr st
(the carrier of R1) misses (the carrier of R2) &
R1 in f.i & R2 in f.i &
(a = union_of(R1,R2) or a = sum_of(R1,R2))} by A5;
then f.i c= f.(i+1) by XBOOLE_1:7;
hence thesis by A7;
end;
A8: for i,j being Nat st i <= j holds f.i c= f.j
proof
let i,j being Nat; assume i <= j;
then consider k being Nat such that A9: j=i+k by NAT_1:28;
defpred P[Nat] means
f.i c= f.(i+$1);
A10: P[0];
A11: for k being Nat st P[k] holds P[k+1]
proof
let k being Nat such that A12: P[k];
A13: (i+k) +1 = i+(k+1) by XCMPLX_1:1;
f.(i+k) c= f.(i+k+1) by A6;
hence thesis by A12,A13,XBOOLE_1:1;
end;
for k being Nat holds P[k] from Ind(A10,A11);
hence thesis by A9;
end;
A14: Union f c= fin_RelStr_sp
proof
let y being set;
assume y in Union f;
then consider x being set such that
A15: x in dom f and A16: y in f.x by CARD_5:10;
defpred P[Nat] means f.$1 c= fin_RelStr_sp;
A17: P[0]
proof
let y be set;
assume y in f.0;
then ex a being Element of fin_RelStr_sp st y = a &
a is trivial RelStr by A4;
hence thesis;
end;
A18: for k being Nat st P[k] holds P[k+1]
proof
let k being Nat such that A19: P[k];
A20: f.(k+1) = f.k \/ {a where a is Element of fin_RelStr_sp:
ex R1,R2 being strict RelStr st
(the carrier of R1) misses (the carrier of R2) &
R1 in f.k & R2 in f.k &
(a = union_of(R1,R2) or a = sum_of(R1,R2))} by A5;
{a where a is Element of fin_RelStr_sp:
ex R1,R2 being strict RelStr st
(the carrier of R1) misses (the carrier of R2) &
R1 in f.k & R2 in f.k &
(a = union_of(R1,R2) or a = sum_of(R1,R2))} c= fin_RelStr_sp
proof
set S = {a where a is Element of fin_RelStr_sp:
ex R1,R2 being strict RelStr st
(the carrier of R1) misses (the carrier of R2) &
R1 in f.k & R2 in f.k &
(a = union_of(R1,R2) or a = sum_of(R1,R2))};
let x be set; assume x in S;
then consider a being Element of fin_RelStr_sp such that
A21: x = a & ex R1,R2 being strict RelStr st
(the carrier of R1) misses (the carrier of R2) &
R1 in f.k & R2 in f.k &
(a = union_of(R1,R2) or a = sum_of(R1,R2));
thus thesis by A21;
end;
hence thesis by A19,A20,XBOOLE_1:8;
end;
for k being Nat holds P[k] from Ind(A17,A18);
then f.x c= fin_RelStr_sp by A3,A15;
hence thesis by A16;
end;
then reconsider M = Union f as Subset of fin_RelStr by XBOOLE_1:1;
A22: for R be strict RelStr st the carrier of R is non empty trivial &
the carrier of R in FinSETS holds R in M
proof
let R be strict RelStr such that
A23: the carrier of R is non empty trivial and
A24: the carrier of R in FinSETS;
A25: R is Element of fin_RelStr_sp by A23,A24,Def5;
R is trivial RelStr by A23,REALSET1:def 13;
then A26: R in f.0 by A4,A25;
f.0 c= M
proof
let x be set; assume x in f.0;
hence thesis by A3,CARD_5:10;
end;
hence thesis by A26;
end;
for H1,H2 be strict RelStr st
(the carrier of H1) misses (the carrier of H2) & H1 in M & H2 in M
holds union_of(H1,H2) in M & sum_of(H1,H2) in M
proof
let H1,H2 be strict RelStr such that
A27: (the carrier of H1) misses (the carrier of H2) and
A28: H1 in M and A29: H2 in M;
consider x1 being set such that
A30: x1 in dom f and A31: H1 in f.x1 by A28,CARD_5:10;
consider x2 being set such that
A32: x2 in dom f and A33: H2 in f.x2 by A29,CARD_5:10;
A34: x1 is Nat by A3,A30;
x2 is Nat by A3,A32;
then reconsider x1,x2 as real number by A34;
A35: max(x1,x2) is Nat by A3,A30,A32,FINSEQ_2:1;
then A36: (max(x1,x2) + 1) in dom f by A3,AXIOMS:28;
x1 <= max(x1,x2) by SQUARE_1:46;
then A37: f.x1 c= f.max(x1,x2) by A3,A8,A30,A35;
x2 <= max(x1,x2) by SQUARE_1:46;
then A38: f.x2 c= f.max(x1,x2) by A3,A8,A32,A35;
set W = {a where a is Element of fin_RelStr_sp:
ex R1,R2 being strict RelStr st
(the carrier of R1) misses (the carrier of R2) &
R1 in f.max(x1,x2) & R2 in f.max(x1,x2) &
(a = union_of(R1,R2) or a = sum_of(R1,R2))};
A39: f.(max(x1,x2)+1) = f.max(x1,x2) \/ W by A5,A35;
union_of(H1,H2) in fin_RelStr_sp by A14,A27,A28,A29,Def5;
then union_of(H1,H2) in W by A27,A31,A33,A37,A38;
then A40: union_of(H1,H2) in f.(max(x1,x2) + 1) by A39,XBOOLE_0:def 2
;
sum_of(H1,H2) in fin_RelStr_sp by A14,A27,A28,A29,Def5;
then sum_of(H1,H2) in W by A27,A31,A33,A37,A38;
then sum_of(H1,H2) in f.(max(x1,x2)+1) by A39,XBOOLE_0:def 2;
hence thesis by A36,A40,CARD_5:10;
end;
then A41: fin_RelStr_sp c= M by A22,Def5;
then A42: Union f = fin_RelStr_sp by A14,XBOOLE_0:def 10;
ex H1,H2 being strict RelStr st
(the carrier of H1) misses (the carrier of H2) &
H1 in Y & H2 in Y & ( X = union_of(H1,H2) or X = sum_of(H1,H2) )
proof
consider y being set such that
A43: y in dom f and A44: X in f.y by A1,A41,CARD_5:10
;
defpred P[Nat] means X in f.$1 implies
ex H1,H2 being strict RelStr st
(the carrier of H1) misses (the carrier of H2) &
H1 in Y & H2 in Y & ( X = union_of(H1,H2) or X = sum_of(H1,H2) );
A45: P[0]
proof
assume X in f.0;
then consider a being Element of fin_RelStr_sp such that A46: X = a
and
A47: a is trivial RelStr by A4;
ex R being strict RelStr st a = R & the carrier of R in FinSETS
by Def4;
then reconsider a as RelStr;
thus thesis by A2,A46,A47,Th4;
end;
A48: for k being Nat st P[k] holds P[k+1]
proof
let n be Nat such that A49: P[n];
set W = {a where a is Element of fin_RelStr_sp:
ex R1,R2 being strict RelStr st
(the carrier of R1) misses (the carrier of R2) &
R1 in f.n & R2 in f.n &
(a = union_of(R1,R2) or a = sum_of(R1,R2))};
A50: f.(n+1) = f.n \/ W by A5;
assume A51: X in f.(n+1);
per cases by A50,A51,XBOOLE_0:def 2;
suppose X in f.n;
hence thesis by A49;
suppose X in W;
then consider a being Element of fin_RelStr_sp such that
A52: a = X and A53:
ex R1,R2 being strict RelStr st
(the carrier of R1) misses (the carrier of R2) &
R1 in f.n & R2 in f.n &
(a = union_of(R1,R2) or a = sum_of(R1,R2));
consider R1,R2 being strict RelStr such that A54:
(the carrier of R1) misses (the carrier of R2) and
A55: R1 in f.n & R2 in f.n &
(X = union_of(R1,R2) or X = sum_of(R1,R2)) by A52,A53;
R1 in Y & R2 in Y by A3,A42,A55,CARD_5:10;
hence thesis by A54,A55;
end;
for n being Nat holds P[n] from Ind(A45,A48);
hence thesis by A3,A43,A44;
end;
hence thesis;
end;
Lm1: the carrier of Necklace 4 = {0,1,2,3}
proof
thus thesis by NECKLACE:2,21;
end;
theorem
for R being strict non empty RelStr st
R in fin_RelStr_sp holds R is N-free
proof
set N_4 = Necklace 4;
let R being strict non empty RelStr; assume
A1: R in fin_RelStr_sp;
then consider S being strict RelStr such that A2: R = S and
A3: the carrier of S in FinSETS by Def4;
assume A4: R embeds N_4;
defpred P[Nat] means ex S being strict non empty RelStr st
S in fin_RelStr_sp &
Card (the carrier of S) = $1 & S embeds N_4;
reconsider C = the carrier of R as Element of FinSETS by A2,A3;
set k = Card C;
A5: ex i being Nat st P[i]
proof
P[k] by A1,A4;
hence thesis;
end;
A6: for m being Nat st m <> 0 & P[m] ex n being Nat st n < m & P[n]
proof
let m be Nat such that m <> 0 and A7: P[m];
consider S being non empty strict RelStr such that
A8: S in fin_RelStr_sp and A9: Card (the carrier of S) = m and
A10: S embeds N_4 by A7;
per cases by A8,Th6;
suppose A11: S is strict non empty trivial RelStr;
consider f being map of N_4,S such that A12: f is one-to-one
& for x,y being Element of N_4 holds
[x,y] in the InternalRel of N_4 iff
[f.x,f.y] in the InternalRel of S by A10,NECKLACE:def 2;
A13: the carrier of N_4 = {0,1,2,3} by NECKLACE:2,21;
then A14: 0 in the carrier of N_4 by ENUMSET1:19;
A15: 1 in the carrier of N_4 by A13,ENUMSET1:19;
(0 = 0+1 or 1 = 0 +1);
then [0,1] in the InternalRel of N_4 by A14,A15,NECKLACE:26;
then A16: [f.0,f.1] in the InternalRel of S by A12,A14,A15;
then A17: f.0 in dom (the InternalRel of S) &
f.1 in rng (the InternalRel of S) by RELAT_1:20;
dom (the InternalRel of S ) c= (the carrier of S) &
rng (the InternalRel of S) c= (the carrier of S) by RELSET_1:12;
then f.0 = f.1 by A11,A17,REALSET1:def 20;
then [0,0] in (the InternalRel of N_4) by A12,A14,A16;
then [0,0] = [0,1] or [0,0]=[1,0] or [0,0]=[1,2] or [0,0]=[2,1] or
[0,0]=[2,3] or [0,0]=[3,2] by Th2,ENUMSET1:28;
hence thesis by ZFMISC_1:33;
suppose ex H1,H2 being strict RelStr st
the carrier of H1 misses the carrier of H2 &
H1 in fin_RelStr_sp & H2 in fin_RelStr_sp &
(S = union_of(H1,H2) or S = sum_of(H1,H2));
then consider H1,H2 being strict RelStr such that
A18: the carrier of H1 misses the carrier of H2 and
A19: H1 in fin_RelStr_sp & H2 in fin_RelStr_sp and
A20: (S = union_of(H1,H2) or S = sum_of(H1,H2));
A21: now assume A22: S = union_of(H1,H2);
consider f being map of N_4,S such that A23: f is one-to-one
and A24: for x,y being Element of N_4 holds
[x,y] in the InternalRel of N_4 iff
[f.x,f.y] in the InternalRel of S by A10,NECKLACE:def 2;
the carrier of N_4 = {0,1,2,3} by NECKLACE:2,21;
then A26: 0 in the carrier of N_4 &
1 in the carrier of N_4 & 2 in the carrier of N_4 &
3 in the carrier of N_4 by ENUMSET1:19;
A27: [0,1] in the InternalRel of N_4 by Th2,ENUMSET1:29;
A28: [1,0] in the InternalRel of N_4 by Th2,ENUMSET1:29;
A29: [1,2] in the InternalRel of N_4 by Th2,ENUMSET1:29;
A30: [2,1] in the InternalRel of N_4 by Th2,ENUMSET1:29;
A31: [2,3] in the InternalRel of N_4 by Th2,ENUMSET1:29;
A32: [3,2] in the InternalRel of N_4 by Th2,ENUMSET1:29;
A33: dom (the InternalRel of S) c= (the carrier of S) &
rng (the InternalRel of S) c= (the carrier of S) by RELSET_1:12;
A34: [f.0,f.1] in the InternalRel of S by A24,A26,A27;
A35: [f.1,f.0] in the InternalRel of S by A24,A26,A28;
f.0 in dom (the InternalRel of S) &
f.1 in rng (the InternalRel of S) by A34,RELAT_1:20;
then A36: f.0 in (the carrier of S) & f.1 in (the carrier of S)
by A33;
A37: [f.1,f.2] in the InternalRel of S by A24,A26,A29;
A38: [f.2,f.1] in the InternalRel of S by A24,A26,A30;
A39: [f.2,f.3] in the InternalRel of S by A24,A26,A31;
A40: [f.3,f.2] in the InternalRel of S by A24,A26,A32;
A41: f.0 in (the carrier of H1) \/ (the carrier of H2) by A22,A36,
Def2;
per cases by A41,XBOOLE_0:def 2;
suppose A42: f.0 in the carrier of H1;
A43: dom (the InternalRel of H1) c= (the carrier of H1)
& rng (the InternalRel of H1) c= (the carrier of H1)
by RELSET_1:12;
A44: dom (the InternalRel of H2) c= (the carrier of H2)
& rng (the InternalRel of H2) c= (the carrier of H2)
by RELSET_1:12;
A45: [f.0,f.1] in (the InternalRel of H1) \/
(the InternalRel of H2) by A22,A34,Def2;
A46: [f.1,f.0] in (the InternalRel of H1) \/
(the InternalRel of H2) by A22,A35,Def2;
A47: [f.0,f.1] in the InternalRel of H1
proof
now assume [f.0,f.1] in the InternalRel of H2;
then f.0 in dom (the InternalRel of H2) &
f.1 in rng (the InternalRel of H2) by RELAT_1:20;
hence contradiction by A18,A42,A44,XBOOLE_0:3;
end;
hence thesis by A45,XBOOLE_0:def 2;
end;
A48: [f.1,f.0] in the InternalRel of H1
proof
now assume [f.1,f.0] in the InternalRel of H2;
then f.1 in dom (the InternalRel of H2) &
f.0 in rng (the InternalRel of H2) by RELAT_1:20;
hence contradiction by A18,A42,A44,XBOOLE_0:3;
end;
hence thesis by A46,XBOOLE_0:def 2;
end;
A49: f.1 in rng (the InternalRel of H1) by A47,RELAT_1:20;
A50: [f.1,f.2] in (the InternalRel of H1) \/
(the InternalRel of H2) by A22,A37,Def2;
A51: [f.2,f.1] in (the InternalRel of H1) \/
(the InternalRel of H2) by A22,A38,Def2;
A52: [f.1,f.2] in the InternalRel of H1
proof
now assume [f.1,f.2] in the InternalRel of H2;
then f.1 in dom (the InternalRel of H2) &
f.2 in rng (the InternalRel of H2) by RELAT_1:20;
hence contradiction by A18,A43,A44,A49,XBOOLE_0:3;
end;
hence thesis by A50,XBOOLE_0:def 2;
end;
A53: [f.2,f.1] in the InternalRel of H1
proof
now assume [f.2,f.1] in the InternalRel of H2;
then f.2 in dom (the InternalRel of H2) &
f.1 in rng (the InternalRel of H2) by RELAT_1:20;
hence contradiction by A18,A43,A44,A49,XBOOLE_0:3;
end;
hence thesis by A51,XBOOLE_0:def 2;
end;
A54: f.2 in rng (the InternalRel of H1) by A52,RELAT_1:20;
A55: [f.2,f.3] in (the InternalRel of H1) \/
(the InternalRel of H2) by A22,A39,Def2;
A56: [f.3,f.2] in (the InternalRel of H1) \/
(the InternalRel of H2) by A22,A40,Def2;
A57: [f.2,f.3] in the InternalRel of H1
proof
now assume [f.2,f.3] in the InternalRel of H2;
then f.2 in dom (the InternalRel of H2) &
f.3 in rng (the InternalRel of H2) by RELAT_1:20;
hence contradiction by A18,A43,A44,A54,XBOOLE_0:3;
end;
hence thesis by A55,XBOOLE_0:def 2;
end;
A58: [f.3,f.2] in the InternalRel of H1
proof
now assume [f.3,f.2] in the InternalRel of H2;
then f.3 in dom (the InternalRel of H2) &
f.2 in rng (the InternalRel of H2) by RELAT_1:20;
hence contradiction by A18,A43,A44,A54,XBOOLE_0:3;
end;
hence thesis by A56,XBOOLE_0:def 2;
end;
A59: f.3 in rng (the InternalRel of H1) by A57,RELAT_1:20;
H2 is non empty by A19,Th4;
then A60: the carrier of H2 is non empty by STRUCT_0:def 1;
A61: dom f = the carrier of N_4 by FUNCT_2:def 1;
rng f c= the carrier of H1
proof
let y be set;
assume y in rng f;
then consider x being set such that A62: x in dom f &
y = f.x by FUNCT_1:def 5;
per cases by A61,A62,Lm1,ENUMSET1:18;
suppose x = 0;
hence thesis by A42,A62;
suppose x = 1;
hence thesis by A43,A49,A62;
suppose x = 2;
hence thesis by A43,A54,A62;
suppose x = 3;
hence thesis by A43,A59,A62;
end;
then f is Function of the carrier of N_4,the carrier of H1
by FUNCT_2:8;
then A63: f is map of N_4,H1;
A64: H1 embeds N_4
proof
for x,y being Element of N_4
holds [x,y] in the InternalRel of N_4
iff [f.x,f.y] in the InternalRel of H1
proof
let x,y being Element of N_4;
thus [x,y] in the InternalRel of N_4 implies
[f.x,f.y] in the InternalRel of H1
proof
assume A65:[x,y] in the InternalRel of N_4;
per cases by A65,Th2,ENUMSET1:28;
suppose [x,y] = [0,1];
then x = 0 & y = 1 by ZFMISC_1:33;::as1
hence thesis by A47;
suppose [x,y] = [1,0];
then x = 1 & y = 0 by ZFMISC_1:33;
hence thesis by A48;
suppose [x,y] = [1,2];
then x = 1 & y = 2 by ZFMISC_1:33;
hence thesis by A52;
suppose [x,y] = [2,1];
then x = 2 & y = 1 by ZFMISC_1:33;
hence thesis by A53;
suppose [x,y] = [2,3];
then x = 2 & y = 3 by ZFMISC_1:33;
hence thesis by A57;
suppose [x,y] = [3,2];
then x = 3 & y = 2 by ZFMISC_1:33;
hence thesis by A58;
end;
thus [f.x,f.y] in the InternalRel of H1 implies
[x,y] in the InternalRel of N_4
proof
assume A66: [f.x,f.y] in the InternalRel of H1;
[f.x,f.y] in the InternalRel of S implies
[x,y] in the InternalRel of N_4 by A24;
then [f.x,f.y] in (the InternalRel of H1) \/
(the InternalRel of H2) implies
[x,y] in the InternalRel of N_4 by A22,Def2;
hence thesis by A66,XBOOLE_0:def 2;
end;
end;
hence thesis by A23,A63,NECKLACE:def 2;
end;
A67: H1 is strict non empty RelStr by A19,Th4;
set cS = the carrier of S,
cH1 = the carrier of H1,
cH2 = the carrier of H2;
H1 is finite by A19,Th4;
then reconsider cH1 as finite set by GROUP_1:def 13;
H2 is finite by A19,Th4;
then reconsider cH2 as finite set by GROUP_1:def 13;
cS = cH1 \/ cH2 by A22,Def2;
then reconsider cS as finite set;
A68: cH1 <> cS
proof
assume A69: cH1 = cS;
A70: cS = cH1 \/ cH2 by A22,Def2;
consider x being set such that A71: x in cH2
by A60,XBOOLE_0:def 1;
cH1 /\ cH2 = {} by A18,XBOOLE_0:def 7;
then not x in cH1 by A71,XBOOLE_0:def 3;
hence contradiction by A69,A70,A71,XBOOLE_0:def 2;
end;
cS = cH1 \/ cH2 by A22,Def2;
then cH1 c= cS by XBOOLE_1:7;
then cH1 c< cS by A68,XBOOLE_0:def 8;
then A72: card cH1 < card cS by CARD_2:67;
thus thesis by A9,A19,A64,A67,A72;
suppose A73: f.0 in the carrier of H2;
A74: dom (the InternalRel of H2) c= (the carrier of H2)
& rng (the InternalRel of H2) c= (the carrier of H2)
by RELSET_1:12;
A75: dom (the InternalRel of H1) c= (the carrier of H1)
& rng (the InternalRel of H1) c= (the carrier of H1)
by RELSET_1:12;
A76: [f.0,f.1] in (the InternalRel of H1) \/
(the InternalRel of H2) by A22,A34,Def2;
A77: [f.1,f.0] in (the InternalRel of H1) \/
(the InternalRel of H2) by A22,A35,Def2;
A78: [f.0,f.1] in the InternalRel of H2
proof
now assume [f.0,f.1] in the InternalRel of H1;
then f.0 in dom (the InternalRel of H1) &
f.1 in rng (the InternalRel of H1) by RELAT_1:20;
hence contradiction by A18,A73,A75,XBOOLE_0:3;
end;
hence thesis by A76,XBOOLE_0:def 2;
end;
A79: [f.1,f.0] in the InternalRel of H2
proof
now assume [f.1,f.0] in the InternalRel of H1;
then f.1 in dom (the InternalRel of H1) &
f.0 in rng (the InternalRel of H1) by RELAT_1:20;
hence contradiction by A18,A73,A75,XBOOLE_0:3;
end;
hence thesis by A77,XBOOLE_0:def 2;
end;
A80: f.1 in rng (the InternalRel of H2) by A78,RELAT_1:20;
A81: [f.1,f.2] in (the InternalRel of H1) \/
(the InternalRel of H2) by A22,A37,Def2;
A82: [f.2,f.1] in (the InternalRel of H1) \/
(the InternalRel of H2) by A22,A38,Def2;
A83: [f.1,f.2] in the InternalRel of H2
proof
now assume [f.1,f.2] in the InternalRel of H1;
then f.1 in dom (the InternalRel of H1) &
f.2 in rng (the InternalRel of H1) by RELAT_1:20;
hence contradiction by A18,A74,A75,A80,XBOOLE_0:3;
end;
hence thesis by A81,XBOOLE_0:def 2;
end;
A84: [f.2,f.1] in the InternalRel of H2
proof
now assume [f.2,f.1] in the InternalRel of H1;
then f.2 in dom (the InternalRel of H1) &
f.1 in rng (the InternalRel of H1) by RELAT_1:20;
hence contradiction by A18,A74,A75,A80,XBOOLE_0:3;
end;
hence thesis by A82,XBOOLE_0:def 2;
end;
A85: f.2 in rng (the InternalRel of H2) by A83,RELAT_1:20;
A86: [f.2,f.3] in (the InternalRel of H1) \/
(the InternalRel of H2) by A22,A39,Def2;
A87: [f.3,f.2] in (the InternalRel of H1) \/
(the InternalRel of H2) by A22,A40,Def2;
A88: [f.2,f.3] in the InternalRel of H2
proof
now assume [f.2,f.3] in the InternalRel of H1;
then f.2 in dom (the InternalRel of H1) &
f.3 in rng (the InternalRel of H1) by RELAT_1:20;
hence contradiction by A18,A74,A75,A85,XBOOLE_0:3;
end;
hence thesis by A86,XBOOLE_0:def 2;
end;
A89: [f.3,f.2] in the InternalRel of H2
proof
now assume [f.3,f.2] in the InternalRel of H1;
then f.3 in dom (the InternalRel of H1) &
f.2 in rng (the InternalRel of H1) by RELAT_1:20;
hence contradiction by A18,A74,A75,A85,XBOOLE_0:3;
end;
hence thesis by A87,XBOOLE_0:def 2;
end;
A90: f.3 in rng (the InternalRel of H2) by A88,RELAT_1:20;
H1 is non empty by A19,Th4;
then A91: the carrier of H1 is non empty by STRUCT_0:def 1;
A92: dom f = the carrier of N_4 by FUNCT_2:def 1;
rng f c= the carrier of H2
proof
let y be set;
assume y in rng f;
then consider x being set such that A93: x in dom f &
y = f.x by FUNCT_1:def 5;
per cases by A92,A93,Lm1,ENUMSET1:18;
suppose x = 0;
hence thesis by A73,A93;
suppose x = 1;
hence thesis by A74,A80,A93;
suppose x = 2;
hence thesis by A74,A85,A93;
suppose x = 3;
hence thesis by A74,A90,A93;
end;
then f is Function of the carrier of N_4,the carrier of H2
by FUNCT_2:8;
then A94: f is map of N_4,H2;
A95: H2 embeds N_4
proof
for x,y being Element of N_4
holds [x,y] in the InternalRel of N_4
iff [f.x,f.y] in the InternalRel of H2
proof
let x,y being Element of N_4;
thus [x,y] in the InternalRel of N_4 implies
[f.x,f.y] in the InternalRel of H2
proof
assume A96:[x,y] in the InternalRel of N_4;
per cases by A96,Th2,ENUMSET1:28;
suppose [x,y] = [0,1];
then x = 0 & y = 1 by ZFMISC_1:33;
hence thesis by A78;
suppose [x,y] = [1,0];
then x = 1 & y = 0 by ZFMISC_1:33;
hence thesis by A79;
suppose [x,y] = [1,2];
then x = 1 & y = 2 by ZFMISC_1:33;
hence thesis by A83;
suppose [x,y] = [2,1];
then x = 2 & y = 1 by ZFMISC_1:33;
hence thesis by A84;
suppose [x,y] = [2,3];
then x = 2 & y = 3 by ZFMISC_1:33;
hence thesis by A88;
suppose [x,y] = [3,2];
then x = 3 & y = 2 by ZFMISC_1:33;
hence thesis by A89;
end;
thus [f.x,f.y] in the InternalRel of H2 implies
[x,y] in the InternalRel of N_4
proof
assume A97: [f.x,f.y] in the InternalRel of H2;
[f.x,f.y] in the InternalRel of S implies
[x,y] in the InternalRel of N_4 by A24;
then [f.x,f.y] in (the InternalRel of H1) \/
(the InternalRel of H2) implies
[x,y] in the InternalRel of N_4 by A22,Def2;
hence thesis by A97,XBOOLE_0:def 2;
end;
end;
hence thesis by A23,A94,NECKLACE:def 2;
end;
A98: H2 is strict non empty RelStr by A19,Th4;
set cS = the carrier of S,
cH1 = the carrier of H1,
cH2 = the carrier of H2;
H1 is finite by A19,Th4;
then reconsider cH1 as finite set by GROUP_1:def 13;
H2 is finite by A19,Th4;
then reconsider cH2 as finite set by GROUP_1:def 13;
cS = cH1 \/ cH2 by A22,Def2;
then reconsider cS as finite set;
A99: cH2 <> cS
proof
assume A100: cH2 = cS;
A101: cS = cH1 \/ cH2 by A22,Def2;
consider x being set such that A102: x in cH1
by A91,XBOOLE_0:def 1;
cH1 /\ cH2 = {} by A18,XBOOLE_0:def 7;
then not x in cH2 by A102,XBOOLE_0:def 3;
hence contradiction by A100,A101,A102,XBOOLE_0:def 2;
end;
cS = cH1 \/ cH2 by A22,Def2;
then cH2 c= cS by XBOOLE_1:7;
then cH2 c< cS by A99,XBOOLE_0:def 8;
then A103: card cH2 < card cS by CARD_2:67;
thus thesis by A9,A19,A95,A98,A103;
end;
now assume A104: S = sum_of(H1,H2);
consider f being map of N_4,S such that A105: f is one-to-one
and A106: for x,y being Element of N_4 holds
[x,y] in the InternalRel of N_4 iff
[f.x,f.y] in the InternalRel of S by A10,NECKLACE:def 2;
the carrier of N_4 = {0,1,2,3} by NECKLACE:2,21;
then A108: 0 in the carrier of N_4 &
1 in the carrier of N_4 & 2 in the carrier of N_4 &
3 in the carrier of N_4 by ENUMSET1:19;
set A = the InternalRel of H1,
B = the InternalRel of H2,
C = [:the carrier of H1,the carrier of H2:],
D = [:the carrier of H2, the carrier of H1:],
cH1 = the carrier of H1,
cH2 = the carrier of H2,
cS = the carrier of S;
A109: [0,1] in the InternalRel of N_4 by Th2,ENUMSET1:29;
A110: [1,0] in the InternalRel of N_4 by Th2,ENUMSET1:29;
A111: [1,2] in the InternalRel of N_4 by Th2,ENUMSET1:29;
A112: [2,1] in the InternalRel of N_4 by Th2,ENUMSET1:29;
A113: [2,3] in the InternalRel of N_4 by Th2,ENUMSET1:29;
A114: [3,2] in the InternalRel of N_4 by Th2,ENUMSET1:29;
A115: dom (the InternalRel of S) c= cS &
rng (the InternalRel of S) c= cS by RELSET_1:12;
A116: [f.0,f.1] in the InternalRel of S by A106,A108,A109;
A117: [f.1,f.0] in the InternalRel of S by A106,A108,A110;
f.0 in dom (the InternalRel of S) &
f.1 in rng (the InternalRel of S) by A116,RELAT_1:20;
then A118: f.0 in cS & f.1 in cS by A115;
then A119: f.1 in cH1 \/ cH2 by A104,Def3;
A120: [f.1,f.2] in the InternalRel of S by A106,A108,A111;
then f.1 in dom (the InternalRel of S) &
f.2 in rng (the InternalRel of S) by RELAT_1:20;
then f.1 in cS & f.2 in cS by A115;
then A121: f.2 in cH1 \/ cH2 by A104,Def3;
A122: [f.2,f.1] in the InternalRel of S by A106,A108,A112;
A123: [f.2,f.3] in the InternalRel of S by A106,A108,A113;
then f.2 in dom (the InternalRel of S) &
f.3 in rng (the InternalRel of S) by RELAT_1:20;
then f.3 in cS by A115;
then A124: f.3 in cH1 \/ cH2 by A104,Def3;
A125: [f.3,f.2] in the InternalRel of S by A106,A108,A114;
A126: f.0 in cH1 \/ cH2 by A104,A118,Def3;
A127: dom B c= cH2 & rng B c= cH2 by RELSET_1:12;
A128: dom A c= cH1 & rng A c= cH1 by RELSET_1:12;
A129: not [0,2] in the InternalRel of N_4
proof
assume A130: [0,2] in the InternalRel of N_4;
per cases by A130,Th2,ENUMSET1:28;
suppose [0,2] = [0,1];
hence contradiction by ZFMISC_1:33;
suppose [0,2] = [1,2];
hence contradiction by ZFMISC_1:33;
suppose [0,2] = [2,3];
hence contradiction by ZFMISC_1:33;
suppose [0,2] = [3,2];
hence contradiction by ZFMISC_1:33;
suppose [0,2] = [2,1];
hence contradiction by ZFMISC_1:33;
suppose [0,2] = [1,0];
hence contradiction by ZFMISC_1:33;
end;
A131: not [0,3] in the InternalRel of N_4
proof
assume A132: [0,3] in the InternalRel of N_4;
per cases by A132,Th2,ENUMSET1:28;
suppose [0,3] = [0,1];
hence contradiction by ZFMISC_1:33;
suppose [0,3] = [1,2];
hence contradiction by ZFMISC_1:33;
suppose [0,3] = [2,3];
hence contradiction by ZFMISC_1:33;
suppose [0,3] = [3,2];
hence contradiction by ZFMISC_1:33;
suppose [0,3] = [2,1];
hence contradiction by ZFMISC_1:33;
suppose [0,3] = [1,0];
hence contradiction by ZFMISC_1:33;
end;
A133: not [1,3] in the InternalRel of N_4
proof
assume A134: [1,3] in the InternalRel of N_4;
per cases by A134,Th2,ENUMSET1:28;
suppose [1,3] = [0,1];
hence contradiction by ZFMISC_1:33;
suppose [1,3] = [1,2];
hence contradiction by ZFMISC_1:33;
suppose [1,3] = [2,3];
hence contradiction by ZFMISC_1:33;
suppose [1,3] = [3,2];
hence contradiction by ZFMISC_1:33;
suppose [1,3] = [2,1];
hence contradiction by ZFMISC_1:33;
suppose [1,3] = [1,0];
hence contradiction by ZFMISC_1:33;
end;
A135: A c= (the InternalRel of S) & B c= (the InternalRel of S) &
C c= (the InternalRel of S) & D c= (the InternalRel of S)
proof
A136: A c= (the InternalRel of S)
proof
let x be set; assume x in A;
then A137: x in A \/ B by XBOOLE_0:def 2;
(A \/ B) c= (A \/ B) \/ C by XBOOLE_1:7;
then A138: x in (A \/ B) \/ C by A137;
((A \/ B) \/ C) c= ((A \/ B) \/ C) \/ D by XBOOLE_1:7;
then ((A \/ B) \/ C) c= the InternalRel of S by A104,Def3
;
hence thesis by A138;
end;
A139: B c= (the InternalRel of S)
proof
let x be set; assume x in B;
then A140: x in A \/ B by XBOOLE_0:def 2;
(A \/ B) c= (A \/ B) \/ C by XBOOLE_1:7;
then A141: x in (A \/ B) \/ C by A140;
((A \/ B) \/ C) c= ((A \/ B) \/ C) \/ D by XBOOLE_1:7;
then ((A \/ B) \/ C) c= the InternalRel of S by A104,Def3
;
hence thesis by A141;
end;
A142: C c= (the InternalRel of S)
proof
let x be set; assume x in C;
then A143: x in (A \/ B) \/ C by XBOOLE_0:def 2;
((A \/ B) \/ C) c= ((A \/ B) \/ C) \/ D by XBOOLE_1:7;
then ((A \/ B) \/ C) c= the InternalRel of S by A104,Def3
;
hence thesis by A143;
end;
D c= (the InternalRel of S)
proof
let x be set; assume x in D;
then A144: x in (B \/ C) \/ D by XBOOLE_0:def 2;
((B \/ C) \/ D) c= A \/ ((B \/ C) \/ D) by XBOOLE_1:7;
then ((B \/ C) \/ D) c= A \/ (B \/ (C \/ D)) by XBOOLE_1:4;
then ((B \/ C) \/ D) c= (A \/ B) \/ (C \/ D) by XBOOLE_1:4;
then ((B \/ C) \/ D) c= ((A \/ B) \/ C) \/ D by XBOOLE_1:4;
then ((B \/ C) \/ D) c= the InternalRel of S by A104,Def3
;
hence thesis by A144;
end;
hence thesis by A136,A139,A142;
end;
per cases by A126,XBOOLE_0:def 2;
suppose A145: f.0 in cH1;
A146: f.2 in cH1
proof
now assume f.2 in cH2;
then [f.0,f.2] in C by A145,ZFMISC_1:106;
hence contradiction by A106,A108,A129,A135;
end;
hence thesis by A121,XBOOLE_0:def 2;
end;
A147: f.3 in cH1
proof
now assume f.3 in cH2;
then [f.0,f.3] in C by A145,ZFMISC_1:106;
hence contradiction by A106,A108,A131,A135;
end;
hence thesis by A124,XBOOLE_0:def 2;
end;
A148: f.1 in cH1
proof
now assume f.1 in cH2;
then [f.1,f.3] in D by A147,ZFMISC_1:106;
hence contradiction by A106,A108,A133,A135;
end;
hence thesis by A119,XBOOLE_0:def 2;
end;
set x1=[f.0,f.1], x2=[f.1,f.2], x3=[f.2,f.3],
x4=[f.1,f.0], x5=[f.2,f.1], x6=[f.3,f.2];
x1 in (A \/ B \/ C \/ D) by A104,A116,Def3;
then x1 in ((A \/ B) \/ C ) or x1 in D by XBOOLE_0:def 2;
then A149: x1 in (A \/ B) or x1 in C or x1 in D by XBOOLE_0:def 2;
A150: [f.0,f.1] in A
proof
A151: now assume x1 in B;
then f.0 in dom B & f.1 in rng B by RELAT_1:20;
hence contradiction by A18,A127,A145,XBOOLE_0:3;
end;
A152: now assume x1 in C;
then f.0 in cH1 & f.1 in cH2 by ZFMISC_1:106;
hence contradiction by A18,A148,XBOOLE_0:3;
end;
now assume x1 in D;
then f.0 in cH2 & f.1 in cH1 by ZFMISC_1:106;
hence contradiction by A18,A145,XBOOLE_0:3;
end;
hence thesis by A149,A151,A152,XBOOLE_0:def 2;
end;
x4 in (A \/ B \/ C \/ D) by A104,A117,Def3;
then x4 in ((A\/ B) \/ C) or x4 in D by XBOOLE_0:def 2;
then A153: x4 in (A \/ B) or x4 in C or x4 in D by XBOOLE_0:def 2;
A154: [f.1,f.0] in A
proof
A155: now assume x4 in B;
then f.1 in dom B & f.0 in rng B by RELAT_1:20;
hence contradiction by A18,A127,A145,XBOOLE_0:3;
end;
A156: now assume x4 in C;
then f.1 in cH1 & f.0 in cH2 by ZFMISC_1:106;
hence contradiction by A18,A145,XBOOLE_0:3;
end;
now assume x4 in D;
then f.1 in cH2 & f.0 in cH1 by ZFMISC_1:106;
hence contradiction by A18,A148,XBOOLE_0:3;
end;
hence thesis by A153,A155,A156,XBOOLE_0:def 2;
end;
x2 in (A \/ B \/ C \/ D) by A104,A120,Def3;
then x2 in ((A\/ B) \/ C) or x2 in D by XBOOLE_0:def 2;
then A157: x2 in (A \/ B) or x2 in C or x2 in D by XBOOLE_0:def 2;
A158: [f.1,f.2] in A
proof
A159: now assume x2 in B;
then f.1 in dom B & f.2 in rng B by RELAT_1:20;
hence contradiction by A18,A127,A148,XBOOLE_0:3;
end;
A160: now assume x2 in C;
then f.1 in cH1 & f.2 in cH2 by ZFMISC_1:106;
hence contradiction by A18,A146,XBOOLE_0:3;
end;
now assume x2 in D;
then f.1 in cH2 & f.2 in cH1 by ZFMISC_1:106;
hence contradiction by A18,A148,XBOOLE_0:3;
end;
hence thesis by A157,A159,A160,XBOOLE_0:def 2;
end;
x5 in (A \/ B \/ C \/ D) by A104,A122,Def3;
then x5 in ((A\/ B) \/ C) or x5 in D by XBOOLE_0:def 2;
then A161: x5 in (A \/ B) or x5 in C or x5 in D by XBOOLE_0:def 2;
A162: [f.2,f.1] in A
proof
A163: now assume x5 in B;
then f.2 in dom B & f.1 in rng B by RELAT_1:20;
hence contradiction by A18,A127,A148,XBOOLE_0:3;
end;
A164: now assume x5 in C;
then f.2 in cH1 & f.1 in cH2 by ZFMISC_1:106;
hence contradiction by A18,A148,XBOOLE_0:3;
end;
now assume x5 in D;
then f.2 in cH2 & f.1 in cH1 by ZFMISC_1:106;
hence contradiction by A18,A146,XBOOLE_0:3;
end;
hence thesis by A161,A163,A164,XBOOLE_0:def 2;
end;
x3 in (A \/ B \/ C \/ D) by A104,A123,Def3;
then x3 in ((A\/ B) \/ C) or x3 in D by XBOOLE_0:def 2;
then A165: x3 in (A \/ B) or x3 in C or x3 in D by XBOOLE_0:def 2;
A166: [f.2,f.3] in A
proof
A167: now assume x3 in B;
then f.2 in dom B & f.3 in rng B by RELAT_1:20;
hence contradiction by A18,A127,A146,XBOOLE_0:3;
end;
A168: now assume x3 in C;
then f.2 in cH1 & f.3 in cH2 by ZFMISC_1:106;
hence contradiction by A18,A147,XBOOLE_0:3;
end;
now assume x3 in D;
then f.2 in cH2 & f.3 in cH1 by ZFMISC_1:106;
hence contradiction by A18,A146,XBOOLE_0:3;
end;
hence thesis by A165,A167,A168,XBOOLE_0:def 2;
end;
x6 in (A \/ B \/ C \/ D) by A104,A125,Def3;
then x6 in ((A\/ B) \/ C) or x6 in D by XBOOLE_0:def 2;
then A169: x6 in (A \/ B) or x6 in C or x6 in D by XBOOLE_0:def 2;
A170: [f.3,f.2] in A
proof
A171: now assume x6 in B;
then f.3 in dom B & f.2 in rng B by RELAT_1:20;
hence contradiction by A18,A127,A146,XBOOLE_0:3;
end;
A172: now assume x6 in C;
then f.3 in cH1 & f.2 in cH2 by ZFMISC_1:106;
hence contradiction by A18,A146,XBOOLE_0:3;
end;
now assume x6 in D;
then f.3 in cH2 & f.2 in cH1 by ZFMISC_1:106;
hence contradiction by A18,A147,XBOOLE_0:3;
end;
hence thesis by A169,A171,A172,XBOOLE_0:def 2;
end;
H2 is non empty by A19,Th4;
then A173: the carrier of H2 is non empty by STRUCT_0:def 1;
A174: dom f = the carrier of N_4 by FUNCT_2:def 1;
rng f c= the carrier of H1
proof
let y be set;
assume y in rng f;
then consider x being set such that A175: x in dom f &
y = f.x by FUNCT_1:def 5;
per cases by A174,A175,Lm1,ENUMSET1:18;
suppose x = 0;
hence thesis by A145,A175;
suppose x = 1;
hence thesis by A148,A175;
suppose x = 2;
hence thesis by A146,A175;
suppose x = 3;
hence thesis by A147,A175;
end;
then f is Function of the carrier of N_4,cH1 by FUNCT_2:8;
then A176: f is map of N_4,H1;
A177: H1 embeds N_4
proof
for x,y being Element of N_4
holds [x,y] in the InternalRel of N_4
iff [f.x,f.y] in the InternalRel of H1
proof
let x,y being Element of N_4;
thus [x,y] in the InternalRel of N_4 implies
[f.x,f.y] in the InternalRel of H1
proof
assume A178:[x,y] in the InternalRel of N_4;
per cases by A178,Th2,ENUMSET1:28;
suppose [x,y] = [0,1];
then x = 0 & y = 1 by ZFMISC_1:33;
hence thesis by A150;
suppose [x,y] = [1,0];
then x = 1 & y = 0 by ZFMISC_1:33;
hence thesis by A154;
suppose [x,y] = [1,2];
then x = 1 & y = 2 by ZFMISC_1:33;
hence thesis by A158;
suppose [x,y] = [2,1];
then x = 2 & y = 1 by ZFMISC_1:33;
hence thesis by A162;
suppose [x,y] = [2,3];
then x = 2 & y = 3 by ZFMISC_1:33;
hence thesis by A166;
suppose [x,y] = [3,2];
then x = 3 & y = 2 by ZFMISC_1:33;
hence thesis by A170;
end;
thus [f.x,f.y] in the InternalRel of H1 implies
[x,y] in the InternalRel of N_4
proof
assume A179: [f.x,f.y] in the InternalRel of H1;
[f.x,f.y] in the InternalRel of S implies
[x,y] in the InternalRel of N_4 by A106;
then [f.x,f.y] in (((A \/ B) \/ C) \/ D) implies
[x,y] in the InternalRel of N_4 by A104,Def3;
then [f.x,f.y] in ((A \/ B) \/ (C\/ D)) implies
[x,y] in the InternalRel of N_4 by XBOOLE_1:4;
then [f.x,f.y] in (A \/ (B\/(C\/D))) implies
[x,y] in the InternalRel of N_4 by XBOOLE_1:4;
hence thesis by A179,XBOOLE_0:def 2;
end;
end;
hence thesis by A105,A176,NECKLACE:def 2;
end;
A180: H1 is strict non empty RelStr by A19,Th4;
H1 is finite by A19,Th4;
then reconsider cH1 as finite set by GROUP_1:def 13;
H2 is finite by A19,Th4;
then reconsider cH2 as finite set by GROUP_1:def 13;
cS = cH1 \/ cH2 by A104,Def3;
then reconsider cS as finite set;
A181: cH1 <> cS
proof
assume A182: cH1 = cS;
A183: cS = cH1 \/ cH2 by A104,Def3;
consider x being set such that A184: x in cH2
by A173,XBOOLE_0:def 1;
cH1 /\ cH2 = {} by A18,XBOOLE_0:def 7;
then not x in cH1 by A184,XBOOLE_0:def 3;
hence contradiction by A182,A183,A184,XBOOLE_0:def 2;
end;
cS = cH1 \/ cH2 by A104,Def3;
then cH1 c= cS by XBOOLE_1:7;
then cH1 c< cS by A181,XBOOLE_0:def 8;
then A185: card cH1 < card cS by CARD_2:67;
thus thesis by A9,A19,A177,A180,A185;
suppose A186: f.0 in the carrier of H2;
A187: f.2 in cH2
proof
now assume f.2 in cH1;
then [f.0,f.2] in D by A186,ZFMISC_1:106;
hence contradiction by A106,A108,A129,A135;
end;
hence thesis by A121,XBOOLE_0:def 2;
end;
A188: f.3 in cH2
proof
now assume f.3 in cH1;
then [f.0,f.3] in D by A186,ZFMISC_1:106;
hence contradiction by A106,A108,A131,A135;
end;
hence thesis by A124,XBOOLE_0:def 2;
end;
A189: f.1 in cH2
proof
now assume f.1 in cH1;
then [f.1,f.3] in C by A188,ZFMISC_1:106;
hence contradiction by A106,A108,A133,A135;
end;
hence thesis by A119,XBOOLE_0:def 2;
end;
set x1=[f.0,f.1], x2=[f.1,f.2], x3=[f.2,f.3],
x4=[f.1,f.0], x5=[f.2,f.1], x6=[f.3,f.2];
x1 in (A \/ B \/ C \/ D) by A104,A116,Def3;
then x1 in ((A \/ B) \/ C ) or x1 in D by XBOOLE_0:def 2;
then A190: x1 in (A \/ B) or x1 in C or x1 in D by XBOOLE_0:def 2;
A191: [f.0,f.1] in B
proof
A192: now assume x1 in A;
then f.0 in dom A & f.1 in rng A by RELAT_1:20;
hence contradiction by A18,A128,A186,XBOOLE_0:3;
end;
A193: now assume x1 in C;
then f.0 in cH1 & f.1 in cH2 by ZFMISC_1:106;
hence contradiction by A18,A186,XBOOLE_0:3;
end;
now assume x1 in D;
then f.0 in cH2 & f.1 in cH1 by ZFMISC_1:106;
hence contradiction by A18,A189,XBOOLE_0:3;
end;
hence thesis by A190,A192,A193,XBOOLE_0:def 2;
end;
x4 in (A \/ B \/ C \/ D) by A104,A117,Def3;
then x4 in ((A\/ B) \/ C) or x4 in D by XBOOLE_0:def 2;
then A194: x4 in (A \/ B) or x4 in C or x4 in D by XBOOLE_0:def 2;
A195: [f.1,f.0] in B
proof
A196: now assume x4 in A;
then f.1 in dom A & f.0 in rng A by RELAT_1:20;
hence contradiction by A18,A128,A189,XBOOLE_0:3;
end;
A197: now assume x4 in C;
then f.1 in cH1 & f.0 in cH2 by ZFMISC_1:106;
hence contradiction by A18,A189,XBOOLE_0:3;
end;
now assume x4 in D;
then f.1 in cH2 & f.0 in cH1 by ZFMISC_1:106;
hence contradiction by A18,A186,XBOOLE_0:3;
end;
hence thesis by A194,A196,A197,XBOOLE_0:def 2;
end;
x2 in (A \/ B \/ C \/ D) by A104,A120,Def3;
then x2 in ((A\/ B) \/ C) or x2 in D by XBOOLE_0:def 2;
then A198: x2 in (A \/ B) or x2 in C or x2 in D by XBOOLE_0:def 2;
A199: [f.1,f.2] in B
proof
A200: now assume x2 in A;
then f.1 in dom A & f.2 in rng A by RELAT_1:20;
hence contradiction by A18,A128,A187,XBOOLE_0:3;
end;
A201: now assume x2 in C;
then f.1 in cH1 & f.2 in cH2 by ZFMISC_1:106;
hence contradiction by A18,A189,XBOOLE_0:3;
end;
now assume x2 in D;
then f.1 in cH2 & f.2 in cH1 by ZFMISC_1:106;
hence contradiction by A18,A187,XBOOLE_0:3;
end;
hence thesis by A198,A200,A201,XBOOLE_0:def 2;
end;
x5 in (A \/ B \/ C \/ D) by A104,A122,Def3;
then x5 in ((A\/ B) \/ C) or x5 in D by XBOOLE_0:def 2;
then A202: x5 in (A \/ B) or x5 in C or x5 in D by XBOOLE_0:def 2;
A203: [f.2,f.1] in B
proof
A204: now assume x5 in A;
then f.2 in dom A & f.1 in rng A by RELAT_1:20;
hence contradiction by A18,A128,A189,XBOOLE_0:3;
end;
A205: now assume x5 in C;
then f.2 in cH1 & f.1 in cH2 by ZFMISC_1:106;
hence contradiction by A18,A187,XBOOLE_0:3;
end;
now assume x5 in D;
then f.2 in cH2 & f.1 in cH1 by ZFMISC_1:106;
hence contradiction by A18,A189,XBOOLE_0:3;
end;
hence thesis by A202,A204,A205,XBOOLE_0:def 2;
end;
x3 in (A \/ B \/ C \/ D) by A104,A123,Def3;
then x3 in ((A\/ B) \/ C) or x3 in D by XBOOLE_0:def 2;
then A206: x3 in (A \/ B) or x3 in C or x3 in D by XBOOLE_0:def 2;
A207: [f.2,f.3] in B
proof
A208: now assume x3 in A;
then f.2 in dom A & f.3 in rng A by RELAT_1:20;
hence contradiction by A18,A128,A187,XBOOLE_0:3;
end;
A209: now assume x3 in C;
then f.2 in cH1 & f.3 in cH2 by ZFMISC_1:106;
hence contradiction by A18,A187,XBOOLE_0:3;
end;
now assume x3 in D;
then f.2 in cH2 & f.3 in cH1 by ZFMISC_1:106;
hence contradiction by A18,A188,XBOOLE_0:3;
end;
hence thesis by A206,A208,A209,XBOOLE_0:def 2;
end;
x6 in (A \/ B \/ C \/ D) by A104,A125,Def3;
then x6 in ((A\/ B) \/ C) or x6 in D by XBOOLE_0:def 2;
then A210: x6 in (A \/ B) or x6 in C or x6 in D by XBOOLE_0:def 2;
A211: [f.3,f.2] in B
proof
A212: now assume x6 in A;
then f.3 in dom A & f.2 in rng A by RELAT_1:20;
hence contradiction by A18,A128,A187,XBOOLE_0:3;
end;
A213: now assume x6 in C;
then f.3 in cH1 & f.2 in cH2 by ZFMISC_1:106;
hence contradiction by A18,A188,XBOOLE_0:3;
end;
now assume x6 in D;
then f.3 in cH2 & f.2 in cH1 by ZFMISC_1:106;
hence contradiction by A18,A187,XBOOLE_0:3;
end;
hence thesis by A210,A212,A213,XBOOLE_0:def 2;
end;
H1 is non empty by A19,Th4;
then A214: the carrier of H1 is non empty by STRUCT_0:def 1;
A215: dom f = the carrier of N_4 by FUNCT_2:def 1;
rng f c= the carrier of H2
proof
let y be set;
assume y in rng f;
then consider x being set such that A216: x in dom f &
y = f.x by FUNCT_1:def 5;
per cases by A215,A216,Lm1,ENUMSET1:18;
suppose x = 0;
hence thesis by A186,A216;
suppose x = 1;
hence thesis by A189,A216;
suppose x = 2;
hence thesis by A187,A216;
suppose x = 3;
hence thesis by A188,A216;
end;
then f is Function of the carrier of N_4,cH2 by FUNCT_2:8;
then A217: f is map of N_4,H2;
A218: H2 embeds N_4
proof
for x,y being Element of N_4
holds [x,y] in the InternalRel of N_4
iff [f.x,f.y] in the InternalRel of H2
proof
let x,y being Element of N_4;
thus [x,y] in the InternalRel of N_4 implies
[f.x,f.y] in the InternalRel of H2
proof
assume A219:[x,y] in the InternalRel of N_4;
per cases by A219,Th2,ENUMSET1:28;
suppose [x,y] = [0,1];
then x = 0 & y = 1 by ZFMISC_1:33;
hence thesis by A191;
suppose [x,y] = [1,0];
then x = 1 & y = 0 by ZFMISC_1:33;
hence thesis by A195;
suppose [x,y] = [1,2];
then x = 1 & y = 2 by ZFMISC_1:33;
hence thesis by A199;
suppose [x,y] = [2,1];
then x = 2 & y = 1 by ZFMISC_1:33;
hence thesis by A203;
suppose [x,y] = [2,3];
then x = 2 & y = 3 by ZFMISC_1:33;
hence thesis by A207;
suppose [x,y] = [3,2];
then x = 3 & y = 2 by ZFMISC_1:33;
hence thesis by A211;
end;
thus [f.x,f.y] in the InternalRel of H2 implies
[x,y] in the InternalRel of N_4
proof
assume A220: [f.x,f.y] in the InternalRel of H2;
[f.x,f.y] in the InternalRel of S implies
[x,y] in the InternalRel of N_4 by A106;
then [f.x,f.y] in (((A \/ B) \/ C) \/ D) implies
[x,y] in the InternalRel of N_4 by A104,Def3;
then [f.x,f.y] in ((A \/ B) \/ (C\/ D)) implies
[x,y] in the InternalRel of N_4 by XBOOLE_1:4;
then [f.x,f.y] in (B \/ (A\/(C\/D))) implies
[x,y] in the InternalRel of N_4 by XBOOLE_1:4;
hence thesis by A220,XBOOLE_0:def 2;
end;
end;
hence thesis by A105,A217,NECKLACE:def 2;
end;
A221: H2 is strict non empty RelStr by A19,Th4;
H1 is finite by A19,Th4;
then reconsider cH1 as finite set by GROUP_1:def 13;
H2 is finite by A19,Th4;
then reconsider cH2 as finite set by GROUP_1:def 13;
cS = cH1 \/ cH2 by A104,Def3;
then reconsider cS as finite set;
A222: cH2 <> cS
proof
assume A223: cH2 = cS;
A224: cS = cH1 \/ cH2 by A104,Def3;
consider x being set such that A225: x in cH1
by A214,XBOOLE_0:def 1;
cH1 /\ cH2 = {} by A18,XBOOLE_0:def 7;
then not x in cH2 by A225,XBOOLE_0:def 3;
hence contradiction by A223,A224,A225,XBOOLE_0:def 2;
end;
cS = cH1 \/ cH2 by A104,Def3;
then cH2 c= cS by XBOOLE_1:7;
then cH2 c< cS by A222,XBOOLE_0:def 8;
then A226: card cH2 < card cS by CARD_2:67;
thus thesis by A9,A19,A218,A221,A226;
end;
hence thesis by A20,A21;
end;
P[0] from Regr(A5,A6);
then consider S being strict non empty RelStr such that
S in fin_RelStr_sp and A227: Card (the carrier of S) = 0 and
S embeds N_4;
thus thesis by A227,CARD_2:59;
end;