let R be non empty RelStr ; ( R is quasi_ordered implies ( R is Dickson iff for S being non empty RelStr st S is quasi_ordered & the InternalRel of R c= the InternalRel of S & the carrier of R = the carrier of S holds
S \~ is well_founded ) )
assume A1:
R is quasi_ordered
; ( R is Dickson iff for S being non empty RelStr st S is quasi_ordered & the InternalRel of R c= the InternalRel of S & the carrier of R = the carrier of S holds
S \~ is well_founded )
A2:
R is reflexive
by A1;
A3:
R is transitive
by A1;
set IR = the InternalRel of R;
set CR = the carrier of R;
thus
( R is Dickson implies for S being non empty RelStr st S is quasi_ordered & the InternalRel of R c= the InternalRel of S & the carrier of R = the carrier of S holds
S \~ is well_founded )
by Th47; ( ( for S being non empty RelStr st S is quasi_ordered & the InternalRel of R c= the InternalRel of S & the carrier of R = the carrier of S holds
S \~ is well_founded ) implies R is Dickson )
assume A4:
for S being non empty RelStr st S is quasi_ordered & the InternalRel of R c= the InternalRel of S & the carrier of R = the carrier of S holds
S \~ is well_founded
; R is Dickson
now R is Dickson assume
not
R is
Dickson
;
contradictionthen
not for
N being non
empty Subset of
R holds
(
min-classes N is
finite & not
min-classes N is
empty )
by A1, Th31;
then consider f being
sequence of
R such that A5:
for
i,
j being
Nat st
i < j holds
not
f . i <= f . j
by A1, Th30;
defpred S1[
object ,
object ]
means (
[$1,$2] in the
InternalRel of
R or ex
i,
j being
Element of
NAT st
(
i < j &
[$1,(f . j)] in the
InternalRel of
R &
[(f . i),$2] in the
InternalRel of
R ) );
consider QOE being
Relation of the
carrier of
R, the
carrier of
R such that A6:
for
x,
y being
object holds
(
[x,y] in QOE iff (
x in the
carrier of
R &
y in the
carrier of
R &
S1[
x,
y] ) )
from RELSET_1:sch 1();
set S =
RelStr(# the
carrier of
R,
QOE #);
now for x, y being object st [x,y] in the InternalRel of R holds
[x,y] in QOElet x,
y be
object ;
( [x,y] in the InternalRel of R implies [x,y] in QOE )assume A7:
[x,y] in the
InternalRel of
R
;
[x,y] in QOEA8:
x in dom the
InternalRel of
R
by A7, XTUPLE_0:def 12;
y in rng the
InternalRel of
R
by A7, XTUPLE_0:def 13;
hence
[x,y] in QOE
by A6, A7, A8;
verum end; then A9:
the
InternalRel of
R c= the
InternalRel of
RelStr(# the
carrier of
R,
QOE #)
by RELAT_1:def 3;
A10:
the
InternalRel of
R is_reflexive_in the
carrier of
R
by A2;
then
for
x being
object st
x in the
carrier of
R holds
[x,x] in QOE
by A6;
then
QOE is_reflexive_in the
carrier of
R
;
then A11:
RelStr(# the
carrier of
R,
QOE #) is
reflexive
;
A12:
the
InternalRel of
R is_transitive_in the
carrier of
R
by A3;
now for x, y, z being object st x in the carrier of R & y in the carrier of R & z in the carrier of R & [x,y] in QOE & [y,z] in QOE holds
[x,z] in QOElet x,
y,
z be
object ;
( x in the carrier of R & y in the carrier of R & z in the carrier of R & [x,y] in QOE & [y,z] in QOE implies [x,z] in QOE )assume that A13:
x in the
carrier of
R
and A14:
y in the
carrier of
R
and A15:
z in the
carrier of
R
and A16:
[x,y] in QOE
and A17:
[y,z] in QOE
;
[x,z] in QOEnow [x,z] in QOEper cases
( [x,y] in the InternalRel of R or ex i, j being Element of NAT st
( i < j & [x,(f . j)] in the InternalRel of R & [(f . i),y] in the InternalRel of R ) )
by A6, A16;
suppose A18:
[x,y] in the
InternalRel of
R
;
[x,z] in QOEnow [x,z] in QOEper cases
( [y,z] in the InternalRel of R or ex i, j being Element of NAT st
( i < j & [y,(f . j)] in the InternalRel of R & [(f . i),z] in the InternalRel of R ) )
by A6, A17;
suppose
ex
i,
j being
Element of
NAT st
(
i < j &
[y,(f . j)] in the
InternalRel of
R &
[(f . i),z] in the
InternalRel of
R )
;
[x,z] in QOEthen consider i,
j being
Element of
NAT such that A19:
i < j
and A20:
[y,(f . j)] in the
InternalRel of
R
and A21:
[(f . i),z] in the
InternalRel of
R
;
[x,(f . j)] in the
InternalRel of
R
by A12, A13, A14, A18, A20;
hence
[x,z] in QOE
by A6, A13, A15, A19, A21;
verum end; end; end; hence
[x,z] in QOE
;
verum end; suppose
ex
i,
j being
Element of
NAT st
(
i < j &
[x,(f . j)] in the
InternalRel of
R &
[(f . i),y] in the
InternalRel of
R )
;
[x,z] in QOEthen consider i,
j being
Element of
NAT such that A22:
i < j
and A23:
[x,(f . j)] in the
InternalRel of
R
and A24:
[(f . i),y] in the
InternalRel of
R
;
now [x,z] in QOEper cases
( [y,z] in the InternalRel of R or ex a, b being Element of NAT st
( a < b & [y,(f . b)] in the InternalRel of R & [(f . a),z] in the InternalRel of R ) )
by A6, A17;
suppose
ex
a,
b being
Element of
NAT st
(
a < b &
[y,(f . b)] in the
InternalRel of
R &
[(f . a),z] in the
InternalRel of
R )
;
[x,z] in QOEthen consider a,
b being
Element of
NAT such that A25:
a < b
and A26:
[y,(f . b)] in the
InternalRel of
R
and A27:
[(f . a),z] in the
InternalRel of
R
;
[(f . i),(f . b)] in the
InternalRel of
R
by A12, A14, A24, A26;
then
f . i <= f . b
;
then
not
i < b
by A5;
then
a <= i
by A25, XXREAL_0:2;
then
a < j
by A22, XXREAL_0:2;
hence
[x,z] in QOE
by A6, A13, A15, A23, A27;
verum end; end; end; hence
[x,z] in QOE
;
verum end; end; end; hence
[x,z] in QOE
;
verum end; then
QOE is_transitive_in the
carrier of
R
;
then
RelStr(# the
carrier of
R,
QOE #) is
transitive
;
then
RelStr(# the
carrier of
R,
QOE #) is
quasi_ordered
by A11;
then A28:
RelStr(# the
carrier of
R,
QOE #)
\~ is
well_founded
by A4, A9;
reconsider f9 =
f as
sequence of
(RelStr(# the carrier of R,QOE #) \~) ;
now for n being Nat holds
( f9 . (n + 1) <> f9 . n & [(f9 . (n + 1)),(f9 . n)] in the InternalRel of (RelStr(# the carrier of R,QOE #) \~) )let n be
Nat;
( f9 . (n + 1) <> f9 . n & [(f9 . (n + 1)),(f9 . n)] in the InternalRel of (RelStr(# the carrier of R,QOE #) \~) )reconsider n1 =
n as
Element of
NAT by ORDINAL1:def 12;
A29:
n < n + 1
by NAT_1:13;
then
not
f . n1 <= f . (n1 + 1)
by A5;
then A30:
not
[(f . n),(f . (n + 1))] in the
InternalRel of
R
;
hence
f9 . (n + 1) <> f9 . n
by A10;
[(f9 . (n + 1)),(f9 . n)] in the InternalRel of (RelStr(# the carrier of R,QOE #) \~)A31:
[(f9 . (n + 1)),(f9 . (n + 1))] in the
InternalRel of
R
by A10;
A32:
[(f9 . n),(f9 . n)] in the
InternalRel of
R
by A10;
A33:
now not [(f9 . n),(f9 . (n + 1))] in QOEassume
[(f9 . n),(f9 . (n + 1))] in QOE
;
contradictionthen
ex
i,
j being
Element of
NAT st
(
i < j &
[(f9 . n),(f . j)] in the
InternalRel of
R &
[(f . i),(f9 . (n + 1))] in the
InternalRel of
R )
by A6, A30;
then consider l,
k being
Element of
NAT such that A34:
k < l
and A35:
[(f9 . n),(f . l)] in the
InternalRel of
R
and A36:
[(f . k),(f9 . (n + 1))] in the
InternalRel of
R
;
A37:
f . n <= f . l
by A35;
A38:
f . k <= f . (n + 1)
by A36;
A39:
l <= n1
by A5, A37;
A40:
n + 1
<= k
by A5, A38;
l < n + 1
by A39, NAT_1:13;
hence
contradiction
by A34, A40, XXREAL_0:2;
verum end; A41:
[(f9 . (n1 + 1)),(f9 . n1)] in QOE
by A6, A29, A31, A32;
not
[(f9 . (n + 1)),(f9 . n)] in QOE ~
by A33, RELAT_1:def 7;
hence
[(f9 . (n + 1)),(f9 . n)] in the
InternalRel of
(RelStr(# the carrier of R,QOE #) \~)
by A41, XBOOLE_0:def 5;
verum end; then
f9 is
descending
by WELLFND1:def 6;
hence
contradiction
by A28, WELLFND1:14;
verum end;
hence
R is Dickson
; verum