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 = 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 S1[
set ,
set ]
means $2
= { (m + n) where m is Element of NAT : m in $1 } ;
A4:
for
e being
set st
e in C holds
ex
u being
set st
S1[
e,
u]
;
consider r being
Function such that
dom r = C
and A5:
for
e being
set st
e in C holds
S1[
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
then A30:
{ (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)}};
A31:
union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) c= the
carrier of
(Mycielskian R)
A41:
{ (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} c= bool the
carrier of
(Mycielskian R)
A43:
union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) = the
carrier of
(Mycielskian R)
now 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 A56:
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 A59:
B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}
;
( A <> B implies not A meets B )assume A60:
A <> B
;
not A meets Bassume
A meets B
;
contradictionthen consider x being
set such that A61:
x in A
and A62:
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 A56, A59, XBOOLE_0:def 3;
suppose that A63:
A in { (d \/ (r . d)) where d is Element of C : d in C }
and A64:
B in { (d \/ (r . d)) where d is Element of C : d in C }
;
contradictionconsider d being
Element of
C such that A65:
A = d \/ (r . d)
and A66:
d in C
by A63;
consider e being
Element of
C such that A67:
B = e \/ (r . e)
and A68:
e in C
by A64;
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 A65, A67, A61, A62, XBOOLE_0:def 3;
suppose that A69:
x in d
and A70:
x in r . e
;
contradictionend; suppose that A72:
x in r . d
and A73:
x in e
;
contradictionend; suppose that A75:
x in r . d
and A76:
x in r . e
;
contradiction
x in { (m + n) where m is Element of NAT : m in d }
by A75, A66, A5;
then consider ma being
Element of
NAT such that A77:
x = ma + n
and A78:
ma in d
;
x in { (m + n) where m is Element of NAT : m in e }
by A76, A68, A5;
then consider mb being
Element of
NAT such that A79:
x = mb + n
and A80:
mb in e
;
d meets e
by A77, A79, A78, A80, XBOOLE_0:3;
then
d = e
by A66, A68, EQREL_1:def 4;
hence
contradiction
by A65, A67, A60;
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 A41, A43, EQREL_1:def 4;
now let x be
set ;
( x in E implies b1 is StableSet of (Mycielskian R) )assume A95:
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 A95, 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 A96:
x = d \/ (r . d)
and A97:
d in C
;
reconsider d =
d as
Subset of
R by A97;
A98:
r . d = { (m + n) where m is Element of NAT : m in d }
by A97, A5;
A99:
x c= the
carrier of
(Mycielskian R)
A108:
d is
stable
by A97, DILWORTH:def 12;
now 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 A109:
a in x
and A110:
b in x
and A111:
a <> b
and A112:
(
a <= b or
b <= a )
;
contradictionA113:
(
[a,b] in the
InternalRel of
(Mycielskian R) or
[b,a] in the
InternalRel of
(Mycielskian R) )
by A112, 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 A109, A110, A96, XBOOLE_0:def 3;
suppose that A116:
a in d
and A117:
b in r . d
;
contradictionconsider bm being
Element of
NAT such that A118:
b = bm + n
and A119:
bm in d
by A117, A98;
reconsider ap1 =
a as
Nat by A116, A1, NECKLACE:3;
A120:
(
[ap1,bm] in the
InternalRel of
R or
[bm,ap1] in the
InternalRel of
R )
by A113, Th42, Th43, A118, A116, A1;
reconsider bmp1 =
bm,
a =
a as
Element of
R by A119, A116;
A121:
(
bmp1 <= a or
a <= bmp1 )
by A120, ORDERS_2:def 5;
bmp1 <> a
by A120, A116, NECKLACE:def 5;
hence
contradiction
by A121, A119, A116, A108, DILWORTH:def 2;
verum end; suppose that A122:
a in r . d
and A123:
b in d
;
contradictionconsider am being
Element of
NAT such that A124:
a = am + n
and A125:
am in d
by A122, A98;
reconsider bp1 =
b as
Nat by A123, A1, NECKLACE:3;
A126:
(
[am,bp1] in the
InternalRel of
R or
[bp1,am] in the
InternalRel of
R )
by A113, Th42, Th43, A124, A123, A1;
reconsider amp1 =
am,
b =
b as
Element of
R by A125, A123;
A127:
(
amp1 <= b or
b <= amp1 )
by A126, ORDERS_2:def 5;
amp1 <> b
by A126, A123, NECKLACE:def 5;
hence
contradiction
by A127, A125, A123, A108, DILWORTH:def 2;
verum end; suppose that A128:
a in r . d
and A129:
b in r . d
;
contradictionend; end; hence
x is
StableSet of
(Mycielskian R)
by A99, 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, A30, 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 A139:
chromatic# R >= card E
by NAT_1:13;
A140:
chromatic# (Mycielskian R) <= card E
by Def3;
then A141:
chromatic# (Mycielskian R) <= chromatic# R
by A139, XXREAL_0:2;
n <= n + n
by NAT_1:11;
then
n < (2 * n) + 1
by NAT_1:13;
then
n c= (2 * n) + 1
by NAT_1:39;
then reconsider S =
n as
Subset of
(Mycielskian R) by Def7;
A142:
R = subrelstr S
by Th45;
then
chromatic# R <= chromatic# (Mycielskian R)
by Th47;
then
chromatic# R = chromatic# (Mycielskian R)
by A141, XXREAL_0:1;
then A143:
card E = chromatic# R
by A139, A140, XXREAL_0:1;
reconsider C =
E | S as
Coloring of
R by A142, Th10;
A144:
card C >= chromatic# R
by Def3;
A145:
card C <= card E
by Th8;
then A146:
card C = chromatic# R
by A143, A144, XXREAL_0:1;
2
* n < (2 * n) + 1
by NAT_1:13;
then
2
* n in (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 A147:
2
* n in e
and A148:
e in E
by TARSKI:def 4;
reconsider e =
e as
Subset of
(Mycielskian R) by A148;
reconsider n2 = 2
* n as
Element of
(Mycielskian R) by A147, A148;
set se =
e /\ S;
e meets S
by A143, A146, A148, Th9;
then A149:
e /\ S in C
by A148;
then consider mp1 being
Element of
R such that A150:
mp1 in e /\ S
and A151:
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 A145, A143, A144, Th31, XXREAL_0:1;
reconsider m =
mp1 as
Nat by A150, A149, NECKLACE:3;
set mn =
m + n;
A152:
0 + n <= m + n
by XREAL_1:6;
m < n
by A150, A149, NAT_1:44;
then A153:
m + n < n + n
by XREAL_1:6;
then
m + n < (2 * n) + 1
by NAT_1:13;
then A154:
m + n in (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 A155:
m + n in f
and A156:
f in E
by TARSKI:def 4;
reconsider f =
f as
Subset of
(Mycielskian R) by A156;
reconsider mnp1 =
m + n as
Element of
(Mycielskian R) by A154, Def7;
A157:
now assume A158:
e <> f
;
contradictionset sf =
f /\ S;
f meets S
by A143, A146, A156, Th9;
then A159:
f /\ S in C
by A156;
A160:
f /\ S c= f
by XBOOLE_1:17;
then consider wp1 being
Element of
R such that A163:
wp1 in Adjacent mp1
and A164:
wp1 in f /\ S
by A159, A151;
reconsider w =
wp1 as
Nat by A164, A159, NECKLACE:3;
A165:
w < n
by A164, A159, NAT_1:44;
(
mp1 < wp1 or
wp1 < mp1 )
by A163, 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 A166:
(
[(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 A164;
f is
stable
by A156, DILWORTH:def 12;
then
( not
wp2 <= mnp1 & not
mnp1 <= wp2 )
by A165, A152, A164, A160, A155, DILWORTH:def 2;
hence
contradiction
by A166, ORDERS_2:def 5;
verum end;
A167:
[(m + n),(2 * n)] in the
InternalRel of
(Mycielskian R)
by A153, A152, Th44;
e is
stable
by A148, DILWORTH:def 12;
then
( not
mnp1 <= n2 & not
n2 <= mnp1 )
by A147, A155, A157, A153, DILWORTH:def 2;
hence
contradiction
by A167, ORDERS_2:def 5;
verum
end;
hence
chromatic# (Mycielskian R) = 1 + (chromatic# R)
by A2, Def3; verum