let R be non empty RelStr ; :: thesis: for s being sequence of R st R is Dickson holds
ex t being sequence of R st
( t is subsequence of s & t is weakly-ascending )
let s be sequence of R; :: thesis: ( R is Dickson implies ex t being sequence of R st
( t is subsequence of s & t is weakly-ascending ) )
assume A1: R is Dickson ; :: thesis: ex t being sequence of R st
( t is subsequence of s & t is weakly-ascending )
set CR = the carrier of R;
deffunc H1( Element of rng s, Element of NAT ) -> set = { n where n is Element of NAT : ( $1 <= s . n & $2 < n ) } ;
deffunc H2( Element of rng s) -> set = { n where n is Element of NAT : $1 <= s . n } ;
defpred S1[ set , Element of NAT , set ] means ex N being Subset of the carrier of R ex B being non empty Subset of the carrier of R st
( N = { (s . w) where w is Element of NAT : ( s . $2 <= s . w & $2 < w ) } & not { w where w is Element of NAT : ( s . $2 <= s . w & $2 < w ) } is finite & B = choose { BB where BB is Element of Dickson-bases N,R : BB is finite } & $3 = s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,$2) is finite ) } ),$2 );
defpred S2[ set , Element of NAT , set ] means ( not { w where w is Element of NAT : ( s . $2 <= s . w & $2 < w ) } is finite implies S1[$1,$2,$3] );
A2: for n, x being Element of NAT ex y being Element of NAT st S2[n,x,y]
proof
let n, x be Element of NAT ; :: thesis: ex y being Element of NAT st S2[n,x,y]
set N = { (s . w) where w is Element of NAT : ( s . x <= s . w & x < w ) } ;
now
let y be set ; :: thesis: ( y in { (s . w) where w is Element of NAT : ( s . x <= s . w & x < w ) } implies y in the carrier of R )
assume y in { (s . w) where w is Element of NAT : ( s . x <= s . w & x < w ) } ; :: thesis: y in the carrier of R
then ex w being Element of NAT st
( y = s . w & s . x <= s . w & x < w ) ;
hence y in the carrier of R ; :: thesis: verum
end;
then reconsider N = { (s . w) where w is Element of NAT : ( s . x <= s . w & x < w ) } as Subset of the carrier of R by TARSKI:def 3;
set W = { w where w is Element of NAT : ( s . x <= s . w & x < w ) } ;
per cases ( N is empty or not N is empty ) ;
suppose A3: N is empty ; :: thesis: ex y being Element of NAT st S2[n,x,y]
take 1 ; :: thesis: S2[n,x,1]
assume not { w where w is Element of NAT : ( s . x <= s . w & x < w ) } is finite ; :: thesis: S1[n,x,1]
then consider ww being set such that
A4: ww in { w where w is Element of NAT : ( s . x <= s . w & x < w ) } by XBOOLE_0:def 1;
consider www being Element of NAT such that
www = ww and
A5: s . x <= s . www and
A6: x < www by A4;
s . www in N by A5, A6;
hence S1[n,x,1] by A3; :: thesis: verum
end;
suppose A7: not N is empty ; :: thesis: ex y being Element of NAT st S2[n,x,y]
set BBX = { BB where BB is Element of Dickson-bases N,R : BB is finite } ;
set B = choose { BB where BB is Element of Dickson-bases N,R : BB is finite } ;
consider BD1 being set such that
A8: BD1 is_Dickson-basis_of N,R and
A9: BD1 is finite by A1, Def10;
BD1 in Dickson-bases N,R by A1, A8, Def13;
then BD1 in { BB where BB is Element of Dickson-bases N,R : BB is finite } by A9;
then choose { BB where BB is Element of Dickson-bases N,R : BB is finite } in { BB where BB is Element of Dickson-bases N,R : BB is finite } ;
then ex BBB being Element of Dickson-bases N,R st
( choose { BB where BB is Element of Dickson-bases N,R : BB is finite } = BBB & BBB is finite ) ;
then A10: choose { BB where BB is Element of Dickson-bases N,R : BB is finite } is_Dickson-basis_of N,R by A1, Def13;
then choose { BB where BB is Element of Dickson-bases N,R : BB is finite } c= N by Def9;
then reconsider B = choose { BB where BB is Element of Dickson-bases N,R : BB is finite } as non empty Subset of the carrier of R by A7, A10, Th27, XBOOLE_1:1;
set y = s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,x) is finite ) } ),x;
take s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,x) is finite ) } ),x ; :: thesis: S2[n,x,s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,x) is finite ) } ),x]
set W = { w where w is Element of NAT : ( s . x <= s . w & x < w ) } ;
assume A11: not { w where w is Element of NAT : ( s . x <= s . w & x < w ) } is finite ; :: thesis: S1[n,x,s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,x) is finite ) } ),x]
take N ; :: thesis: ex B being non empty Subset of the carrier of R st
( N = { (s . w) where w is Element of NAT : ( s . x <= s . w & x < w ) } & not { w where w is Element of NAT : ( s . x <= s . w & x < w ) } is finite & B = choose { BB where BB is Element of Dickson-bases N,R : BB is finite } & s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,x) is finite ) } ),x = s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,x) is finite ) } ),x )
reconsider B = B as non empty Subset of the carrier of R ;
take B ; :: thesis: ( N = { (s . w) where w is Element of NAT : ( s . x <= s . w & x < w ) } & not { w where w is Element of NAT : ( s . x <= s . w & x < w ) } is finite & B = choose { BB where BB is Element of Dickson-bases N,R : BB is finite } & s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,x) is finite ) } ),x = s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,x) is finite ) } ),x )
thus N = { (s . w) where w is Element of NAT : ( s . x <= s . w & x < w ) } ; :: thesis: ( not { w where w is Element of NAT : ( s . x <= s . w & x < w ) } is finite & B = choose { BB where BB is Element of Dickson-bases N,R : BB is finite } & s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,x) is finite ) } ),x = s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,x) is finite ) } ),x )
thus not { w where w is Element of NAT : ( s . x <= s . w & x < w ) } is finite by A11; :: thesis: ( B = choose { BB where BB is Element of Dickson-bases N,R : BB is finite } & s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,x) is finite ) } ),x = s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,x) is finite ) } ),x )
thus B = choose { BB where BB is Element of Dickson-bases N,R : BB is finite } ; :: thesis: s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,x) is finite ) } ),x = s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,x) is finite ) } ),x
thus s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,x) is finite ) } ),x = s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,x) is finite ) } ),x ; :: thesis: verum
end;
end;
end;
consider B being set such that
A12: B is_Dickson-basis_of rng s,R and
A13: B is finite by A1, Def10;
reconsider B = B as non empty set by A12, Th27;
set BALL = { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H2(b9) is finite ) } ;
set b1 = choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H2(b9) is finite ) } ;
consider f being Function of NAT ,NAT such that
A14: f . 0 = s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H2(b9) is finite ) } ) and
A15: for n being Element of NAT holds S2[n,f . n,f . (n + 1)] from RECDEF_1:sch 2(A2);
 A16: dom f = NAT by FUNCT_2:def 1;
