let R be RelStr ; ( R is with_finite_clique# & R is with_finite_stability# implies R is finite )
assume A1:
R is with_finite_clique#
; ( not R is with_finite_stability# or R is finite )
assume A2:
R is with_finite_stability#
; R is finite
assume A3:
R is infinite
; contradiction
reconsider R = R as with_finite_clique# with_finite_stability# RelStr by A1, A2;
consider C being finite Clique of R such that
A4:
card C = clique# R
by Def4;
consider An being finite StableSet of R such that
A5:
card An = stability# R
by Def6;
set h = clique# R;
set w = stability# R;
A6:
0 + 1 <= clique# R
by A3, NAT_1:13;
A7:
0 + 1 <= stability# R
by A3, NAT_1:13;
set cR = the carrier of R;
A8:
the carrier of R = [#] R
;
per cases
( clique# R = 1 or stability# R = 1 or ( clique# R > 1 & stability# R > 1 ) )
by A6, A7, XXREAL_0:1;
suppose A13:
(
clique# R > 1 &
stability# R > 1 )
;
contradictionset m =
(max ((clique# R),(stability# R))) + 1;
reconsider m =
(max ((clique# R),(stability# R))) + 1 as
Nat ;
consider r being
Nat such that A14:
for
X being
finite set for
P being
a_partition of
the_subsets_of_card (2,
X) st
card X >= r &
card P = 2 holds
ex
S being
Subset of
X st
(
card S >= m &
S is_homogeneous_for P )
by RAMSEY_1:17;
consider Y being
finite Subset of
R such that A15:
card Y > r
by A3, Th5;
set X =
(Y \/ An) \/ C;
reconsider X =
(Y \/ An) \/ C as
finite Subset of
R ;
(
Y c= Y \/ An &
Y \/ An c= (Y \/ An) \/ C )
by XBOOLE_1:7;
then A16:
card Y <= card X
by NAT_1:43, XBOOLE_1:1;
set A =
{ {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } ;
set B =
{ {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ;
set E =
the_subsets_of_card (2,
X);
set P =
{ { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } };
A17:
{ {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } c= the_subsets_of_card (2,
X)
proof
let x be
object ;
TARSKI:def 3 ( not x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or x in the_subsets_of_card (2,X) )
reconsider x1 =
x as
set by TARSKI:1;
assume
x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) }
;
x in the_subsets_of_card (2,X)
then consider xx,
yy being
Element of
R such that A18:
{xx,yy} = x
and A19:
xx <> yy
and A20:
xx in X
and A21:
yy in X
and
(
xx <= yy or
yy <= xx )
;
(
x is
Subset of
X &
card x1 = 2 )
by A18, A19, A20, A21, CARD_2:57, ZFMISC_1:32;
hence
x in the_subsets_of_card (2,
X)
;
verum
end; A22:
{ {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } c= the_subsets_of_card (2,
X)
proof
let x be
object ;
TARSKI:def 3 ( not x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } or x in the_subsets_of_card (2,X) )
reconsider x1 =
x as
set by TARSKI:1;
assume
x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) }
;
x in the_subsets_of_card (2,X)
then consider xx,
yy being
Element of
R such that A23:
{xx,yy} = x
and A24:
xx <> yy
and A25:
xx in X
and A26:
yy in X
and
( not
xx <= yy & not
yy <= xx )
;
(
x is
Subset of
X &
card x1 = 2 )
by A23, A24, A25, A26, CARD_2:57, ZFMISC_1:32;
hence
x in the_subsets_of_card (2,
X)
;
verum
end; A27:
(
{ {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } &
{ {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } )
by TARSKI:def 2;
A28:
now not { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } assume A29:
{ {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) }
;
contradictionconsider a,
b being
set such that A30:
a in An
and A31:
b in An
and A32:
a <> b
by A13, A5, NAT_1:59;
reconsider a =
a,
b =
b as
Element of
R by A30, A31;
A33:
( not
a <= b & not
b <= a )
by A30, A31, A32, Def2;
(
a in Y \/ An &
b in Y \/ An )
by A30, A31, XBOOLE_0:def 3;
then
(
a in X &
b in X )
by XBOOLE_0:def 3;
then
{a,b} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) }
by A33, A32;
then consider aa,
bb being
Element of
R such that A34:
{a,b} = {aa,bb}
and
(
aa <> bb &
aa in X &
bb in X )
and A35:
(
aa <= bb or
bb <= aa )
by A29;
( (
a = aa &
b = bb ) or (
a = bb &
b = aa ) )
by A34, ZFMISC_1:6;
hence
contradiction
by A35, A30, A31, A32, Def2;
verum end; A36:
{ { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } c= bool (the_subsets_of_card (2,X))
proof
let x be
object ;
TARSKI:def 3 ( not x in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or x in bool (the_subsets_of_card (2,X)) )
reconsider xx =
x as
set by TARSKI:1;
assume
x in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } }
;
x in bool (the_subsets_of_card (2,X))
then
xx c= the_subsets_of_card (2,
X)
by A17, A22, TARSKI:def 2;
hence
x in bool (the_subsets_of_card (2,X))
;
verum
end; A37:
union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } = the_subsets_of_card (2,
X)
proof
thus
union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } c= the_subsets_of_card (2,
X)
XBOOLE_0:def 10 the_subsets_of_card (2,X) c= union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } }proof
let x be
object ;
TARSKI:def 3 ( not x in union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or x in the_subsets_of_card (2,X) )
assume
x in union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } }
;
x in the_subsets_of_card (2,X)
then consider Y being
set such that A38:
x in Y
and A39:
Y in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } }
by TARSKI:def 4;
(
Y = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or
Y = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } )
by A39, TARSKI:def 2;
hence
x in the_subsets_of_card (2,
X)
by A38, A17, A22;
verum
end;
thus
the_subsets_of_card (2,
X)
c= union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } }
verumproof
let x be
object ;
TARSKI:def 3 ( not x in the_subsets_of_card (2,X) or x in union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } )
assume
x in the_subsets_of_card (2,
X)
;
x in union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } }
then consider xx being
Subset of
X such that A40:
x = xx
and A41:
card xx = 2
;
consider a,
b being
object such that A42:
a <> b
and A43:
xx = {a,b}
by A41, CARD_2:60;
(
a in xx &
b in xx )
by A43, TARSKI:def 2;
then
(
a in X &
b in X )
;
then reconsider a =
a,
b =
b as
Element of
R ;
A44:
(
a in xx &
b in xx )
by A43, TARSKI:def 2;
( ( not
a <= b & not
b <= a ) or
a <= b or
b <= a )
;
then
(
{a,b} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or
{a,b} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } )
by A44, A42;
hence
x in union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } }
by A40, A43, A27, TARSKI:def 4;
verum
end;
end;
for
a being
Subset of
(the_subsets_of_card (2,X)) st
a in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } holds
(
a <> {} & ( for
b being
Subset of
(the_subsets_of_card (2,X)) holds
( not
b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or
a = b or
a misses b ) ) )
proof
let a be
Subset of
(the_subsets_of_card (2,X));
( a in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } implies ( a <> {} & ( for b being Subset of (the_subsets_of_card (2,X)) holds
( not b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or a = b or a misses b ) ) ) )
assume A45:
a in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } }
;
( a <> {} & ( for b being Subset of (the_subsets_of_card (2,X)) holds
( not b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or a = b or a misses b ) ) )
thus
a <> {}
for b being Subset of (the_subsets_of_card (2,X)) holds
( not b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or a = b or a misses b )proof
per cases
( a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } )
by A45, TARSKI:def 2;
suppose A46:
a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) }
;
a <> {} consider aa,
bb being
set such that A47:
aa in C
and A48:
bb in C
and A49:
aa <> bb
by A13, A4, NAT_1:59;
reconsider aa =
aa,
bb =
bb as
Element of
R by A47, A48;
A50:
(
aa <= bb or
bb <= aa )
by A47, A48, A49, Th6;
(
aa in (Y \/ An) \/ C &
bb in (Y \/ An) \/ C )
by A47, A48, XBOOLE_0:def 3;
then
{aa,bb} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) }
by A50, A49;
hence
a <> {}
by A46;
verum end; suppose A51:
a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) }
;
a <> {} consider aa,
bb being
set such that A52:
aa in An
and A53:
bb in An
and A54:
aa <> bb
by A13, A5, NAT_1:59;
reconsider aa =
aa,
bb =
bb as
Element of
R by A52, A53;
A55:
( not
aa <= bb & not
bb <= aa )
by A52, A53, A54, Def2;
(
aa in Y \/ An &
bb in Y \/ An )
by A52, A53, XBOOLE_0:def 3;
then
(
aa in X &
bb in X )
by XBOOLE_0:def 3;
then
{aa,bb} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) }
by A55, A54;
hence
a <> {}
by A51;
verum end;
end;
let b be
Subset of
(the_subsets_of_card (2,X));
( not b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or a = b or a misses b )
assume A56:
b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } }
;
( a = b or a misses b )
assume A57:
a <> b
;
a misses b
assume A58:
a meets b
;
contradiction
( (
a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or
a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) & (
b = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or
b = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) )
by A45, A56, TARSKI:def 2;
then
{ {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } /\ { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } <> {}
by A57, A58;
then consider x being
object such that A59:
x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } /\ { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) }
by XBOOLE_0:def 1;
x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) }
by A59, XBOOLE_0:def 4;
then consider xx,
yy being
Element of
R such that A60:
{xx,yy} = x
and
(
xx <> yy &
xx in X &
yy in X )
and A61:
(
xx <= yy or
yy <= xx )
;
x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) }
by A59, XBOOLE_0:def 4;
then consider x2,
y2 being
Element of
R such that A62:
{x2,y2} = x
and
(
x2 <> y2 &
x2 in X &
y2 in X )
and A63:
( not
x2 <= y2 & not
y2 <= x2 )
;
( (
xx = x2 &
yy = y2 ) or (
xx = y2 &
yy = x2 ) )
by A60, A62, ZFMISC_1:6;
hence
contradiction
by A61, A63;
verum
end; then reconsider P =
{ { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } as
a_partition of
the_subsets_of_card (2,
X)
by A37, A36, EQREL_1:def 4;
card P = 2
by A28, CARD_2:57;
then consider S being
Subset of
X such that A64:
card S >= m
and A65:
S is_homogeneous_for P
by A16, A14, A15, XXREAL_0:2;
reconsider S =
S as
finite Subset of
R by XBOOLE_1:1;
max (
(clique# R),
(stability# R))
>= clique# R
by XXREAL_0:25;
then
m > clique# R
by NAT_1:13;
then A66:
card S > clique# R
by A64, XXREAL_0:2;
max (
(clique# R),
(stability# R))
>= stability# R
by XXREAL_0:25;
then
m > stability# R
by NAT_1:13;
then A67:
card S > stability# R
by A64, XXREAL_0:2;
consider p being
Element of
P such that A68:
the_subsets_of_card (2,
S)
c= p
by A65, RAMSEY_1:def 1;
per cases
( p = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or p = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } )
by TARSKI:def 2;
suppose A69:
p = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) }
;
contradictionnow for x, y being Element of R st x in S & y in S & x <> y & not x <= y holds
y <= xlet x,
y be
Element of
R;
( x in S & y in S & x <> y & not x <= y implies y <= x )assume that A70:
x in S
and A71:
y in S
and A72:
x <> y
;
( x <= y or y <= x )
(
{x,y} is
Subset of
S &
card {x,y} = 2 )
by A70, A71, A72, CARD_2:57, ZFMISC_1:32;
then
{x,y} in the_subsets_of_card (2,
S)
;
then
{x,y} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) }
by A69, A68;
then consider xx,
yy being
Element of
R such that A73:
{xx,yy} = {x,y}
and
(
xx <> yy &
xx in X &
yy in X )
and A74:
(
xx <= yy or
yy <= xx )
;
( (
xx = x &
yy = y ) or (
xx = y &
yy = x ) )
by A73, ZFMISC_1:6;
hence
(
x <= y or
y <= x )
by A74;
verum end; then
S is
Clique of
R
by Th6;
hence
contradiction
by A66, Def4;
verum suppose A75:
p = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) }
;
contradiction
S is
stable
proof
let x,
y be
Element of
R;
DILWORTH:def 2 ( x in S & y in S & x <> y implies ( not x <= y & not y <= x ) )
assume that A76:
x in S
and A77:
y in S
and A78:
x <> y
;
( not x <= y & not y <= x )
(
{x,y} is
Subset of
S &
card {x,y} = 2 )
by A76, A77, A78, CARD_2:57, ZFMISC_1:32;
then
{x,y} in the_subsets_of_card (2,
S)
;
then
{x,y} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) }
by A75, A68;
then consider xx,
yy being
Element of
R such that A79:
{xx,yy} = {x,y}
and
(
xx <> yy &
xx in X &
yy in X )
and A80:
( not
xx <= yy & not
yy <= xx )
;
( (
xx = x &
yy = y ) or (
xx = y &
yy = x ) )
by A79, ZFMISC_1:6;
hence
( not
x <= y & not
y <= x )
by A80;
verum
end; hence
contradiction
by A67, Def6;
verum end; end;