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 not R is finite )
;
suppose S0:
not
R is
finite
;
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;
P1:
S1[
0 ]
;
P2:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A:
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 B:
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 C:
C is
strong-chain
and D:
for
D being
Subset of
P holds
( not
D is
strong-chain or not
C c< D )
by Maxsc;
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 S1a:
C c< the
carrier of
P
by XBOOLE_0:def 8;
set cP9 = the
carrier of
P \ C;
E: 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 ;
set P9 =
subrelstr cP9;
cP9 <> {}
by S1a, XBOOLE_1:105;
then reconsider P9 =
subrelstr cP9 as non
empty transitive antisymmetric with_finite_stability# RelStr ;
cP9c:
cP9 = the
carrier of
P9
by YELLOW_0:def 15;
G:
stability# P9 <= k + 1
by B, Wsubp0;
H:
stability# P9 <> k + 1
proof
assume AA:
stability# P9 = k + 1
;
contradiction
consider A being
finite StableSet of
P9 such that A1:
card A = stability# P9
by Lwidth;
reconsider A9 =
A as non
empty finite StableSet of
P by A1, SPAChain1;
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[
set ,
set ]
means ex
S being non
empty finite Subset of
P st
( $2
= S & $1
in $2 &
S3[
S,
C \/ {$1}] );
P:
for
x being
set st
x in A holds
ex
y being
set st
S4[
x,
y]
proof
let a be
set ;
( a in A implies ex y being set st S4[a,y] )
assume A2:
a in A
;
ex y being set st S4[a,y]
A c= the
carrier of
P
by cP9c, XBOOLE_1:1;
then
{a} c= the
carrier of
P
by A2, ZFMISC_1:37;
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 B2:
S3[
S,
Ca]
by Lsc;
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 B2;
verum
end;
consider f being
Function such that C1:
dom f = A
and E1:
for
x being
set st
x in A holds
S4[
x,
f . x]
from CLASSES1:sch 1(P);
D1a:
rng f is
finite
by C1, FINSET_1:26;
set SS =
union (rng f);
C1bb:
for
x being
set st
x in rng f holds
x is
finite
C1c:
union (rng f) c= the
carrier of
P
C1a:
A9 c= union (rng f)
then reconsider SS =
union (rng f) as non
empty finite Subset of
P by C1bb, D1a, FINSET_1:25, C1c;
set SSp =
subrelstr SS;
cSS:
SS = the
carrier of
(subrelstr SS)
by YELLOW_0:def 15;
consider p being
Clique-partition of
(subrelstr SS) such that F1:
card p <= stability# P
and G1:
not
S2[
SS,
p,
C]
by C, Lsc;
consider c being
set such that H1:
c in p
and I1:
SS /\ C c= c
and J1:
for
d being
set st
d in p &
d <> c holds
C /\ d = {}
by G1;
reconsider c =
c as
Element of
p by H1;
A9 = A9 /\ SS
by C1a, XBOOLE_1:28;
then reconsider A =
A9 as non
empty finite StableSet of
(subrelstr SS) by SPAChain;
K1:
stability# (subrelstr SS) >= card A
by Lwidth;
card p >= stability# (subrelstr SS)
by Chpw;
then
card p >= card A
by K1, XXREAL_0:2;
then consider a being
Element of
A such that L1:
c /\ A = {a}
by ACpart2, F1, A1, AA, B, XXREAL_0:1;
a in c /\ A
by L1, TARSKI:def 1;
then M1:
a in c
by XBOOLE_0:def 4;
consider S being non
empty finite Subset of
P such that N1:
f . a = S
and O1:
a in f . a
and P1:
S3[
S,
C \/ {a}]
by E1;
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] } ;
R1:
S c= SS
then reconsider Sp =
{ H1(e) where e is Element of p : S5[e] } as
a_partition of
S by cSS, 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 YELLOW_0:def 15, LCpart;
T1a:
Sp = { H1(e) where e is Element of p : S5[e] }
;
T1b:
card Sp <= card p
from DILWORTH:sch 1(T1a);
set cc =
c /\ S;
c meets S
by M1, N1, O1, XBOOLE_0:3;
then U1:
c /\ S in Sp
;
S /\ (C \/ {a}) c= c /\ S
then consider d being
set such that V1:
d in Sp
and W1:
d <> c /\ S
and X1:
(C \/ {a}) /\ d <> {}
by U1, T1b, F1, XXREAL_0:2, P1;
consider dd being
Element of
p such that Y1:
d = dd /\ S
and
dd meets S
by V1;
C /\ dd = {}
by Y1, W1, J1;
then Z1a:
C /\ d =
{} /\ S
by Y1, XBOOLE_1:16
.=
{}
;
(C /\ d) \/ ({a} /\ d) <> {}
by X1, XBOOLE_1:23;
then consider x being
set such that Y1a:
x in {a} /\ d
by Z1a, XBOOLE_0:def 1;
(
x in {a} &
x in d )
by Y1a, XBOOLE_0:def 4;
then
a in d
by TARSKI:def 1;
then
a in dd
by Y1, XBOOLE_0:def 4;
then
c meets dd
by M1, XBOOLE_0:3;
hence
contradiction
by Y1, W1, EQREL_1:def 6;
verum
end; then
stability# P9 < k + 1
by G, XXREAL_0:1;
then Ha:
stability# P9 <= k
by NAT_1:13;
consider A being
finite StableSet of
P such that I:
card A = stability# P
by Lwidth;
Y:
stability# P9 = k
proof
per cases
( A /\ C = {} or A /\ C <> {} )
;
suppose
A /\ C <> {}
;
stability# P9 = kthen consider x being
set such that A3:
x in A /\ C
by XBOOLE_0:def 1;
B3:
x in A
by A3, XBOOLE_0:def 4;
C3:
x in C
by A3, XBOOLE_0:def 4;
set A9 =
A \ {x};
{x} c= A
by B3, ZFMISC_1:37;
then D3:
A = (A \ {x}) \/ {x}
by XBOOLE_1:45;
x in {x}
by TARSKI:def 1;
then
not
x in A \ {x}
by XBOOLE_0:def 5;
then D4a:
card A = (card (A \ {x})) + 1
by D3, CARD_2:54;
E4:
A \ {x} c= A
by XBOOLE_1:36;
A \ {x} c= cP9
then F4:
A \ {x} c= A /\ cP9
by E4, XBOOLE_1:19;
A /\ cP9 c= A \ {x}
then
A \ {x} = A /\ cP9
by F4, XBOOLE_0:def 10;
then reconsider A9 =
A \ {x} as
StableSet of
P9 by SPAChain;
stability# P9 >= card A9
by Lwidth;
hence
stability# P9 = k
by D4a, I, B, Ha, XXREAL_0:1;
verum end;
end; then consider Cp9 being
Clique-partition of
P9 such that Z:
card Cp9 = stability# P9
by A;
set Cp =
Cp9 \/ {(the carrier of P \ cP9)};
Zk:
Cp9 is
finite
by Z;
cP9 <> the
carrier of
P
by E, XBOOLE_1:37;
then Zl:
cP9 c< the
carrier of
P
by XBOOLE_0:def 8;
then reconsider Cp =
Cp9 \/ {(the carrier of P \ cP9)} as
a_partition of the
carrier of
P by cP9c, SPpart;
then reconsider Cp =
Cp as
Clique-partition of
P by LCpart;
take
Cp
;
card Cp = stability# P
not the
carrier of
P \ cP9 in Cp9
hence
card Cp = stability# P
by B, Y, Z, Zk, CARD_2:54;
verum end;
end;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(P1, P2);
hence
ex
C being
Clique-partition of
R st
card C = stability# R
by S0;
verum end;