let R be with_finite_chromatic# RelStr ; :: thesis: for C being finite Coloring of R
for c being set st c in C & card C = chromatic# R holds
ex v being Element of R st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of R st
( w in Adjacent v & w in d ) ) )
let C be finite Coloring of R; :: thesis: for c being set st c in C & card C = chromatic# R holds
ex v being Element of R st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of R st
( w in Adjacent v & w in d ) ) )
let c be set ; :: thesis: ( c in C & card C = chromatic# R implies ex v being Element of R st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of R st
( w in Adjacent v & w in d ) ) ) )
assume that
A1: c in C and
A2: card C = chromatic# R ; :: thesis: ex v being Element of R st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of R st
( w in Adjacent v & w in d ) ) )
assume A3: for v being Element of R holds
( not v in c or ex d being Element of C st
( d <> c & ( for w being Element of R holds
( not w in Adjacent v or not w in d ) ) ) ) ; :: thesis: contradiction
set cR = the carrier of R;
A4: union C = the carrier of R by EQREL_1:def 4;
reconsider c = c as Subset of the carrier of R by A1;
A5: c <> {} by A1, EQREL_1:def 4;
set Cc = C \ {c};
A6: c in {c} by TARSKI:def 1;
per cases ( C \ {c} is empty or not C \ {c} is empty ) ;
suppose A7: C \ {c} is empty ; :: thesis: contradiction
consider v being set such that
A8: v in c by A5, XBOOLE_0:def 1;
reconsider v = v as Element of R by A8;
consider d being Element of C such that
A9: d <> c and
for w being Element of R holds
( not w in Adjacent v or not w in d ) by A8, A3;
0 = (card C) - (card {c}) by A1, A7, CARD_1:27, EULER_1:4;
then 0 + 1 = ((card C) - 1) + 1 by CARD_1:30;
then consider x being set such that
A10: C = {x} by CARD_2:42;
( c = x & d = x ) by A1, A10, TARSKI:def 1;
hence contradiction by A9; :: thesis: verum
end;
suppose not C \ {c} is empty ; :: thesis: contradiction
then reconsider Cc = C \ {c} as non empty set ;
defpred S1[ set , set ] means for vv being Element of the carrier of R st $1 = vv holds
( $2 <> c & $2 in C & ( for w being Element of R holds
( not w in Adjacent vv or not w in $2 ) ) );
A11: for e being set st e in c holds
ex u being set st S1[e,u]
proof
let v be set ; :: thesis: ( v in c implies ex u being set st S1[v,u] )
assume A12: v in c ; :: thesis: ex u being set st S1[v,u]
reconsider vv = v as Element of the carrier of R by A12;
consider d being Element of C such that
A13: d <> c and
A14: for w being Element of R holds
( not w in Adjacent vv or not w in d ) by A12, A3;
take d ; :: thesis: S1[v,d]
thus S1[v,d] by A13, A14, A1; :: thesis: verum
end;
consider r being Function such that
A15: dom r = c and
A16: for e being set st e in c holds
S1[e,r . e] from CLASSES1:sch 1(A11);
defpred S2[ set ] means verum;
deffunc H1( set ) -> set = $1 \/ (r " {$1});
reconsider Cc = Cc as non empty finite set ;
set D = { H1(d) where d is Element of Cc : S2[d] } ;
consider d being set such that
A17: d in Cc by XBOOLE_0:def 1;
A18: d \/ (r " {d}) in { H1(d) where d is Element of Cc : S2[d] } by A17;
A19: { H1(d) where d is Element of Cc : S2[d] } c= bool the carrier of R
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { H1(d) where d is Element of Cc : S2[d] } or x in bool the carrier of R )
assume x in { H1(d) where d is Element of Cc : S2[d] } ; :: thesis: x in bool the carrier of R
then consider d being Element of Cc such that
A20: x = d \/ (r " {d}) ;
A21: r " {d} c= c by A15, RELAT_1:132;
A22: r " {d} c= the carrier of R by A21, XBOOLE_1:1;
d in C by XBOOLE_0:def 5;
then x c= the carrier of R by A20, A22, XBOOLE_1:8;
hence x in bool the carrier of R ; :: thesis: verum
end;
A23: union { H1(d) where d is Element of Cc : S2[d] } = the carrier of R
proof
thus union { H1(d) where d is Element of Cc : S2[d] } c= the carrier of R :: according to XBOOLE_0:def 10 :: thesis: the carrier of R c= union { H1(d) where d is Element of Cc : S2[d] }
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union { H1(d) where d is Element of Cc : S2[d] } or x in the carrier of R )
assume x in union { H1(d) where d is Element of Cc : S2[d] } ; :: thesis: x in the carrier of R
then consider Y being set such that
A24: x in Y and
A25: Y in { H1(d) where d is Element of Cc : S2[d] } by TARSKI:def 4;
thus x in the carrier of R by A24, A25, A19; :: thesis: verum
end;
thus the carrier of R c= union { H1(d) where d is Element of Cc : S2[d] } :: thesis: verum
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of R or x in union { H1(d) where d is Element of Cc : S2[d] } )
assume A26: x in the carrier of R ; :: thesis: x in union { H1(d) where d is Element of Cc : S2[d] }
then consider d being set such that
A27: x in d and
A28: d in C by A4, TARSKI:def 4;
reconsider xp1 = x as Element of the carrier of R by A26;
per cases ( d = c or d <> c ) ;
suppose A29: d = c ; :: thesis: x in union { H1(d) where d is Element of Cc : S2[d] }
then r . xp1 <> c by A27, A16;
then A30: not r . xp1 in {c} by TARSKI:def 1;
r . xp1 in C by A27, A29, A16;
then A31: r . xp1 in Cc by A30, XBOOLE_0:def 5;
r . xp1 in {(r . xp1)} by TARSKI:def 1;
then x in r " {(r . xp1)} by A27, A29, A15, FUNCT_1:def 7;
then A32: x in (r . xp1) \/ (r " {(r . xp1)}) by XBOOLE_0:def 3;
(r . xp1) \/ (r " {(r . xp1)}) in { H1(d) where d is Element of Cc : S2[d] } by A31;
hence x in union { H1(d) where d is Element of Cc : S2[d] } by A32, TARSKI:def 4; :: thesis: verum
end;
suppose d <> c ; :: thesis: x in union { H1(d) where d is Element of Cc : S2[d] }
then not d in {c} by TARSKI:def 1;
then d in Cc by A28, XBOOLE_0:def 5;
then A33: d \/ (r " {d}) in { H1(d) where d is Element of Cc : S2[d] } ;
x in d \/ (r " {d}) by A27, XBOOLE_0:def 3;
hence x in union { H1(d) where d is Element of Cc : S2[d] } by A33, TARSKI:def 4; :: thesis: verum
end;
end;
end;
end;
A34: for A being Subset of the carrier of R st A in { H1(d) where d is Element of Cc : S2[d] } holds
( A <> {} & ( for B being Subset of the carrier of R holds
( not B in { H1(d) where d is Element of Cc : S2[d] } or A = B or A misses B ) ) )
proof
let A be Subset of the carrier of R; :: thesis: ( A in { H1(d) where d is Element of Cc : S2[d] } implies ( A <> {} & ( for B being Subset of the carrier of R holds
( not B in { H1(d) where d is Element of Cc : S2[d] } or A = B or A misses B ) ) ) )
assume A in { H1(d) where d is Element of Cc : S2[d] } ; :: thesis: ( A <> {} & ( for B being Subset of the carrier of R holds
( not B in { H1(d) where d is Element of Cc : S2[d] } or A = B or A misses B ) ) )
then consider da being Element of Cc such that
A35: A = da \/ (r " {da}) ;
A36: da in C by XBOOLE_0:def 5;
then not da is empty by EQREL_1:def 4;
hence A <> {} by A35; :: thesis: for B being Subset of the carrier of R holds
( not B in { H1(d) where d is Element of Cc : S2[d] } or A = B or A misses B )
let B be Subset of the carrier of R; :: thesis: ( not B in { H1(d) where d is Element of Cc : S2[d] } or A = B or A misses B )
assume B in { H1(d) where d is Element of Cc : S2[d] } ; :: thesis: ( A = B or A misses B )
then consider db being Element of Cc such that
A37: B = db \/ (r " {db}) ;
A38: db in C by XBOOLE_0:def 5;
per cases ( da = db or da <> db ) ;
suppose da = db ; :: thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A35, A37; :: thesis: verum
end;
suppose A39: da <> db ; :: thesis: ( A = B or A misses B )
then A40: da misses db by A36, A38, EQREL_1:def 4;
A41: r " {da} misses r " {db} by A39, FUNCT_1:71, ZFMISC_1:11;
assume A <> B ; :: thesis: A misses B
assume A meets B ; :: thesis: contradiction
then consider x being set such that
A42: x in A and
A43: x in B by XBOOLE_0:3;
per cases ( ( x in da & x in db ) or ( x in da & x in r " {db} ) or ( x in r " {da} & x in db ) or ( x in r " {da} & x in r " {db} ) ) by A42, A43, A35, A37, XBOOLE_0:def 3;
suppose ( x in r " {da} & x in r " {db} ) ; :: thesis: contradiction
hence contradiction by A41, XBOOLE_0:3; :: thesis: verum
end;
end;
end;
end;
end;
reconsider D = { H1(d) where d is Element of Cc : S2[d] } as a_partition of the carrier of R by A19, A23, A34, EQREL_1:def 4;
now
let x be set ; :: thesis: ( x in D implies x is StableSet of R )
assume A50: x in D ; :: thesis: x is StableSet of R
then reconsider S = x as Subset of R ;
consider d being Element of Cc such that
A51: x = d \/ (r " {d}) by A50;
A52: r " {d} c= c by A15, RELAT_1:132;
A53: d in C by XBOOLE_0:def 5;
A54: d is StableSet of R by A53, DILWORTH:def 12;
A55: c is StableSet of R by A1, DILWORTH:def 12;
S is stable
proof
let a, b be Element of R; :: according to DILWORTH:def 2 :: thesis: ( not a in S or not b in S or a = b or ( not a <= b & not b <= a ) )
assume that
A56: a in S and
A57: b in S and
A58: a <> b ; :: thesis: ( not a <= b & not b <= a )
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 A56, A57, A51, XBOOLE_0:def 3;
suppose ( a in d & b in d ) ; :: thesis: ( not a <= b & not b <= a )
hence ( not a <= b & not b <= a ) by A54, A58, DILWORTH:def 2; :: thesis: verum
end;
suppose that A59: a in d and
A60: b in r " {d} ; :: thesis: ( not a <= b & not b <= a )
r . b in {d} by A60, FUNCT_1:def 7;
then r . b = d by TARSKI:def 1;
then not a in Adjacent b by A59, A52, A60, A16;
then ( not a < b & not b < a ) by Def6;
hence ( not a <= b & not b <= a ) by A58, ORDERS_2:def 6; :: thesis: verum
end;
suppose that A61: a in r " {d} and
A62: b in d ; :: thesis: ( not a <= b & not b <= a )
r . a in {d} by A61, FUNCT_1:def 7;
then r . a = d by TARSKI:def 1;
then not b in Adjacent a by A62, A52, A61, A16;
then ( not a < b & not b < a ) by Def6;
hence ( not a <= b & not b <= a ) by A58, ORDERS_2:def 6; :: thesis: verum
end;
suppose ( a in r " {d} & b in r " {d} ) ; :: thesis: ( not a <= b & not b <= a )
hence ( not a <= b & not b <= a ) by A52, A55, A58, DILWORTH:def 2; :: thesis: verum
end;
end;
end;
hence x is StableSet of R ; :: thesis: verum
end;
then reconsider D = D as Coloring of R by DILWORTH:def 12;
card Cc = (card C) - (card {c}) by A1, EULER_1:4;
then (card Cc) + 1 = ((card C) - 1) + 1 by CARD_1:30;
then A63: card Cc < card C by NAT_1:13;
deffunc H2( set ) -> set = $1 \/ (r " {$1});
consider s being Function such that
A64: dom s = Cc and
A65: for x being set st x in Cc holds
s . x = H2(x) from FUNCT_1:sch 3();
A66: rng s c= D
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s or y in D )
assume y in rng s ; :: thesis: y in D
then consider d being set such that
A67: d in dom s and
A68: y = s . d by FUNCT_1:def 3;
y = d \/ (r " {d}) by A64, A65, A67, A68;
hence y in D by A67, A64; :: thesis: verum
end;
then reconsider s = s as Function of Cc,D by A64, FUNCT_2:2;
A69: s is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 s or not x2 in proj1 s or not s . x1 = s . x2 or x1 = x2 )
assume that
A70: x1 in dom s and
A71: x2 in dom s and
A72: s . x1 = s . x2 ; :: thesis: x1 = x2
A73: s . x1 = x1 \/ (r " {x1}) by A70, A65;
A74: s . x2 = x2 \/ (r " {x2}) by A71, A65;
thus x1 c= x2 :: according to XBOOLE_0:def 10 :: thesis: x2 c= x1
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in x1 or x in x2 )
assume A75: x in x1 ; :: thesis: x in x2
then A76: x in s . x1 by A73, XBOOLE_0:def 3;
per cases ( x in x2 or x in r " {x2} ) by A76, A72, A74, XBOOLE_0:def 3;
suppose x in x2 ; :: thesis: x in x2
hence x in x2 ; :: thesis: verum
end;
suppose A77: x in r " {x2} ; :: thesis: x in x2
A78: r " {x2} c= dom r by RELAT_1:132;
A79: x1 in C by A70, XBOOLE_0:def 5;
then reconsider x1 = x1 as Subset of the carrier of R ;
x1 meets c by A78, A77, A15, A75, XBOOLE_0:3;
then x1 = c by A79, A1, EQREL_1:def 4;
hence x in x2 by A6, A70, XBOOLE_0:def 5; :: thesis: verum
end;
end;
end;
thus x2 c= x1 :: thesis: verum
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in x2 or x in x1 )
assume A80: x in x2 ; :: thesis: x in x1
then A81: x in s . x2 by A74, XBOOLE_0:def 3;
per cases ( x in x1 or x in r " {x1} ) by A81, A72, A73, XBOOLE_0:def 3;
suppose x in x1 ; :: thesis: x in x1
hence x in x1 ; :: thesis: verum
end;
suppose A82: x in r " {x1} ; :: thesis: x in x1
A83: r " {x1} c= dom r by RELAT_1:132;
A84: x2 in C by A71, XBOOLE_0:def 5;
then reconsider x2 = x2 as Subset of the carrier of R ;
x2 meets c by A83, A82, A15, A80, XBOOLE_0:3;
then x2 = c by A84, A1, EQREL_1:def 4;
hence x in x1 by A6, A71, XBOOLE_0:def 5; :: thesis: verum
end;
end;
end;
end;
D c= rng s
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in rng s )
assume x in D ; :: thesis: x in rng s
then consider d being Element of Cc such that
A85: x = d \/ (r " {d}) ;
s . d = d \/ (r " {d}) by A65;
hence x in rng s by A85, A64, FUNCT_1:def 3; :: thesis: verum
end;
then D = rng s by A66, XBOOLE_0:def 10;
then s is onto by FUNCT_2:def 3;
then A86: card Cc = card D by A69, A18, EULER_1:11;
then D is finite ;
hence contradiction by A63, A86, A2, Def3; :: thesis: verum
end;
end;