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 b' being Element of rng s st
( b' = b & not H1(b',$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 consider w being Element of NAT such that
A3: ( y = s . w & s . x <= s . w & x < w ) ;
thus y in the carrier of R by A3; :: 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 A4: 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
A5: 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
A6: ( s . x <= s . www & x < www ) by A5;
s . www in N by A6;
hence S1[n,x,1] by A4; :: 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 consider BBB being Element of Dickson-bases N,R such that
A10: choose { BB where BB is Element of Dickson-bases N,R : BB is finite } = BBB and
BBB is finite ;
A11: choose { BB where BB is Element of Dickson-bases N,R : BB is finite } is_Dickson-basis_of N,R by A1, A10, 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, A11, Th27, XBOOLE_1:1;
set y = s mindex (choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',x) is finite ) } ),x;
take s mindex (choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',x) is finite ) } ),x ; :: thesis: S2[n,x,s mindex (choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',x) is finite ) } ),x]
set W = { w where w is Element of NAT : ( s . x <= s . w & x < w ) } ;
assume A12: 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 b' being Element of rng s st
( b' = b & not H1(b',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 b' being Element of rng s st
( b' = b & not H1(b',x) is finite ) } ),x = s mindex (choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',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 b' being Element of rng s st
( b' = b & not H1(b',x) is finite ) } ),x = s mindex (choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',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 b' being Element of rng s st
( b' = b & not H1(b',x) is finite ) } ),x = s mindex (choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',x) is finite ) } ),x )
thus not { w where w is Element of NAT : ( s . x <= s . w & x < w ) } is finite by A12; :: 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 b' being Element of rng s st
( b' = b & not H1(b',x) is finite ) } ),x = s mindex (choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',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 b' being Element of rng s st
( b' = b & not H1(b',x) is finite ) } ),x = s mindex (choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',x) is finite ) } ),x
thus s mindex (choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',x) is finite ) } ),x = s mindex (choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',x) is finite ) } ),x ; :: thesis: verum
end;
end;
end;
consider B being set such that
A13: B is_Dickson-basis_of rng s,R and
A14: B is finite by A1, Def10;
reconsider B = B as non empty set by A13, Th27;
set BALL = { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H2(b') is finite ) } ;
set b1 = choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H2(b') is finite ) } ;
consider f being Function of NAT ,NAT such that
A15: f . 0 = s mindex (choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H2(b') is finite ) } ) and
A16: for n being Element of NAT holds S2[n,f . n,f . (n + 1)] from RECDEF_1:sch 2(A2);
 A17: dom f = NAT by FUNCT_2:def 1;
A18: rng f c= NAT ;
now
A19: B is finite by A14;
assume A20: 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 } ;
A21: { H2(b) where b is Element of rng s : b in B } is finite from FRAENKEL:sch 21(A19);
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 consider b being Element of rng s such that
A22: X = H2(b) and
A23: b in B ;
thus X is finite by A20, A22, A23; :: thesis: verum
end;
then A24: union { H2(b) where b is Element of rng s : b in B } is finite by A21, 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 x' = x as Element of NAT ;
dom s = NAT by FUNCT_2:def 1;
then x' in dom s ;
then A25: 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
A26: b in B and
A27: b <= sx by A13, A25, Def9;
B c= rng s by A13, Def9;
then reconsider b = b as Element of rng s by A26;
A28: x' in H2(b) by A27;
H2(b) in { H2(b) where b is Element of rng s : b in B } by A26;
hence x in union { H2(b) where b is Element of rng s : b in B } by A28, 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 A24; :: thesis: verum
end;
then consider tb being Element of rng s such that
A29: ( tb in B & not H2(tb) is finite ) ;
A30: tb in { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H2(b') is finite ) } by A29;
then choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H2(b') is finite ) } in { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H2(b') is finite ) } ;
then consider bt being Element of B such that
A31: choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H2(b') is finite ) } = bt and
A32: ex b' being Element of rng s st
( b' = bt & not H2(b') is finite ) ;
consider b' being Element of rng s such that
A33: b' = bt and
not H2(b') is finite by A32;
dom s = NAT by NORMSP_1:17;
then A34: s . (f . 0 ) = choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H2(b') is finite ) } by A15, A31, A33, Def11;
choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H2(b') is finite ) } in { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H2(b') is finite ) } by A30;
then consider eb being Element of B such that
A35: choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H2(b') is finite ) } = eb and
A36: ex eb' being Element of rng s st
( eb' = eb & not H2(eb') is finite ) ;
consider eb' being Element of rng s such that
A37: eb' = eb and
A38: not H2(eb') is finite by A36;
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] ) } ;
A39: { 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
A40: x = w and
A41: s . (f . 0 ) <= s . w ;
A42: 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 A40, A41, A42;
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 A43: 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 A43, 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 consider w being Element of NAT such that
A44: ( x = w & s . (f . 0 ) <= s . w & f . 0 < w ) ;
thus x in { w where w is Element of NAT : s . (f . 0 ) <= s . w } by A44; :: 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 consider w being Element of NAT such that
A45: ( x = w & 0 <= w & w <= f . 0 & s . (f . 0 ) <= s . w ) ;
thus x in { w where w is Element of NAT : s . (f . 0 ) <= s . w } by A45; :: thesis: verum
end;
end;
end;
then { w where w is Element of NAT : s . (f . 0 ) <= s . w } = { 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 TARSKI:2;
then A46: not { w where w is Element of NAT : ( s . (f . 0 ) <= s . w & f . 0 < w ) } is finite by A34, A35, A37, A38, A39;
defpred S4[ Element of NAT ] means S1[$1,f . $1,f . ($1 + 1)];
A47: S4[ 0 ] by A16, A46;
A48: now
let k be Element of NAT ; :: thesis: ( S4[k] implies S4[k + 1] )
assume A49: S4[k] ; :: thesis: S4[k + 1]
consider N being Subset of the carrier of R, B being non empty Subset of the carrier of R such that
A50: N = { (s . w) where w is Element of NAT : ( s . (f . k) <= s . w & f . k < w ) } and
A51: not { w where w is Element of NAT : ( s . (f . k) <= s . w & f . k < w ) } is finite and
A52: B = choose { BB where BB is Element of Dickson-bases N,R : BB is finite } and
A53: f . (k + 1) = s mindex (choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',f . k) is finite ) } ),(f . k) by A49;
set BALL = { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',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
A54: ( BD is_Dickson-basis_of N,R & BD is finite ) by A1, Def10;
BD in Dickson-bases N,R by A1, A54, Def13;
then BD in { BB where BB is Element of Dickson-bases N,R : BB is finite } by A54;
then B in { BB where BB is Element of Dickson-bases N,R : BB is finite } by A52;
then consider BB being Element of Dickson-bases N,R such that
A55: ( B = BB & BB is finite ) ;
A56: B is_Dickson-basis_of N,R by A1, A55, Def13;
now
deffunc H4( Element of rng s) -> set = H1($1,f . k);
A57: B is finite by A55;
assume A58: 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 } ;
A59: { H4(b) where b is Element of rng s : b in B } is finite from FRAENKEL:sch 21(A57);
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 consider b being Element of rng s such that
A60: X = H1(b,f . k) and
A61: b in B ;
thus X is finite by A58, A60, A61; :: thesis: verum
end;
then A62: union { H4(b) where b is Element of rng s : b in B } is finite by A59, 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
A63: x = w and
A64: s . (f . k) <= s . w and
A65: f . k < w ;
A66: s . w in N by A50, A64, A65;
reconsider sw = s . w as Element of R ;
consider b being Element of R such that
A67: b in B and
A68: b <= sw by A56, A66, Def9;
A69: B c= N by A56, 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 consider u being Element of NAT such that
A70: x = s . u and
s . (f . k) <= s . u and
f . k < u by A50;
dom s = NAT by FUNCT_2:def 1;
hence x in rng s by A70, FUNCT_1:12; :: thesis: verum
end;
then B c= rng s by A69, XBOOLE_1:1;
then reconsider b = b as Element of rng s by A67;
A71: w in H1(b,f . k) by A65, A68;
H1(b,f . k) in { H4(b) where b is Element of rng s : b in B } by A67;
hence x in union { H4(b) where b is Element of rng s : b in B } by A63, A71, TARSKI:def 4; :: thesis: verum
end;
hence contradiction by A51, A62; :: thesis: verum
end;
then consider b being Element of rng s such that
A72: ( b in B & not H1(b,f . k) is finite ) ;
b in { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',f . k) is finite ) } by A72;
then choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',f . k) is finite ) } in { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',f . k) is finite ) } ;
then consider b being Element of B such that
A73: b = choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',f . k) is finite ) } and
A74: ex b' being Element of rng s st
( b' = b & not H1(b',f . k) is finite ) ;
consider b' being Element of rng s such that
A75: b' = b and
A76: not H1(b',f . k) is finite by A74;
A77: b in B ;
B c= N by A56, Def9;
then b in N by A77;
then consider w being Element of NAT such that
A78: b = s . w and
s . (f . k) <= s . w and
A79: f . k < w by A50;
A80: s . (f . (k + 1)) = choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',f . k) is finite ) } by A53, A73, A78, A79, Def12;
A81: f . k < f . (k + 1) by A53, A73, A78, A79, 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] ) } ;
A82: { 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
A83: x = w and
A84: ( s . (f . (k + 1)) <= s . w & 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 A83, A84;
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 A85: 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 A85, 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
A86: ( x = w & s . (f . (k + 1)) <= s . w & f . (k + 1) < w ) ;
f . k < w by A81, A86, XXREAL_0:2;
hence x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . k < w1 ) } by A86; :: 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 consider w being Element of NAT such that
A87: ( x = w & f . k < w & w <= f . (k + 1) & s . (f . (k + 1)) <= s . w ) ;
thus x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . k < w1 ) } by A87; :: thesis: verum
end;
end;
end;
then { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . k < w1 ) } = { 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 TARSKI:2;
then not { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } is finite by A73, A75, A76, A80, A82;
hence S4[k + 1] by A16; :: thesis: verum
end;
A88: for n being Element of NAT holds S4[n] from NAT_1:sch 1(A47, A48);
 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 A17, FUNCT_1:def 5;
then reconsider fn = f . n as Element of NAT by A18;
consider N being Subset of the carrier of R, B being non empty Subset of the carrier of R such that
A89: N = { (s . w) where w is Element of NAT : ( s . fn <= s . w & fn < w ) } and
A90: not { w where w is Element of NAT : ( s . fn <= s . w & fn < w ) } is finite and
A91: B = choose { BB where BB is Element of Dickson-bases N,R : BB is finite } and
A92: f . (n + 1) = s mindex (choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',fn) is finite ) } ),fn by A88;
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 b' being Element of rng s st
( b' = b & not H1(b',fn) is finite ) } ;
set BC = choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',fn) is finite ) } ;
consider BD being set such that
A93: ( BD is_Dickson-basis_of N,R & BD is finite ) by A1, Def10;
BD in Dickson-bases N,R by A1, A93, Def13;
then BD in { BB where BB is Element of Dickson-bases N,R : BB is finite } by A93;
then B in { BB where BB is Element of Dickson-bases N,R : BB is finite } by A91;
then consider BB being Element of Dickson-bases N,R such that
A94: B = BB and
A95: BB is finite ;
A96: B is_Dickson-basis_of N,R by A1, A94, Def13;
then A97: B c= N by Def9;
now
A98: B is finite by A94, A95;
assume A99: 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 ) } ;
A100: { H4(b) where b is Element of rng s : b in B } is finite from FRAENKEL:sch 21(A98);
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 consider b being Element of rng s such that
A101: X = H1(b,fn) and
A102: b in B ;
thus X is finite by A99, A101, A102; :: thesis: verum
end;
then A103: union { H4(b) where b is Element of rng s : b in B } is finite by A100, 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
A104: x = w and
A105: s . fn <= s . w and
A106: f . n < w ;
A107: s . w in N by A89, A105, A106;
reconsider sw = s . w as Element of R ;
consider b being Element of R such that
A108: b in B and
A109: b <= sw by A96, A107, Def9;
A110: B c= N by A96, 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 consider u being Element of NAT such that
A111: x = s . u and
s . fn <= s . u and
fn < u by A89;
dom s = NAT by FUNCT_2:def 1;
hence x in rng s by A111, FUNCT_1:12; :: thesis: verum
end;
then B c= rng s by A110, XBOOLE_1:1;
then reconsider b = b as Element of rng s by A108;
A112: w in H1(b,fn) by A106, A109;
H1(b,fn) in { H4(b) where b is Element of rng s : b in B } by A108;
hence x in union { H4(b) where b is Element of rng s : b in B } by A104, A112, TARSKI:def 4; :: thesis: verum
end;
hence contradiction by A90, A103; :: thesis: verum
end;
then consider b being Element of rng s such that
A113: ( b in B & not H1(b,fn) is finite ) ;
b in { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',fn) is finite ) } by A113;
then choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',fn) is finite ) } in { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',fn) is finite ) } ;
then consider b being Element of B such that
A114: choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',fn) is finite ) } = b and
ex b' being Element of rng s st
( b' = b & not H1(b',fn) is finite ) ;
choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',fn) is finite ) } in N by A97, A114, TARSKI:def 3;
then consider j being Element of NAT such that
A115: ( choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',fn) is finite ) } = s . j & s . fn <= s . j & fn < j ) by A89;
thus f . n < f . (n + 1) by A92, A115, 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 A17, FUNCT_1:def 5;
hence f . n is Element of NAT by A18; :: 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
A116: (s * f) . n = s . (f . n) by A17, FUNCT_1:23;
A117: (s * f) . (n + 1) = s . (f . (n + 1)) by A17, FUNCT_1:23;
consider N being Subset of the carrier of R, B being non empty Subset of the carrier of R such that
A118: N = { (s . w) where w is Element of NAT : ( s . (f . n) <= s . w & f . n < w ) } and
A119: not { w where w is Element of NAT : ( s . (f . n) <= s . w & f . n < w ) } is finite and
A120: B = choose { BB where BB is Element of Dickson-bases N,R : BB is finite } and
A121: f . (n + 1) = s mindex (choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',f . n) is finite ) } ),(f . n) by A88;
set BX = { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',f . n) is finite ) } ;
set sfn1 = choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',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
A122: ( BD is_Dickson-basis_of N,R & BD is finite ) by A1, Def10;
BD in Dickson-bases N,R by A1, A122, Def13;
then BD in { BB where BB is Element of Dickson-bases N,R : BB is finite } by A122;
then B in { BB where BB is Element of Dickson-bases N,R : BB is finite } by A120;
then consider BB being Element of Dickson-bases N,R such that
A123: BB = B and
A124: BB is finite ;
A125: B is_Dickson-basis_of N,R by A1, A123, Def13;
now
A126: B is finite by A123, A124;
assume A127: 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 ) } ;
A128: { H4(b) where b is Element of rng s : b in B } is finite from FRAENKEL:sch 21(A126);
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 consider b being Element of rng s such that
A129: X = H1(b,f . n) and
A130: b in B ;
thus X is finite by A127, A129, A130; :: thesis: verum
end;
then A131: union { H4(b) where b is Element of rng s : b in B } is finite by A128, 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
A132: x = w and
A133: s . (f . n) <= s . w and
A134: f . n < w ;
A135: s . w in N by A118, A133, A134;
reconsider sw = s . w as Element of R ;
consider b being Element of R such that
A136: b in B and
A137: b <= sw by A125, A135, Def9;
A138: B c= N by A125, 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 consider u being Element of NAT such that
A139: x = s . u and
s . (f . n) <= s . u and
f . n < u by A118;
dom s = NAT by FUNCT_2:def 1;
hence x in rng s by A139, FUNCT_1:12; :: thesis: verum
end;
then B c= rng s by A138, XBOOLE_1:1;
then reconsider b = b as Element of rng s by A136;
A140: w in H1(b,f . n) by A134, A137;
H1(b,f . n) in { H4(b) where b is Element of rng s : b in B } by A136;
hence x in union { H4(b) where b is Element of rng s : b in B } by A132, A140, TARSKI:def 4; :: thesis: verum
end;
hence contradiction by A119, A131; :: thesis: verum
end;
then consider b being Element of rng s such that
A141: ( b in B & not H1(b,f . n) is finite ) ;
b in { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',f . n) is finite ) } by A141;
then choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',f . n) is finite ) } in { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',f . n) is finite ) } ;
then consider b being Element of B such that
A142: b = choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',f . n) is finite ) } and
ex b' being Element of rng s st
( b' = b & not H1(b',f . n) is finite ) ;
A143: choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',f . n) is finite ) } in B by A142;
B c= N by A125, Def9;
then choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',f . n) is finite ) } in N by A143;
then consider w being Element of NAT such that
A144: choose { b where b is Element of B : ex b' being Element of rng s st
( b' = b & not H1(b',f . n) is finite ) } = s . w and
A145: s . (f . n) <= s . w and
A146: f . n < w by A118;
(s * f) . n <= (s * f) . (n + 1) by A116, A117, A121, A144, A145, A146, Def12;
hence [((s * f) . n),((s * f) . (n + 1))] in the InternalRel of R by ORDERS_2:def 9; :: thesis: verum