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