let R be non empty transitive antisymmetric with_finite_stability# RelStr ; ex S being non empty Subset of R st
( S is strong-chain & ( for D being Subset of R holds
( not D is strong-chain or not S c< D ) ) )
set E = { C where C is Subset of R : C is strong-chain } ;
set x = the Element of R;
A1:
{ the Element of R} in { C where C is Subset of R : C is strong-chain }
;
now for Z being set st Z c= { C where C is Subset of R : C is strong-chain } & Z is c=-linear holds
ex Y being set st
( Y in { C where C is Subset of R : C is strong-chain } & ( for X1 being set st X1 in Z holds
X1 c= Y ) )let Z be
set ;
( Z c= { C where C is Subset of R : C is strong-chain } & Z is c=-linear implies ex Y being set st
( Y in { C where C is Subset of R : C is strong-chain } & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )assume that A2:
Z c= { C where C is Subset of R : C is strong-chain }
and A3:
Z is
c=-linear
;
ex Y being set st
( Y in { C where C is Subset of R : C is strong-chain } & ( for X1 being set st X1 in Z holds
X1 c= Y ) )set Y =
union Z;
take Y =
union Z;
( Y in { C where C is Subset of R : C is strong-chain } & ( for X1 being set st X1 in Z holds
X1 c= Y ) )then reconsider Y9 =
Y as
Subset of
R by ZFMISC_1:76;
Y9 is
strong-chain
proof
let S be non
empty finite Subset of
R;
DILWORTH:def 13 ex P being Clique-partition of (subrelstr S) st
( card P <= stability# R & ex c being set st
( c in P & S /\ Y9 c= c & ( for d being set st d in P & d <> c holds
Y9 /\ d = {} ) ) )
set F =
S /\ Y;
per cases
( S /\ Y is empty or not S /\ Y is empty )
;
suppose A7:
not
S /\ Y is
empty
;
ex P being Clique-partition of (subrelstr S) st
( card P <= stability# R & ex c being set st
( c in P & S /\ Y9 c= c & ( for d being set st d in P & d <> c holds
Y9 /\ d = {} ) ) )then A8:
not
Z is
empty
by ZFMISC_1:2;
defpred S1[
object ,
object ]
means ex
D2 being
set st
(
D2 = $2 & $1
in S /\ Y & $2
in Z & $1
in D2 );
A9:
for
x being
object st
x in S /\ Y holds
ex
y being
object st
(
y in Z &
S1[
x,
y] )
consider f being
Function of
(S /\ Y),
Z such that A13:
for
x being
object st
x in S /\ Y holds
S1[
x,
f . x]
from FUNCT_2:sch 1(A9);
set rf =
rng f;
(
rng f c= Z &
Z is
c=-linear implies
rng f is
c=-linear )
;
then consider m being
set such that A14:
m in rng f
and A15:
for
C being
set st
C in rng f holds
C c= m
by A3, A7, A8, FINSET_1:12, RELAT_1:def 19;
rng f c= Z
by RELAT_1:def 19;
then
m in Z
by A14;
then
m in { C where C is Subset of R : C is strong-chain }
by A2;
then consider C being
Subset of
R such that A16:
m = C
and A17:
C is
strong-chain
;
A18:
S /\ Y c= C
consider p being
Clique-partition of
(subrelstr S) such that A21:
card p <= stability# R
and A22:
ex
c being
set st
(
c in p &
S /\ C c= c & ( for
d being
set st
d in p &
d <> c holds
C /\ d = {} ) )
by A17;
take
p
;
( card p <= stability# R & ex c being set st
( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds
Y9 /\ d = {} ) ) )thus
card p <= stability# R
by A21;
ex c being set st
( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds
Y9 /\ d = {} ) )consider c being
set such that A23:
c in p
and A24:
S /\ C c= c
and A25:
for
d being
set st
d in p &
d <> c holds
C /\ d = {}
by A22;
take
c
;
( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds
Y9 /\ d = {} ) )thus
c in p
by A23;
( S /\ Y9 c= c & ( for d being set st d in p & d <> c holds
Y9 /\ d = {} ) )thus
S /\ Y9 c= c
for d being set st d in p & d <> c holds
Y9 /\ d = {} let d be
set ;
( d in p & d <> c implies Y9 /\ d = {} )assume that A26:
d in p
and A27:
d <> c
;
Y9 /\ d = {} assume
Y9 /\ d <> {}
;
contradictionthen consider x being
object such that A28:
x in Y9 /\ d
by XBOOLE_0:def 1;
A29:
x in Y9
by A28, XBOOLE_0:def 4;
A30:
x in d
by A28, XBOOLE_0:def 4;
d is
Subset of
S
by A26, YELLOW_0:def 15;
then
x in S /\ Y
by A30, A29, XBOOLE_0:def 4;
then
x in C /\ d
by A30, A18, XBOOLE_0:def 4;
hence
contradiction
by A26, A27, A25;
verum end; end;
end; hence
Y in { C where C is Subset of R : C is strong-chain }
;
for X1 being set st X1 in Z holds
X1 c= Ylet X1 be
set ;
( X1 in Z implies X1 c= Y )assume A31:
X1 in Z
;
X1 c= Ythus
X1 c= Y
by A31, ZFMISC_1:74;
verum end;
then consider Y being set such that
A32:
Y in { C where C is Subset of R : C is strong-chain }
and
A33:
for Z being set st Z in { C where C is Subset of R : C is strong-chain } & Z <> Y holds
not Y c= Z
by A1, ORDERS_1:65;
consider C being Subset of R such that
A34:
Y = C
and
A35:
C is strong-chain
by A32;
reconsider S = C as non empty Subset of R by A34, A1, A33, XBOOLE_1:2;
take
S
; ( S is strong-chain & ( for D being Subset of R holds
( not D is strong-chain or not S c< D ) ) )
thus
S is strong-chain
by A35; for D being Subset of R holds
( not D is strong-chain or not S c< D )
let D be Subset of R; ( not D is strong-chain or not S c< D )
assume that
A36:
D is strong-chain
and
A37:
S c< D
; contradiction
A38:
D in { C where C is Subset of R : C is strong-chain }
by A36;
( D <> S & S c= D )
by A37;
hence
contradiction
by A34, A38, A33; verum