let R be non empty RelStr ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: ( ( 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 ; :: thesis: R is Dickson
now :: thesis: R is Dickson
assume not R is Dickson ; :: thesis: contradiction
then 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 :: thesis: for x, y being object st [x,y] in the InternalRel of R holds
[x,y] in QOE
let x, y be object ; :: thesis: ( [x,y] in the InternalRel of R implies [x,y] in QOE )
assume A7: [x,y] in the InternalRel of R ; :: thesis: [x,y] in QOE
A8: 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; :: thesis: 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 :: thesis: 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 QOE
let x, y, z be object ; :: thesis: ( 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 ; :: thesis: [x,z] in QOE
now :: thesis: [x,z] in QOE
per 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 ; :: thesis: [x,z] in QOE
now :: thesis: [x,z] in QOE
per 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 [y,z] in the InternalRel of R ; :: thesis: [x,z] in QOE
then [x,z] in the InternalRel of R by A12, A13, A14, A15, A18;
hence [x,z] in QOE by A6, A13, A15; :: thesis: verum
end;
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 ) ; :: thesis: [x,z] in QOE
then 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; :: thesis: verum
end;
end;
end;
hence [x,z] in QOE ; :: thesis: 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 ) ; :: thesis: [x,z] in QOE
then 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 :: thesis: [x,z] in QOE
per 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 [y,z] in the InternalRel of R ; :: thesis: [x,z] in QOE
then [(f . i),z] in the InternalRel of R by A12, A14, A15, A24;
hence [x,z] in QOE by A6, A13, A15, A22, A23; :: thesis: verum
end;
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 ) ; :: thesis: [x,z] in QOE
then 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; :: thesis: verum
end;
end;
end;
hence [x,z] in QOE ; :: thesis: verum
end;
end;
end;
hence [x,z] in QOE ; :: thesis: 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 :: thesis: 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; :: thesis: ( 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; :: thesis: [(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 :: thesis: not [(f9 . n),(f9 . (n + 1))] in QOE
assume [(f9 . n),(f9 . (n + 1))] in QOE ; :: thesis: contradiction
then 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; :: thesis: 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; :: thesis: verum
end;
then f9 is descending by WELLFND1:def 6;
hence contradiction by A28, WELLFND1:14; :: thesis: verum
end;
hence R is Dickson ; :: thesis: verum