A17: rng f c= NAT ;
now
A18: B is finite by A13;
assume A19: for b being Element of rng s st b in B holds
H2(b) is finite ; :: thesis: contradiction
set Ball = { H2(b) where b is Element of rng s : b in B } ;
A20: { H2(b) where b is Element of rng s : b in B } is finite from FRAENKEL:sch 21(A18);
now
let X be set ; :: thesis: ( X in { H2(b) where b is Element of rng s : b in B } implies X is finite )
assume X in { H2(b) where b is Element of rng s : b in B } ; :: thesis: X is finite
then ex b being Element of rng s st
( X = H2(b) & b in B ) ;
hence X is finite by A19; :: thesis: verum
end;
then A21: union { H2(b) where b is Element of rng s : b in B } is finite by A20, FINSET_1:25;
now
let x be set ; :: thesis: ( x in NAT implies x in union { H2(b) where b is Element of rng s : b in B } )
assume x in NAT ; :: thesis: x in union { H2(b) where b is Element of rng s : b in B }
then reconsider x9 = x as Element of NAT ;
dom s = NAT by FUNCT_2:def 1;
then x9 in dom s ;
then A22: s . x in rng s by FUNCT_1:12;
then reconsider sx = s . x as Element of R ;
consider b being Element of R such that
A23: b in B and
A24: b <= sx by A12, A22, Def9;
B c= rng s by A12, Def9;
then reconsider b = b as Element of rng s by A23;
A25: x9 in H2(b) by A24;
H2(b) in { H2(b) where b is Element of rng s : b in B } by A23;
hence x in union { H2(b) where b is Element of rng s : b in B } by A25, TARSKI:def 4; :: thesis: verum
end;
then NAT c= union { H2(b) where b is Element of rng s : b in B } by TARSKI:def 3;
hence contradiction by A21; :: thesis: verum
end;
then consider tb being Element of rng s such that
A26: tb in B and
A27: not H2(tb) is finite ;
A28: tb in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H2(b9) is finite ) } by A26, A27;
then choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H2(b9) is finite ) } in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H2(b9) is finite ) } ;
then A29: ex bt being Element of B st
( choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H2(b9) is finite ) } = bt & ex b9 being Element of rng s st
( b9 = bt & not H2(b9) is finite ) ) ;
dom s = NAT by NORMSP_1:17;
then A30: s . (f . 0 ) = choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H2(b9) is finite ) } by A14, A29, Def11;
choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H2(b9) is finite ) } in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H2(b9) is finite ) } by A28;
then A31: ex eb being Element of B st
( choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H2(b9) is finite ) } = eb & ex eb9 being Element of rng s st
( eb9 = eb & not H2(eb9) is finite ) ) ;
deffunc H3( set ) -> set = $1;
defpred S3[ Element of NAT ] means s . (f . 0 ) <= s . $1;
set W1 = { w where w is Element of NAT : s . (f . 0 ) <= s . w } ;
set W2 = { w where w is Element of NAT : ( s . (f . 0 ) <= s . w & f . 0 < w ) } ;
set W3 = { H3(w) where w is Element of NAT : ( 0 <= w & w <= f . 0 & S3[w] ) } ;
A32: { H3(w) where w is Element of NAT : ( 0 <= w & w <= f . 0 & S3[w] ) } is finite from FINSEQ_1:sch 6();
now
let x be set ; :: thesis: ( ( x in { w where w is Element of NAT : s . (f . 0 ) <= s . w } implies x in { w where w is Element of NAT : ( s . (f . 0 ) <= s . w & f . 0 < w ) } \/ { H3(w) where w is Element of NAT : ( 0 <= w & w <= f . 0 & S3[w] ) } ) & ( x in { w where w is Element of NAT : ( s . (f . 0 ) <= s . w & f . 0 < w ) } \/ { H3(w) where w is Element of NAT : ( 0 <= w & w <= f . 0 & S3[w] ) } implies b1 in { b2 where w is Element of NAT : s . (f . 0 ) <= s . b2 } ) )
hereby :: thesis: ( x in { w where w is Element of NAT : ( s . (f . 0 ) <= s . w & f . 0 < w ) } \/ { H3(w) where w is Element of NAT : ( 0 <= w & w <= f . 0 & S3[w] ) } implies b1 in { b2 where w is Element of NAT : s . (f . 0 ) <= s . b2 } )
assume x in { w where w is Element of NAT : s . (f . 0 ) <= s . w } ; :: thesis: x in { w where w is Element of NAT : ( s . (f . 0 ) <= s . w & f . 0 < w ) } \/ { H3(w) where w is Element of NAT : ( 0 <= w & w <= f . 0 & S3[w] ) }
then consider w being Element of NAT such that
A33: x = w and
A34: s . (f . 0 ) <= s . w ;
A35: 0 <= w by NAT_1:2;
( w <= f . 0 or w > f . 0 ) ;
then ( x in { w where w is Element of NAT : ( s . (f . 0 ) <= s . w & f . 0 < w ) } or x in { H3(w) where w is Element of NAT : ( 0 <= w & w <= f . 0 & S3[w] ) } ) by A33, A34, A35;
hence x in { w where w is Element of NAT : ( s . (f . 0 ) <= s . w & f . 0 < w ) } \/ { H3(w) where w is Element of NAT : ( 0 <= w & w <= f . 0 & S3[w] ) } by XBOOLE_0:def 3; :: thesis: verum
end;
assume A36: x in { w where w is Element of NAT : ( s . (f . 0 ) <= s . w & f . 0 < w ) } \/ { H3(w) where w is Element of NAT : ( 0 <= w & w <= f . 0 & S3[w] ) } ; :: thesis: b1 in { b2 where w is Element of NAT : s . (f . 0 ) <= s . b2 }
per cases ( x in { w where w is Element of NAT : ( s . (f . 0 ) <= s . w & f . 0 < w ) } or x in { H3(w) where w is Element of NAT : ( 0 <= w & w <= f . 0 & S3[w] ) } ) by A36, XBOOLE_0:def 3;
suppose x in { w where w is Element of NAT : ( s . (f . 0 ) <= s . w & f . 0 < w ) } ; :: thesis: b1 in { b2 where w is Element of NAT : s . (f . 0 ) <= s . b2 }
then ex w being Element of NAT st
( x = w & s . (f . 0 ) <= s . w & f . 0 < w ) ;
hence x in { w where w is Element of NAT : s . (f . 0 ) <= s . w } ; :: thesis: verum
end;
suppose x in { H3(w) where w is Element of NAT : ( 0 <= w & w <= f . 0 & S3[w] ) } ; :: thesis: b1 in { b2 where w is Element of NAT : s . (f . 0 ) <= s . b2 }
then ex w being Element of NAT st
( x = w & 0 <= w & w <= f . 0 & s . (f . 0 ) <= s . w ) ;
hence x in { w where w is Element of NAT : s . (f . 0 ) <= s . w } ; :: thesis: verum
end;
end;
end;
then A37: not { w where w is Element of NAT : ( s . (f . 0 ) <= s . w & f . 0 < w ) } is finite by A30, A31, A32, TARSKI:2;
defpred S4[ Element of NAT ] means S1[$1,f . $1,f . ($1 + 1)];
A38: S4[ 0 ] by A15, A37;
A39: now
let k be Element of NAT ; :: thesis: ( S4[k] implies S4[k + 1] )
assume S4[k] ; :: thesis: S4[k + 1]
then consider N being Subset of the carrier of R, B being non empty Subset of the carrier of R such that
A40: N = { (s . w) where w is Element of NAT : ( s . (f . k) <= s . w & f . k < w ) } and
A41: not { w where w is Element of NAT : ( s . (f . k) <= s . w & f . k < w ) } is finite and
A42: B = choose { BB where BB is Element of Dickson-bases N,R : BB is finite } and
A43: f . (k + 1) = s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . k) is finite ) } ),(f . k) ;
set BALL = { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . k) is finite ) } ;
set BBX = { BB where BB is Element of Dickson-bases N,R : BB is finite } ;
set iN = { w where w is Element of NAT : ( s . (f . k) <= s . w & f . k < w ) } ;
consider BD being set such that
A44: BD is_Dickson-basis_of N,R and
A45: BD is finite by A1, Def10;
BD in Dickson-bases N,R by A1, A44, Def13;
then BD in { BB where BB is Element of Dickson-bases N,R : BB is finite } by A45;
then B in { BB where BB is Element of Dickson-bases N,R : BB is finite } by A42;
then A46: ex BB being Element of Dickson-bases N,R st
( B = BB & BB is finite ) ;
then A47: B is_Dickson-basis_of N,R by A1, Def13;
now
deffunc H4( Element of rng s) -> set = H1($1,f . k);
A48: B is finite by A46;
assume A49: for b being Element of rng s st b in B holds
H1(b,f . k) is finite ; :: thesis: contradiction
set Ball = { H4(b) where b is Element of rng s : b in B } ;
A50: { H4(b) where b is Element of rng s : b in B } is finite from FRAENKEL:sch 21(A48);
now
let X be set ; :: thesis: ( X in { H4(b) where b is Element of rng s : b in B } implies X is finite )
assume X in { H4(b) where b is Element of rng s : b in B } ; :: thesis: X is finite
then ex b being Element of rng s st
( X = H1(b,f . k) & b in B ) ;
hence X is finite by A49; :: thesis: verum
end;
then A51: union { H4(b) where b is Element of rng s : b in B } is finite by A50, FINSET_1:25;
{ w where w is Element of NAT : ( s . (f . k) <= s . w & f . k < w ) } c= union { H4(b) where b is Element of rng s : b in B }
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of NAT : ( s . (f . k) <= s . w & f . k < w ) } or x in union { H4(b) where b is Element of rng s : b in B } )
assume x in { w where w is Element of NAT : ( s . (f . k) <= s . w & f . k < w ) } ; :: thesis: x in union { H4(b) where b is Element of rng s : b in B }
then consider w being Element of NAT such that
A52: x = w and
A53: s . (f . k) <= s . w and
A54: f . k < w ;
A55: s . w in N by A40, A53, A54;
reconsider sw = s . w as Element of R ;
consider b being Element of R such that
A56: b in B and
A57: b <= sw by A47, A55, Def9;
A58: B c= N by A47, Def9;
N c= rng s
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in N or x in rng s )
assume x in N ; :: thesis: x in rng s
then A59: ex u being Element of NAT st
( x = s . u & s . (f . k) <= s . u & f . k < u ) by A40;
dom s = NAT by FUNCT_2:def 1;
hence x in rng s by A59, FUNCT_1:12; :: thesis: verum
end;
then B c= rng s by A58, XBOOLE_1:1;
then reconsider b = b as Element of rng s by A56;
A60: w in H1(b,f . k) by A54, A57;
H1(b,f . k) in { H4(b) where b is Element of rng s : b in B } by A56;
hence x in union { H4(b) where b is Element of rng s : b in B } by A52, A60, TARSKI:def 4; :: thesis: verum
end;
hence contradiction by A41, A51; :: thesis: verum
end;
then consider b being Element of rng s such that
A61: b in B and
A62: not H1(b,f . k) is finite ;
b in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . k) is finite ) } by A61, A62;
then choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . k) is finite ) } in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . k) is finite ) } ;
then consider b being Element of B such that
A63: b = choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . k) is finite ) } and
A64: ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . k) is finite ) ;
A65: b in B ;
B c= N by A47, Def9;
then b in N by A65;
then A66: ex w being Element of NAT st
( b = s . w & s . (f . k) <= s . w & f . k < w ) by A40;
then A67: s . (f . (k + 1)) = choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . k) is finite ) } by A43, A63, Def12;
A68: f . k < f . (k + 1) by A43, A63, A66, Def12;
deffunc H4( set ) -> set = $1;
defpred S5[ Element of NAT ] means s . (f . (k + 1)) <= s . $1;
set W1 = { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . k < w1 ) } ;
set W2 = { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } ;
set W3 = { H4(w1) where w1 is Element of NAT : ( f . k < w1 & w1 <= f . (k + 1) & S5[w1] ) } ;
A69: { H4(w1) where w1 is Element of NAT : ( f . k < w1 & w1 <= f . (k + 1) & S5[w1] ) } is finite from DICKSON:sch 1();
now
let x be set ; :: thesis: ( ( x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . k < w1 ) } implies x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } \/ { H4(w1) where w1 is Element of NAT : ( f . k < w1 & w1 <= f . (k + 1) & S5[w1] ) } ) & ( x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } \/ { H4(w1) where w1 is Element of NAT : ( f . k < w1 & w1 <= f . (k + 1) & S5[w1] ) } implies b1 in { b2 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . b2 & f . k < b2 ) } ) )
hereby :: thesis: ( x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } \/ { H4(w1) where w1 is Element of NAT : ( f . k < w1 & w1 <= f . (k + 1) & S5[w1] ) } implies b1 in { b2 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . b2 & f . k < b2 ) } )
assume x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . k < w1 ) } ; :: thesis: x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } \/ { H4(w1) where w1 is Element of NAT : ( f . k < w1 & w1 <= f . (k + 1) & S5[w1] ) }
then consider w being Element of NAT such that
A70: x = w and
A71: s . (f . (k + 1)) <= s . w and
A72: f . k < w ;
( w <= f . (k + 1) or w > f . (k + 1) ) ;
then ( x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } or x in { H4(w1) where w1 is Element of NAT : ( f . k < w1 & w1 <= f . (k + 1) & S5[w1] ) } ) by A70, A71, A72;
hence x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } \/ { H4(w1) where w1 is Element of NAT : ( f . k < w1 & w1 <= f . (k + 1) & S5[w1] ) } by XBOOLE_0:def 3; :: thesis: verum
end;
assume A73: x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } \/ { H4(w1) where w1 is Element of NAT : ( f . k < w1 & w1 <= f . (k + 1) & S5[w1] ) } ; :: thesis: b1 in { b2 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . b2 & f . k < b2 ) }
per cases ( x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } or x in { H4(w1) where w1 is Element of NAT : ( f . k < w1 & w1 <= f . (k + 1) & S5[w1] ) } ) by A73, XBOOLE_0:def 3;
suppose x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } ; :: thesis: b1 in { b2 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . b2 & f . k < b2 ) }
then consider w being Element of NAT such that
A74: x = w and
A75: s . (f . (k + 1)) <= s . w and
A76: f . (k + 1) < w ;
f . k < w by A68, A76, XXREAL_0:2;
hence x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . k < w1 ) } by A74, A75; :: thesis: verum
end;
suppose x in { H4(w1) where w1 is Element of NAT : ( f . k < w1 & w1 <= f . (k + 1) & S5[w1] ) } ; :: thesis: b1 in { b2 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . b2 & f . k < b2 ) }
then ex w being Element of NAT st
( x = w & f . k < w & w <= f . (k + 1) & s . (f . (k + 1)) <= s . w ) ;
hence x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . k < w1 ) } ; :: thesis: verum
end;
end;
end;
then not { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } is finite by A63, A64, A67, A69, TARSKI:2;
hence S4[k + 1] by A15; :: thesis: verum
end;
A77: for n being Element of NAT holds S4[n] from NAT_1:sch 1(A38, A39);
 set t = s * f;
