let R be non empty RelStr ; :: thesis: ( R is quasi_ordered & ( for N being non empty Subset of R holds
( min-classes N is finite & not min-classes N is empty ) ) implies R is Dickson )
assume that
A1:
R is quasi_ordered
and
A2:
for N being non empty Subset of R holds
( min-classes N is finite & not min-classes N is empty )
; :: thesis: R is Dickson
A3:
R is transitive
by A1, Def3;
A4:
R is reflexive
by A1, Def3;
set IR = the InternalRel of R;
set CR = the carrier of R;
set IR' = the InternalRel of (R \~ );
let N be Subset of the carrier of R; :: according to DICKSON:def 10 :: thesis: ex B being set st
( B is_Dickson-basis_of N,R & B is finite )
per cases
( N = {} the carrier of R or not N is empty )
;
suppose
not
N is
empty
;
:: thesis: ex B being set st
( B is_Dickson-basis_of N,R & B is finite )then reconsider N' =
N as non
empty Subset of the
carrier of
R ;
reconsider MCN' =
min-classes N' as non
empty finite Subset-Family of the
carrier of
R by A2;
take B =
{ (choose x) where x is Element of MCN' : verum } ;
:: thesis: ( B is_Dickson-basis_of N,R & B is finite )thus
B is_Dickson-basis_of N,
R
:: thesis: B is finite proof
hence
B c= N
by 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 A8:
a in N
;
:: thesis: ex b being Element of R st
( b in B & b <= a )
defpred S1[
Element of
R]
means $1
<= a;
set NN' =
{ d where d is Element of N' : S1[d] } ;
A9:
{ d where d is Element of N' : S1[d] } is
Subset of
N'
from DOMAIN_1:sch 7();
a <= a
by A4, ORDERS_2:24;
then
a in { d where d is Element of N' : S1[d] }
by A8;
then reconsider NN' =
{ d where d is Element of N' : S1[d] } as non
empty Subset of the
carrier of
R by A9, XBOOLE_1:1;
consider m being
Element of
min-classes NN';
A10:
not
min-classes NN' is
empty
by A2;
then reconsider m' =
m as non
empty set by A1, Th23;
consider c being
Element of
m';
consider y being
Element of
(R \~ ) such that
y is_minimal_wrt NN',the
InternalRel of
(R \~ )
and A11:
m' = (Class (EqRel R),y) /\ NN'
by A10, Def8;
A12:
(
c in Class (EqRel R),
y &
c in NN' )
by A11, XBOOLE_0:def 4;
then reconsider c =
c as
Element of
(R \~ ) ;
reconsider c' =
c as
Element of
R ;
consider d being
Element of
N' such that A13:
(
c = d &
d <= a )
by A12;
A14:
c is_minimal_wrt NN',the
InternalRel of
(R \~ )
by A1, A10, Th20;
now assume
not
c is_minimal_wrt N,the
InternalRel of
(R \~ )
;
:: thesis: contradictionthen consider w being
set such that A15:
w in N
and A16:
w <> c
and A17:
[w,c] in the
InternalRel of
(R \~ )
by A13, WAYBEL_4:def 26;
reconsider w' =
w as
Element of
R by A17, ZFMISC_1:106;
w' <= c'
by A17, ORDERS_2:def 9;
then
w' <= a
by A3, A13, ORDERS_2:26;
then
w' in NN'
by A15;
hence
contradiction
by A14, A16, A17, WAYBEL_4:def 26;
:: thesis: verum end;
then A18:
(Class (EqRel R),c) /\ N in min-classes N
by Def8;
then A19:
not
(Class (EqRel R),c) /\ N is
empty
by A1, Th23;
set t =
choose ((Class (EqRel R),c) /\ N);
choose ((Class (EqRel R),c) /\ N) in N
by A19, XBOOLE_0:def 4;
then reconsider t =
choose ((Class (EqRel R),c) /\ N) as
Element of
R ;
take
t
;
:: thesis: ( t in B & t <= a )
thus
t in B
by A18;
:: thesis: t <= a
t in Class (EqRel R),
c
by A19, XBOOLE_0:def 4;
then
[t,c] in EqRel R
by EQREL_1:27;
then
[t,c] in the
InternalRel of
R /\ (the InternalRel of R ~ )
by A1, Def4;
then
[t,c] in the
InternalRel of
R
by XBOOLE_0:def 4;
then
t <= c'
by ORDERS_2:def 9;
hence
t <= a
by A3, A13, ORDERS_2:26;
:: thesis: verum
end; deffunc H1(
set )
-> Element of $1 =
choose $1;
defpred S1[
set ]
means verum;
{ H1(x) where x is Element of MCN' : S1[x] } is
finite
from PRE_CIRC:sch 1();
hence
B is
finite
;
:: thesis: verum end;