let n be Nat; for R being irreflexive NatRelStr of n holds chromatic# (Mycielskian R) = 1 + (chromatic# R)
let R be irreflexive NatRelStr of n; chromatic# (Mycielskian R) = 1 + (chromatic# R)
set cR = the carrier of R;
set iR = the InternalRel of R;
set cnR = chromatic# R;
set MR = Mycielskian R;
set cnMR = chromatic# (Mycielskian R);
set cMR = the carrier of (Mycielskian R);
set iMR = the InternalRel of (Mycielskian R);
A1:
the carrier of R = Segm n
by Def7;
A2:
ex C being finite Coloring of (Mycielskian R) st card C = 1 + (chromatic# R)
proof
consider C being
finite Coloring of
R such that A3:
card C = chromatic# R
by Def3;
defpred S2[
object ,
object ]
means ex
D1 being
set st
(
D1 = $1 & $2
= { (m + n) where m is Element of NAT : m in D1 } );
A4:
for
e being
object st
e in C holds
ex
u being
object st
S2[
e,
u]
consider r being
Function such that
dom r = C
and A5:
for
e being
object st
e in C holds
S2[
e,
r . e]
from CLASSES1:sch 1(A4);
set D =
{ (d \/ (r . d)) where d is Element of C : d in C } ;
A6:
card { (d \/ (r . d)) where d is Element of C : d in C } = card C
proof
per cases
( { (d \/ (r . d)) where d is Element of C : d in C } is empty or not { (d \/ (r . d)) where d is Element of C : d in C } is empty )
;
suppose A9:
not
{ (d \/ (r . d)) where d is Element of C : d in C } is
empty
;
card { (d \/ (r . d)) where d is Element of C : d in C } = card Cdefpred S3[
object ,
object ]
means ex
D1 being
set st
(
D1 = $1 & $2
= D1 \/ (r . $1) );
A10:
for
e being
object st
e in C holds
ex
u being
object st
S3[
e,
u]
proof
let e be
object ;
( e in C implies ex u being object st S3[e,u] )
assume
e in C
;
ex u being object st S3[e,u]
reconsider ee =
e as
set by TARSKI:1;
take u =
ee \/ (r . e);
S3[e,u]
thus
S3[
e,
u]
;
verum
end; consider s being
Function such that A11:
dom s = C
and A12:
for
e being
object st
e in C holds
S3[
e,
s . e]
from CLASSES1:sch 1(A10);
A13:
rng s c= { (d \/ (r . d)) where d is Element of C : d in C }
then reconsider s =
s as
Function of
C,
{ (d \/ (r . d)) where d is Element of C : d in C } by A11, FUNCT_2:2;
{ (d \/ (r . d)) where d is Element of C : d in C } c= rng s
then
rng s = { (d \/ (r . d)) where d is Element of C : d in C }
by A13;
then A18:
s is
onto
by FUNCT_2:def 3;
s is
one-to-one
hence
card { (d \/ (r . d)) where d is Element of C : d in C } = card C
by A18, A9, EULER_1:11;
verum end;
end;
then A33:
{ (d \/ (r . d)) where d is Element of C : d in C } is
finite
;
set E =
{ (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}};
A34:
union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) c= the
carrier of
(Mycielskian R)
A44:
{ (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} c= bool the
carrier of
(Mycielskian R)
A46:
union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) = the
carrier of
(Mycielskian R)
now for A being Subset of the carrier of (Mycielskian R) st A in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} holds
( A <> {} & ( for B being Subset of the carrier of (Mycielskian R) st B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} & A <> B holds
not A meets B ) )let A be
Subset of the
carrier of
(Mycielskian R);
( A in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} implies ( A <> {} & ( for B being Subset of the carrier of (Mycielskian R) st B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} & A <> B holds
not A meets B ) ) )assume A59:
A in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}
;
( A <> {} & ( for B being Subset of the carrier of (Mycielskian R) st B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} & A <> B holds
not A meets B ) )thus
A <> {}
for B being Subset of the carrier of (Mycielskian R) st B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} & A <> B holds
not A meets Blet B be
Subset of the
carrier of
(Mycielskian R);
( B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} & A <> B implies not A meets B )assume A62:
B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}
;
( A <> B implies not A meets B )assume A63:
A <> B
;
not A meets Bassume
A meets B
;
contradictionthen consider x being
object such that A64:
x in A
and A65:
x in B
by XBOOLE_0:3;
per cases
( ( A in { (d \/ (r . d)) where d is Element of C : d in C } & B in { (d \/ (r . d)) where d is Element of C : d in C } ) or ( A in { (d \/ (r . d)) where d is Element of C : d in C } & B in {{(2 * n)}} ) or ( A in {{(2 * n)}} & B in { (d \/ (r . d)) where d is Element of C : d in C } ) or ( A in {{(2 * n)}} & B in {{(2 * n)}} ) )
by A59, A62, XBOOLE_0:def 3;
suppose that A66:
A in { (d \/ (r . d)) where d is Element of C : d in C }
and A67:
B in { (d \/ (r . d)) where d is Element of C : d in C }
;
contradictionconsider d being
Element of
C such that A68:
A = d \/ (r . d)
and A69:
d in C
by A66;
consider e being
Element of
C such that A70:
B = e \/ (r . e)
and A71:
e in C
by A67;
per cases
( ( x in d & x in e ) or ( x in d & x in r . e ) or ( x in r . d & x in e ) or ( x in r . d & x in r . e ) )
by A68, A70, A64, A65, XBOOLE_0:def 3;
suppose that A72:
x in d
and A73:
x in r . e
;
contradictionend; suppose that A75:
x in r . d
and A76:
x in e
;
contradictionend; suppose that A78:
x in r . d
and A79:
x in r . e
;
contradiction
S2[
d,
r . d]
by A69, A5;
then
x in { (m + n) where m is Element of NAT : m in d }
by A78;
then consider ma being
Element of
NAT such that A80:
x = ma + n
and A81:
ma in d
;
S2[
e,
r . e]
by A71, A5;
then
x in { (m + n) where m is Element of NAT : m in e }
by A79;
then consider mb being
Element of
NAT such that A82:
x = mb + n
and A83:
mb in e
;
d meets e
by A80, A82, A81, A83, XBOOLE_0:3;
then
d = e
by A69, A71, EQREL_1:def 4;
hence
contradiction
by A68, A70, A63;
verum end; end; end;
then reconsider E =
{ (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} as
a_partition of the
carrier of
(Mycielskian R) by A44, A46, EQREL_1:def 4;
now for x being set st x in E holds
x is StableSet of (Mycielskian R)let x be
set ;
( x in E implies b1 is StableSet of (Mycielskian R) )assume A100:
x in E
;
b1 is StableSet of (Mycielskian R)per cases
( x in { (d \/ (r . d)) where d is Element of C : d in C } or x in {{(2 * n)}} )
by A100, XBOOLE_0:def 3;
suppose
x in { (d \/ (r . d)) where d is Element of C : d in C }
;
b1 is StableSet of (Mycielskian R)then consider d being
Element of
C such that A101:
x = d \/ (r . d)
and A102:
d in C
;
reconsider d =
d as
Subset of
R by A102;
S2[
d,
r . d]
by A102, A5;
then A103:
r . d = { (m + n) where m is Element of NAT : m in d }
;
A104:
x c= the
carrier of
(Mycielskian R)
A110:
now for x being Nat st x in r . d holds
( n <= x & x < 2 * n )end; A113:
d is
stable
by DILWORTH:def 12;
now for a, b being Element of (Mycielskian R) st a in x & b in x & a <> b holds
( not a <= b & not b <= a )let a,
b be
Element of
(Mycielskian R);
( a in x & b in x & a <> b implies ( not a <= b & not b <= a ) )assume that A114:
a in x
and A115:
b in x
and A116:
a <> b
and A117:
(
a <= b or
b <= a )
;
contradictionA118:
(
[a,b] in the
InternalRel of
(Mycielskian R) or
[b,a] in the
InternalRel of
(Mycielskian R) )
by A117, ORDERS_2:def 5;
per cases
( ( a in d & b in d ) or ( a in d & b in r . d ) or ( a in r . d & b in d ) or ( a in r . d & b in r . d ) )
by A114, A115, A101, XBOOLE_0:def 3;
suppose that A121:
a in d
and A122:
b in r . d
;
contradictionconsider bm being
Element of
NAT such that A123:
b = bm + n
and A124:
bm in d
by A122, A103;
a in Segm n
by A121, A1;
then reconsider ap1 =
a as
Nat ;
A125:
(
[ap1,bm] in the
InternalRel of
R or
[bm,ap1] in the
InternalRel of
R )
by A118, Th42, Th43, A123, A121, A1;
reconsider bmp1 =
bm,
a =
a as
Element of
R by A124, A121;
A126:
(
bmp1 <= a or
a <= bmp1 )
by A125, ORDERS_2:def 5;
bmp1 <> a
by A125, A121, NECKLACE:def 5;
hence
contradiction
by A126, A124, A121, A113;
verum end; suppose that A127:
a in r . d
and A128:
b in d
;
contradictionconsider am being
Element of
NAT such that A129:
a = am + n
and A130:
am in d
by A127, A103;
b in Segm n
by A128, A1;
then reconsider bp1 =
b as
Nat ;
A131:
(
[am,bp1] in the
InternalRel of
R or
[bp1,am] in the
InternalRel of
R )
by A118, Th42, Th43, A129, A128, A1;
reconsider amp1 =
am,
b =
b as
Element of
R by A130, A128;
A132:
(
amp1 <= b or
b <= amp1 )
by A131, ORDERS_2:def 5;
amp1 <> b
by A131, A128, NECKLACE:def 5;
hence
contradiction
by A132, A130, A128, A113;
verum end; suppose that A133:
a in r . d
and A134:
b in r . d
;
contradictionend; end; hence
x is
StableSet of
(Mycielskian R)
by A104, DILWORTH:def 2;
verum end; end;
then reconsider E =
E as
Coloring of
(Mycielskian R) by DILWORTH:def 12;
take
E
;
card E = 1 + (chromatic# R)
hence
card E = 1
+ (chromatic# R)
by A6, A33, A3, CARD_2:41;
verum
end;
for C being finite Coloring of (Mycielskian R) holds 1 + (chromatic# R) <= card C
proof
let E be
finite Coloring of
(Mycielskian R);
1 + (chromatic# R) <= card E
assume
1
+ (chromatic# R) > card E
;
contradiction
then A145:
chromatic# R >= card E
by NAT_1:13;
A146:
chromatic# (Mycielskian R) <= card E
by Def3;
then A147:
chromatic# (Mycielskian R) <= chromatic# R
by A145, XXREAL_0:2;
n <= n + n
by NAT_1:11;
then
n < (2 * n) + 1
by NAT_1:13;
then
Segm n c= Segm ((2 * n) + 1)
by NAT_1:39;
then reconsider S =
n as
Subset of
(Mycielskian R) by Def7;
A148:
R = subrelstr S
by Th45;
then
chromatic# R <= chromatic# (Mycielskian R)
by Th47;
then
chromatic# R = chromatic# (Mycielskian R)
by A147, XXREAL_0:1;
then A149:
card E = chromatic# R
by A145, A146, XXREAL_0:1;
reconsider C =
E | S as
Coloring of
R by A148, Th10;
A150:
card C >= chromatic# R
by Def3;
A151:
card C <= card E
by Th8;
then A152:
card C = chromatic# R
by A149, A150, XXREAL_0:1;
2
* n < (2 * n) + 1
by NAT_1:13;
then
2
* n in Segm ((2 * n) + 1)
by NAT_1:44;
then
2
* n in the
carrier of
(Mycielskian R)
by Def7;
then
2
* n in union E
by EQREL_1:def 4;
then consider e being
set such that A153:
2
* n in e
and A154:
e in E
by TARSKI:def 4;
reconsider e =
e as
Subset of
(Mycielskian R) by A154;
reconsider n2 = 2
* n as
Element of
(Mycielskian R) by A153, A154;
set se =
e /\ S;
e meets S
by A149, A152, A154, Th9;
then A155:
e /\ S in C
by A154;
then consider mp1 being
Element of
R such that A156:
mp1 in e /\ S
and A157:
for
d being
Element of
C st
d <> e /\ S holds
ex
w being
Element of
R st
(
w in Adjacent mp1 &
w in d )
by A151, A149, A150, Th31, XXREAL_0:1;
mp1 in Segm n
by A156, A155;
then reconsider m =
mp1 as
Nat ;
set mn =
m + n;
A158:
0 + n <= m + n
by XREAL_1:6;
m in Segm n
by A156, A155;
then
m < n
by NAT_1:44;
then A159:
m + n < n + n
by XREAL_1:6;
then
m + n < (2 * n) + 1
by NAT_1:13;
then A160:
m + n in Segm ((2 * n) + 1)
by NAT_1:44;
then
m + n in the
carrier of
(Mycielskian R)
by Def7;
then
m + n in union E
by EQREL_1:def 4;
then consider f being
set such that A161:
m + n in f
and A162:
f in E
by TARSKI:def 4;
reconsider f =
f as
Subset of
(Mycielskian R) by A162;
reconsider mnp1 =
m + n as
Element of
(Mycielskian R) by A160, Def7;
A163:
now not e <> fassume A164:
e <> f
;
contradictionset sf =
f /\ S;
f meets S
by A149, A152, A162, Th9;
then A165:
f /\ S in C
by A162;
A166:
f /\ S c= f
by XBOOLE_1:17;
then consider wp1 being
Element of
R such that A169:
wp1 in Adjacent mp1
and A170:
wp1 in f /\ S
by A165, A157;
wp1 in Segm n
by A170, A165;
then reconsider w =
wp1 as
Nat ;
w in Segm n
by A170, A165;
then A171:
w < n
by NAT_1:44;
(
mp1 < wp1 or
wp1 < mp1 )
by A169, Def6;
then
(
mp1 <= wp1 or
wp1 <= mp1 )
by ORDERS_2:def 6;
then
(
[m,w] in the
InternalRel of
R or
[w,m] in the
InternalRel of
R )
by ORDERS_2:def 5;
then A172:
(
[(m + n),w] in the
InternalRel of
(Mycielskian R) or
[w,(m + n)] in the
InternalRel of
(Mycielskian R) )
by Th41;
reconsider wp2 =
wp1 as
Element of
(Mycielskian R) by A170;
f is
stable
by A162, DILWORTH:def 12;
then
( not
wp2 <= mnp1 & not
mnp1 <= wp2 )
by A171, A158, A170, A166, A161;
hence
contradiction
by A172, ORDERS_2:def 5;
verum end;
A173:
[(m + n),(2 * n)] in the
InternalRel of
(Mycielskian R)
by A159, A158, Th44;
e is
stable
by A154, DILWORTH:def 12;
then
( not
mnp1 <= n2 & not
n2 <= mnp1 )
by A153, A161, A163, A159;
hence
contradiction
by A173, ORDERS_2:def 5;
verum
end;
hence
chromatic# (Mycielskian R) = 1 + (chromatic# R)
by A2, Def3; verum