take s * f ; :: thesis: ( s * f is subsequence of s & s * f is weakly-ascending )
reconsider f = f as Function of NAT ,REAL by FUNCT_2:9;
now
now
let n be Element of NAT ; :: thesis: f . n < f . (n + 1)
f . n in rng f by A16, FUNCT_1:def 5;
then reconsider fn = f . n as Element of NAT by A17;
consider N being Subset of the carrier of R, B being non empty Subset of the carrier of R such that
A78: N = { (s . w) where w is Element of NAT : ( s . fn <= s . w & fn < w ) } and
A79: not { w where w is Element of NAT : ( s . fn <= s . w & fn < w ) } is finite and
A80: B = choose { BB where BB is Element of Dickson-bases N,R : BB is finite } and
A81: f . (n + 1) = s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,fn) is finite ) } ),fn by A77;
set BBX = { BB where BB is Element of Dickson-bases N,R : BB is finite } ;
set BJ = { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,fn) is finite ) } ;
set BC = choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,fn) is finite ) } ;
consider BD being set such that
A82: BD is_Dickson-basis_of N,R and
A83: BD is finite by A1, Def10;
BD in Dickson-bases N,R by A1, A82, Def13;
then BD in { BB where BB is Element of Dickson-bases N,R : BB is finite } by A83;
then B in { BB where BB is Element of Dickson-bases N,R : BB is finite } by A80;
then A84: ex BB being Element of Dickson-bases N,R st
( B = BB & BB is finite ) ;
then A85: B is_Dickson-basis_of N,R by A1, Def13;
then A86: B c= N by Def9;
now
A87: B is finite by A84;
assume A88: for b being Element of rng s st b in B holds
H1(b,fn) is finite ; :: thesis: contradiction
deffunc H4( Element of rng s) -> set = H1($1,fn);
set Ball = { H4(b) where b is Element of rng s : b in B } ;
set iN = { w where w is Element of NAT : ( s . fn <= s . w & fn < w ) } ;
A89: { H4(b) where b is Element of rng s : b in B } is finite from FRAENKEL:sch 21(A87);
now
let X be set ; :: thesis: ( X in { H4(b) where b is Element of rng s : b in B } implies X is finite )
assume X in { H4(b) where b is Element of rng s : b in B } ; :: thesis: X is finite
then ex b being Element of rng s st
( X = H1(b,fn) & b in B ) ;
hence X is finite by A88; :: thesis: verum
end;
then A90: union { H4(b) where b is Element of rng s : b in B } is finite by A89, FINSET_1:25;
{ w where w is Element of NAT : ( s . fn <= s . w & fn < w ) } c= union { H4(b) where b is Element of rng s : b in B }
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of NAT : ( s . fn <= s . w & fn < w ) } or x in union { H4(b) where b is Element of rng s : b in B } )
assume x in { w where w is Element of NAT : ( s . fn <= s . w & fn < w ) } ; :: thesis: x in union { H4(b) where b is Element of rng s : b in B }
then consider w being Element of NAT such that
A91: x = w and
A92: s . fn <= s . w and
A93: f . n < w ;
A94: s . w in N by A78, A92, A93;
reconsider sw = s . w as Element of R ;
consider b being Element of R such that
A95: b in B and
A96: b <= sw by A85, A94, Def9;
A97: B c= N by A85, Def9;
N c= rng s
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in N or x in rng s )
assume x in N ; :: thesis: x in rng s
then A98: ex u being Element of NAT st
( x = s . u & s . fn <= s . u & fn < u ) by A78;
dom s = NAT by FUNCT_2:def 1;
hence x in rng s by A98, FUNCT_1:12; :: thesis: verum
end;
then B c= rng s by A97, XBOOLE_1:1;
then reconsider b = b as Element of rng s by A95;
A99: w in H1(b,fn) by A93, A96;
H1(b,fn) in { H4(b) where b is Element of rng s : b in B } by A95;
hence x in union { H4(b) where b is Element of rng s : b in B } by A91, A99, TARSKI:def 4; :: thesis: verum
end;
hence contradiction by A79, A90; :: thesis: verum
end;
then consider b being Element of rng s such that
A100: b in B and
A101: not H1(b,fn) is finite ;
b in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,fn) is finite ) } by A100, A101;
then choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,fn) is finite ) } in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,fn) is finite ) } ;
then ex b being Element of B st
( choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,fn) is finite ) } = b & ex b9 being Element of rng s st
( b9 = b & not H1(b9,fn) is finite ) ) ;
then choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,fn) is finite ) } in N by A86, TARSKI:def 3;
then ex j being Element of NAT st
( choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,fn) is finite ) } = s . j & s . fn <= s . j & fn < j ) by A78;
hence f . n < f . (n + 1) by A81, Def12; :: thesis: verum
end;
hence f is increasing by SEQM_3:def 11; :: thesis: for n being Element of NAT holds f . n is Element of NAT
let n be Element of NAT ; :: thesis: f . n is Element of NAT
f . n in rng f by A16, FUNCT_1:def 5;
hence f . n is Element of NAT by A17; :: thesis: verum
end;
then reconsider f = f as increasing sequence of NAT ;
s * f = s * f ;
hence s * f is subsequence of s ; :: thesis: s * f is weakly-ascending
let n be Element of NAT ; :: according to DICKSON:def 2 :: thesis: [((s * f) . n),((s * f) . (n + 1))] in the InternalRel of R
A102: (s * f) . n = s . (f . n) by A16, FUNCT_1:23;
A103: (s * f) . (n + 1) = s . (f . (n + 1)) by A16, FUNCT_1:23;
consider N being Subset of the carrier of R, B being non empty Subset of the carrier of R such that
A104: N = { (s . w) where w is Element of NAT : ( s . (f . n) <= s . w & f . n < w ) } and
A105: not { w where w is Element of NAT : ( s . (f . n) <= s . w & f . n < w ) } is finite and
A106: B = choose { BB where BB is Element of Dickson-bases N,R : BB is finite } and
A107: f . (n + 1) = s mindex (choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . n) is finite ) } ),(f . n) by A77;
set BX = { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . n) is finite ) } ;
set sfn1 = choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . n) is finite ) } ;
set BBX = { BB where BB is Element of Dickson-bases N,R : BB is finite } ;
consider BD being set such that
A108: BD is_Dickson-basis_of N,R and
A109: BD is finite by A1, Def10;
BD in Dickson-bases N,R by A1, A108, Def13;
then BD in { BB where BB is Element of Dickson-bases N,R : BB is finite } by A109;
then B in { BB where BB is Element of Dickson-bases N,R : BB is finite } by A106;
then A110: ex BB being Element of Dickson-bases N,R st
( BB = B & BB is finite ) ;
then A111: B is_Dickson-basis_of N,R by A1, Def13;
now
A112: B is finite by A110;
assume A113: for b being Element of rng s st b in B holds
H1(b,f . n) is finite ; :: thesis: contradiction
deffunc H4( Element of rng s) -> set = H1($1,f . n);
set Ball = { H4(b) where b is Element of rng s : b in B } ;
set iN = { w where w is Element of NAT : ( s . (f . n) <= s . w & f . n < w ) } ;
A114: { H4(b) where b is Element of rng s : b in B } is finite from FRAENKEL:sch 21(A112);
now
let X be set ; :: thesis: ( X in { H4(b) where b is Element of rng s : b in B } implies X is finite )
assume X in { H4(b) where b is Element of rng s : b in B } ; :: thesis: X is finite
then ex b being Element of rng s st
( X = H1(b,f . n) & b in B ) ;
hence X is finite by A113; :: thesis: verum
end;
then A115: union { H4(b) where b is Element of rng s : b in B } is finite by A114, FINSET_1:25;
{ w where w is Element of NAT : ( s . (f . n) <= s . w & f . n < w ) } c= union { H4(b) where b is Element of rng s : b in B }
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of NAT : ( s . (f . n) <= s . w & f . n < w ) } or x in union { H4(b) where b is Element of rng s : b in B } )
assume x in { w where w is Element of NAT : ( s . (f . n) <= s . w & f . n < w ) } ; :: thesis: x in union { H4(b) where b is Element of rng s : b in B }
then consider w being Element of NAT such that
A116: x = w and
A117: s . (f . n) <= s . w and
A118: f . n < w ;
A119: s . w in N by A104, A117, A118;
reconsider sw = s . w as Element of R ;
consider b being Element of R such that
A120: b in B and
A121: b <= sw by A111, A119, Def9;
A122: B c= N by A111, Def9;
N c= rng s
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in N or x in rng s )
assume x in N ; :: thesis: x in rng s
then A123: ex u being Element of NAT st
( x = s . u & s . (f . n) <= s . u & f . n < u ) by A104;
dom s = NAT by FUNCT_2:def 1;
hence x in rng s by A123, FUNCT_1:12; :: thesis: verum
end;
then B c= rng s by A122, XBOOLE_1:1;
then reconsider b = b as Element of rng s by A120;
A124: w in H1(b,f . n) by A118, A121;
H1(b,f . n) in { H4(b) where b is Element of rng s : b in B } by A120;
hence x in union { H4(b) where b is Element of rng s : b in B } by A116, A124, TARSKI:def 4; :: thesis: verum
end;
hence contradiction by A105, A115; :: thesis: verum
end;
then consider b being Element of rng s such that
A125: b in B and
A126: not H1(b,f . n) is finite ;
b in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . n) is finite ) } by A125, A126;
then choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . n) is finite ) } in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . n) is finite ) } ;
then ex b being Element of B st
( b = choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . n) is finite ) } & ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . n) is finite ) ) ;
then A127: choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . n) is finite ) } in B ;
B c= N by A111, Def9;
then choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . n) is finite ) } in N by A127;
then ex w being Element of NAT st
( choose { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & not H1(b9,f . n) is finite ) } = s . w & s . (f . n) <= s . w & f . n < w ) by A104;
then (s * f) . n <= (s * f) . (n + 1) by A102, A103, A107, Def12;
hence [((s * f) . n),((s * f) . (n + 1))] in the InternalRel of R by ORDERS_2:def 9; :: thesis: verum