let R be transitive antisymmetric with_finite_stability# RelStr ; ex C being Clique-partition of R st card C = stability# R
per cases
( R is finite or R is infinite )
;
suppose A1:
R is
infinite
;
ex C being Clique-partition of R st card C = stability# Rdefpred S1[
Nat]
means for
P being non
empty transitive antisymmetric with_finite_stability# RelStr st
stability# P = $1 holds
ex
C being
Clique-partition of
P st
card C = stability# P;
A2:
S1[
0 ]
;
A3:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
let P be non
empty transitive antisymmetric with_finite_stability# RelStr ;
( stability# P = k + 1 implies ex C being Clique-partition of P st card C = stability# P )
assume A5:
stability# P = k + 1
;
ex C being Clique-partition of P st card C = stability# P
consider C being non
empty Subset of
P such that A6:
C is
strong-chain
and A7:
for
D being
Subset of
P holds
( not
D is
strong-chain or not
C c< D )
by Th52;
set cP = the
carrier of
P;
per cases
( C = the carrier of P or C <> the carrier of P )
;
suppose
C <> the
carrier of
P
;
ex C being Clique-partition of P st card C = stability# Pthen A10:
C c< the
carrier of
P
;
set cP9 = the
carrier of
P \ C;
A11: the
carrier of
P \ ( the carrier of P \ C) =
the
carrier of
P /\ C
by XBOOLE_1:48
.=
C
by XBOOLE_1:28
;
reconsider cP9 = the
carrier of
P \ C as
Subset of
P ;
cP9 <> {}
by A10, XBOOLE_1:105;
then reconsider P9 =
subrelstr cP9 as non
empty transitive antisymmetric with_finite_stability# RelStr ;
A12:
cP9 = the
carrier of
P9
by YELLOW_0:def 15;
A13:
stability# P9 <= k + 1
by A5, Th44;
A14:
stability# P9 <> k + 1
proof
assume A15:
stability# P9 = k + 1
;
contradiction
consider A being
finite StableSet of
P9 such that A16:
card A = stability# P9
by Def6;
reconsider A9 =
A as non
empty finite StableSet of
P by A16, Th30;
defpred S2[
set ,
set ,
set ]
means for
c being
set holds
( not
c in $2 or not $1
/\ $3
c= c or ex
d being
set st
(
d in $2 &
d <> c & $3
/\ d <> {} ) );
defpred S3[
finite Subset of
P,
set ]
means for
p being
Clique-partition of
(subrelstr $1) st
card p <= stability# P holds
S2[$1,
p,$2];
defpred S4[
object ,
object ]
means ex
S being non
empty finite Subset of
P st
( $2
= S & $1
in S &
S3[
S,
C \/ {$1}] );
A17:
for
x being
object st
x in A holds
ex
y being
object st
S4[
x,
y]
proof
let a be
object ;
( a in A implies ex y being object st S4[a,y] )
assume A18:
a in A
;
ex y being object st S4[a,y]
A c= the
carrier of
P
by A12, XBOOLE_1:1;
then
{a} c= the
carrier of
P
by A18, ZFMISC_1:31;
then reconsider Ca =
C \/ {a} as
Subset of
P by XBOOLE_1:8;
then consider S being non
empty finite Subset of
P such that A22:
S3[
S,
Ca]
;
take
S
;
S4[a,S]
take
S
;
( S = S & a in S & S3[S,C \/ {a}] )
thus
S = S
;
( a in S & S3[S,C \/ {a}] )
hence
a in S
;
S3[S,C \/ {a}]
thus
S3[
S,
C \/ {a}]
by A22;
verum
end;
consider f being
Function such that A38:
dom f = A
and A39:
for
x being
object st
x in A holds
S4[
x,
f . x]
from CLASSES1:sch 1(A17);
A40:
rng f is
finite
by A38, FINSET_1:8;
set SS =
union (rng f);
A41:
for
x being
set st
x in rng f holds
x is
finite
A45:
union (rng f) c= the
carrier of
P
A51:
A9 c= union (rng f)
then reconsider SS =
union (rng f) as non
empty finite Subset of
P by A41, A40, A45, FINSET_1:7;
set SSp =
subrelstr SS;
A54:
SS = the
carrier of
(subrelstr SS)
by YELLOW_0:def 15;
consider p being
Clique-partition of
(subrelstr SS) such that A55:
card p <= stability# P
and A56:
not
S2[
SS,
p,
C]
by A6;
consider c being
set such that A57:
c in p
and A58:
SS /\ C c= c
and A59:
for
d being
set st
d in p &
d <> c holds
C /\ d = {}
by A56;
reconsider c =
c as
Element of
p by A57;
A9 = A9 /\ SS
by A51, XBOOLE_1:28;
then reconsider A =
A9 as non
empty finite StableSet of
(subrelstr SS) by Th31;
A60:
stability# (subrelstr SS) >= card A
by Def6;
card p >= stability# (subrelstr SS)
by Th46;
then
card p >= card A
by A60, XXREAL_0:2;
then consider a being
Element of
A such that A61:
c /\ A = {a}
by Th48, A55, A16, A15, A5, XXREAL_0:1;
a in c /\ A
by A61, TARSKI:def 1;
then A62:
a in c
by XBOOLE_0:def 4;
S4[
a,
f . a]
by A39;
then consider S being non
empty finite Subset of
P such that A63:
f . a = S
and A64:
a in f . a
and A65:
S3[
S,
C \/ {a}]
;
deffunc H1(
set )
-> Element of
bool the
carrier of
P = $1
/\ S;
defpred S5[
set ]
means $1
meets S;
set Sp =
{ H1(e) where e is Element of p : S5[e] } ;
A66:
S c= SS
then reconsider Sp =
{ H1(e) where e is Element of p : S5[e] } as
a_partition of
S by A54, PUA2MSS1:11;
for
x being
set st
x in Sp holds
x is
Clique of
(subrelstr S)
then reconsider Sp =
Sp as
Clique-partition of
(subrelstr S) by Def11, YELLOW_0:def 15;
A69:
Sp = { H1(e) where e is Element of p : S5[e] }
;
A70:
card Sp <= card p
from DILWORTH:sch 1(A69);
set cc =
c /\ S;
c meets S
by A62, A63, A64, XBOOLE_0:3;
then A71:
c /\ S in Sp
;
S /\ (C \/ {a}) c= c /\ S
then consider d being
set such that A75:
d in Sp
and A76:
d <> c /\ S
and A77:
(C \/ {a}) /\ d <> {}
by A71, A70, A55, A65, XXREAL_0:2;
consider dd being
Element of
p such that A78:
d = dd /\ S
and
dd meets S
by A75;
C /\ dd = {}
by A78, A76, A59;
then A79:
C /\ d =
{} /\ S
by A78, XBOOLE_1:16
.=
{}
;
(C /\ d) \/ ({a} /\ d) <> {}
by A77, XBOOLE_1:23;
then consider x being
object such that A80:
x in {a} /\ d
by A79, XBOOLE_0:def 1;
(
x in {a} &
x in d )
by A80, XBOOLE_0:def 4;
then
a in d
by TARSKI:def 1;
then
a in dd
by A78, XBOOLE_0:def 4;
then
c meets dd
by A62, XBOOLE_0:3;
hence
contradiction
by A78, A76, EQREL_1:def 4;
verum
end; then
stability# P9 < k + 1
by A13, XXREAL_0:1;
then A81:
stability# P9 <= k
by NAT_1:13;
consider A being
finite StableSet of
P such that A82:
card A = stability# P
by Def6;
A83:
stability# P9 = k
then consider Cp9 being
Clique-partition of
P9 such that A97:
card Cp9 = stability# P9
by A4;
set Cp =
Cp9 \/ {( the carrier of P \ cP9)};
A98:
Cp9 is
finite
by A97;
cP9 <> the
carrier of
P
by A11, XBOOLE_1:37;
then A99:
cP9 c< the
carrier of
P
;
then reconsider Cp =
Cp9 \/ {( the carrier of P \ cP9)} as
a_partition of the
carrier of
P by A12, Th4;
then reconsider Cp =
Cp as
Clique-partition of
P by Def11;
take
Cp
;
card Cp = stability# P
not the
carrier of
P \ cP9 in Cp9
hence
card Cp = stability# P
by A5, A83, A97, A98, CARD_2:41;
verum end;
end;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A2, A3);
hence
ex
C being
Clique-partition of
R st
card C = stability# R
by A1;
verum end;