let R be non empty Poset; :: thesis: for N being non empty Subset of R st R is Dickson holds
ex B being set st
( B is_Dickson-basis_of N,R & ( for C being set st C is_Dickson-basis_of N,R holds
B c= C ) )
let N be non empty Subset of R; :: thesis: ( R is Dickson implies ex B being set st
( B is_Dickson-basis_of N,R & ( for C being set st C is_Dickson-basis_of N,R holds
B c= C ) ) )
assume A1:
R is Dickson
; :: thesis: ex B being set st
( B is_Dickson-basis_of N,R & ( for C being set st C is_Dickson-basis_of N,R holds
B c= C ) )
set IR = the InternalRel of R;
set CR = the carrier of R;
set IR' = the InternalRel of (R \~ );
set B = { b where b is Element of (R \~ ) : b is_minimal_wrt N,the InternalRel of (R \~ ) } ;
A2:
R is quasi_ordered
by Def3;
then
for f being sequence of R ex i, j being Element of NAT st
( i < j & f . i <= f . j )
by A1, Th30;
then
( min-classes N is finite & not min-classes N is empty )
by A2, Th32;
then consider x being set such that
A3:
x in min-classes N
by XBOOLE_0:def 1;
consider y being Element of (R \~ ) such that
A4:
( y is_minimal_wrt N,the InternalRel of (R \~ ) & x = (Class (EqRel R),y) /\ N )
by A3, Def8;
y in { b where b is Element of (R \~ ) : b is_minimal_wrt N,the InternalRel of (R \~ ) }
by A4;
then reconsider B = { b where b is Element of (R \~ ) : b is_minimal_wrt N,the InternalRel of (R \~ ) } as non empty set ;
take
B
; :: thesis: ( B is_Dickson-basis_of N,R & ( for C being set st C is_Dickson-basis_of N,R holds
B c= C ) )
then A9:
B c= N
by TARSKI:def 3;
thus
B is_Dickson-basis_of N,R
:: thesis: for C being set st C is_Dickson-basis_of N,R holds
B c= Cproof
thus
B c= N
by A5, TARSKI:def 3;
:: according to DICKSON:def 9 :: thesis: for a being Element of R st a in N holds
ex b being Element of R st
( b in B & b <= a )
let a be
Element of
R;
:: thesis: ( a in N implies ex b being Element of R st
( b in B & b <= a ) )
assume A10:
a in N
;
:: thesis: ex b being Element of R st
( b in B & b <= a )
reconsider a' =
a as
Element of
(R \~ ) ;
now assume A11:
for
b being
Element of
R holds
( not
b in B or not
b <= a )
;
:: thesis: contradictionper cases
( (the InternalRel of (R \~ ) -Seg a) /\ N = {} or (the InternalRel of (R \~ ) -Seg a) /\ N <> {} )
;
suppose A12:
(the InternalRel of (R \~ ) -Seg a) /\ N <> {}
;
:: thesis: contradiction
R \~ is
well_founded
by A1, A2, Th34;
then
the
InternalRel of
(R \~ ) is_well_founded_in the
carrier of
R
by WELLFND1:def 2;
then consider z being
set such that A13:
z in (the InternalRel of (R \~ ) -Seg a) /\ N
and A14:
the
InternalRel of
(R \~ ) -Seg z misses (the InternalRel of (R \~ ) -Seg a) /\ N
by A12, WELLORD1:def 3;
A15:
z in the
InternalRel of
(R \~ ) -Seg a
by A13, XBOOLE_0:def 4;
then
[z,a] in the
InternalRel of
(R \~ )
by WELLORD1:def 1;
then
z in dom the
InternalRel of
(R \~ )
by RELAT_1:def 4;
then reconsider z =
z as
Element of
(R \~ ) ;
reconsider z' =
z as
Element of
R ;
z is_minimal_wrt (the InternalRel of (R \~ ) -Seg a') /\ N,the
InternalRel of
(R \~ )
by A13, A14, Th7;
then
z is_minimal_wrt N,the
InternalRel of
(R \~ )
by Th8;
then A16:
z in B
;
[z,a] in the
InternalRel of
R \ (the InternalRel of R ~ )
by A15, WELLORD1:def 1;
then
z' <= a
by ORDERS_2:def 9;
hence
contradiction
by A11, A16;
:: thesis: verum end; end;
hence
ex
b being
Element of
R st
(
b in B &
b <= a )
;
:: thesis: verum
end;
let C be set ; :: thesis: ( C is_Dickson-basis_of N,R implies B c= C )
assume A17:
C is_Dickson-basis_of N,R
; :: thesis: B c= C
A18:
C c= N
by A17, Def9;
now let b be
set ;
:: thesis: ( b in B implies b in C )assume A19:
b in B
;
:: thesis: b in C
b in N
by A5, A19;
then reconsider b' =
b as
Element of
R ;
consider c being
Element of
R such that A20:
(
c in C &
c <= b' )
by A9, A17, A19, Def9;
consider b'' being
Element of
(R \~ ) such that A21:
(
b'' = b &
b'' is_minimal_wrt N,the
InternalRel of
(R \~ ) )
by A19;
A22:
[c,b] in the
InternalRel of
R
by A20, ORDERS_2:def 9;
A23:
the
InternalRel of
R is_antisymmetric_in the
carrier of
R
by ORDERS_2:def 6;
[b,c] in the
InternalRel of
R
by A18, A20, A21, A22, Th18;
hence
b in C
by A20, A22, A23, RELAT_2:def 4;
:: thesis: verum end;
hence
B c= C
by TARSKI:def 3; :: thesis: verum