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 ) } & { w where w is Element of NAT : ( s . $2 <= s . w & $2 < w ) } is infinite & B = the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite } & $3 = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,$2) is infinite ) } ,$2) );
defpred S2[ set , Element of NAT , set ] means ( { w where w is Element of NAT : ( s . $2 <= s . w & $2 < w ) } is infinite implies S1[$1,$2,$3] );
A2: for n being Nat
for x being Element of NAT ex y being Element of NAT st S2[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of NAT ex y being Element of NAT st S2[n,x,y]
let 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 :: thesis: for y being object st y in { (s . w) where w is Element of NAT : ( s . x <= s . w & x < w ) } holds
y in the carrier of R
let y be object ; :: 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 { w where w is Element of NAT : ( s . x <= s . w & x < w ) } is infinite ; :: thesis: S1[n,x,1]
then consider ww being object 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 = the Element of { 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;
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 the Element of { 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
( the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite } = BBB & BBB is finite ) ;
then A10: the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite } is_Dickson-basis_of N,R by A1, Def13;
reconsider B = the Element of { 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, Th25, XBOOLE_1:1;
set y = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x);
take s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) ; :: thesis: S2[n,x,s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x)]
set W = { w where w is Element of NAT : ( s . x <= s . w & x < w ) } ;
assume A11: { w where w is Element of NAT : ( s . x <= s . w & x < w ) } is infinite ; :: thesis: S1[n,x,s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,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 ) } & { w where w is Element of NAT : ( s . x <= s . w & x < w ) } is infinite & B = the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite } & s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,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 ) } & { w where w is Element of NAT : ( s . x <= s . w & x < w ) } is infinite & B = the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite } & s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) )
thus N = { (s . w) where w is Element of NAT : ( s . x <= s . w & x < w ) } ; :: thesis: ( { w where w is Element of NAT : ( s . x <= s . w & x < w ) } is infinite & B = the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite } & s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) )
thus { w where w is Element of NAT : ( s . x <= s . w & x < w ) } is infinite by A11; :: thesis: ( B = the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite } & s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) )
thus B = the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite } ; :: thesis: s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x)
thus s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,x) = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,x) is infinite ) } ,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;
reconsider B = B as non empty set by A12, Th25;
set BALL = { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } ;
set b1 = the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } ;
consider f being sequence of NAT such that
A14: f . 0 = s mindex the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } and
A15: for n being 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 :: thesis: ex b being Element of rng s st
( b in B & not H2(b) is finite )
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 :: thesis: for X being set st X in { H2(b) where b is Element of rng s : b in B } holds
X is finite
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:7;
now :: thesis: for x being object st x in NAT holds
x in union { H2(b) where b is Element of rng s : b in B }
let x be object ; :: 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:3;
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;
B c= rng s by A12;
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 } ;
hence contradiction by A21; :: thesis: verum
end;
then consider tb being Element of rng s such that
A26: tb in B and
A27: H2(tb) is infinite ;
A28: tb in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } by A26, A27;
then the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } ;
then A29: ex bt being Element of B st
( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } = bt & ex b9 being Element of rng s st
( b9 = bt & H2(b9) is infinite ) ) ;
dom s = NAT by NORMSP_1:12;
then A30: s . (f . 0) = the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } by A14, A29, Def11;
the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } by A28;
then A31: ex eb being Element of B st
( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H2(b9) is infinite ) } = eb & ex eb9 being Element of rng s st
( eb9 = eb & H2(eb9) is infinite ) ) ;
deffunc H3( set ) -> set = $1;
defpred S3[ Nat] means ( 0 <= $1 & 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 Nat : ( w <= f . 0 & S3[w] ) } ;
A32: { H3(w) where w is Nat : ( w <= f . 0 & S3[w] ) } is finite from FINSEQ_1:sch 6();
now :: thesis: for x being object holds
( ( 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 Nat : ( 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 Nat : ( w <= f . 0 & S3[w] ) } implies x in { w where w is Element of NAT : s . (f . 0) <= s . w } ) )
let x be object ; :: 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 Nat : ( 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 Nat : ( 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 Nat : ( 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 Nat : ( 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 Nat : ( 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 Nat : ( 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 Nat : ( 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 Nat : ( 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 Nat : ( w <= f . 0 & S3[w] ) } ; :: thesis: b1 in { b2 where w is Element of NAT : s . (f . 0) <= s . b2 }
then A37: ex w being Nat st
( x = w & w <= f . 0 & 0 <= w & s . (f . 0) <= s . w ) ;
then reconsider w = x as Element of NAT by ORDINAL1:def 12;
( 0 <= w & w <= f . 0 & s . (f . 0) <= s . w ) by A37;
hence x in { w where w is Element of NAT : s . (f . 0) <= s . w } ; :: thesis: verum
end;
end;
end;
then A38: { w where w is Element of NAT : ( s . (f . 0) <= s . w & f . 0 < w ) } is infinite by A30, A31, A32, TARSKI:2;
defpred S4[ Nat] means S1[$1,f . $1,f . ($1 + 1)];
A39: S4[ 0 ] by A15, A38;
A40: now :: thesis: for k being Nat st S4[k] holds
S4[k + 1]
let k be 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
A41: N = { (s . w) where w is Element of NAT : ( s . (f . k) <= s . w & f . k < w ) } and
A42: { w where w is Element of NAT : ( s . (f . k) <= s . w & f . k < w ) } is infinite and
A43: B = the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite } and
A44: f . (k + 1) = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . k) is infinite ) } ,(f . k)) ;
set BALL = { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . k) is infinite ) } ;
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
A45: BD is_Dickson-basis_of N,R and
A46: BD is finite by A1;
BD in Dickson-bases (N,R) by A1, A45, Def13;
then BD in { BB where BB is Element of Dickson-bases (N,R) : BB is finite } by A46;
then B in { BB where BB is Element of Dickson-bases (N,R) : BB is finite } by A43;
then A47: ex BB being Element of Dickson-bases (N,R) st
( B = BB & BB is finite ) ;
then A48: B is_Dickson-basis_of N,R by A1, Def13;
now :: thesis: ex b being Element of rng s st
( b in B & not H1(b,f . k) is finite )
deffunc H4( Element of rng s) -> set = H1($1,f . k);
A49: B is finite by A47;
assume A50: 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 } ;
A51: { H4(b) where b is Element of rng s : b in B } is finite from FRAENKEL:sch 21(A49);
now :: thesis: for X being set st X in { H4(b) where b is Element of rng s : b in B } holds
X is finite
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 A50; :: thesis: verum
end;
then A52: union { H4(b) where b is Element of rng s : b in B } is finite by A51, FINSET_1:7;
{ 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 object ; :: 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
A53: x = w and
A54: s . (f . k) <= s . w and
A55: f . k < w ;
A56: s . w in N by A41, A54, A55;
reconsider sw = s . w as Element of R ;
consider b being Element of R such that
A57: b in B and
A58: b <= sw by A48, A56;
A59: B c= N by A48;
N c= rng s
proof
let x be object ; :: 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 A60: ex u being Element of NAT st
( x = s . u & s . (f . k) <= s . u & f . k < u ) by A41;
dom s = NAT by FUNCT_2:def 1;
hence x in rng s by A60, FUNCT_1:3; :: thesis: verum
end;
then B c= rng s by A59;
then reconsider b = b as Element of rng s by A57;
A61: w in H1(b,f . k) by A55, A58;
H1(b,f . k) in { H4(b) where b is Element of rng s : b in B } by A57;
hence x in union { H4(b) where b is Element of rng s : b in B } by A53, A61, TARSKI:def 4; :: thesis: verum
end;
hence contradiction by A42, A52; :: thesis: verum
end;
then consider b being Element of rng s such that
A62: b in B and
A63: H1(b,f . k) is infinite ;
b in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . k) is infinite ) } by A62, A63;
then the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . k) is infinite ) } in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . k) is infinite ) } ;
then consider b being Element of B such that
A64: b = the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . k) is infinite ) } and
A65: ex b9 being Element of rng s st
( b9 = b & H1(b9,f . k) is infinite ) ;
B c= N by A48;
then b in N ;
then A66: ex w being Element of NAT st
( b = s . w & s . (f . k) <= s . w & f . k < w ) by A41;
then A67: s . (f . (k + 1)) = the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . k) is infinite ) } by A44, A64, Def12;
A68: f . k < f . (k + 1) by A44, A64, A66, Def12;
deffunc H4( set ) -> set = $1;
defpred S5[ Nat] means ( f . k < $1 & 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 Nat : ( w1 <= f . (k + 1) & S5[w1] ) } ;
A69: { H4(w1) where w1 is Nat : ( w1 <= f . (k + 1) & S5[w1] ) } is finite from FINSEQ_1:sch 6();
now :: thesis: for x being object holds
( ( 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 Nat : ( 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 Nat : ( w1 <= f . (k + 1) & S5[w1] ) } implies x in { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . k < w1 ) } ) )
let x be object ; :: 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 Nat : ( 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 Nat : ( 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 Nat : ( 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 Nat : ( 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 Nat : ( 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 Nat : ( 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 Nat : ( 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 Nat : ( 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 Nat : ( 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 Nat such that
A77: ( x = w & w <= f . (k + 1) & f . k < w & s . (f . (k + 1)) <= s . w ) ;
reconsider w = w as Element of NAT by ORDINAL1:def 12;
( x = w & f . k < w & w <= f . (k + 1) & s . (f . (k + 1)) <= s . w ) by A77;
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 { w1 where w1 is Element of NAT : ( s . (f . (k + 1)) <= s . w1 & f . (k + 1) < w1 ) } is infinite by A64, A65, A67, A69, TARSKI:2;
hence S4[k + 1] by A15; :: thesis: verum
end;
A78: for n being Nat holds S4[n] from NAT_1:sch 2(A39, A40);
 set t = s * f;
take s * f ; :: thesis: ( s * f is subsequence of s & s * f is weakly-ascending )
reconsider f = f as sequence of REAL by FUNCT_2:7, NUMBERS:19;
now :: thesis: ( f is increasing & ( for n being Element of NAT holds f . n is Element of NAT ) )
now :: thesis: for n being Nat holds f . n < f . (n + 1)
let n be Nat; :: thesis: f . n < f . (n + 1)
A79: n in NAT by ORDINAL1:def 12;
f . n in rng f by A16, A79, FUNCT_1:def 3;
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
A80: N = { (s . w) where w is Element of NAT : ( s . fn <= s . w & fn < w ) } and
A81: { w where w is Element of NAT : ( s . fn <= s . w & fn < w ) } is infinite and
A82: B = the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite } and
A83: f . (n + 1) = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) } ,fn) by A78;
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 & H1(b9,fn) is infinite ) } ;
set BC = the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) } ;
consider BD being set such that
A84: BD is_Dickson-basis_of N,R and
A85: BD is finite by A1;
BD in Dickson-bases (N,R) by A1, A84, Def13;
then BD in { BB where BB is Element of Dickson-bases (N,R) : BB is finite } by A85;
then B in { BB where BB is Element of Dickson-bases (N,R) : BB is finite } by A82;
then A86: ex BB being Element of Dickson-bases (N,R) st
( B = BB & BB is finite ) ;
then A87: B is_Dickson-basis_of N,R by A1, Def13;
then A88: B c= N ;
now :: thesis: ex b being Element of rng s st
( b in B & not H1(b,fn) is finite )
A89: B is finite by A86;
assume A90: 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 ) } ;
A91: { H4(b) where b is Element of rng s : b in B } is finite from FRAENKEL:sch 21(A89);
now :: thesis: for X being set st X in { H4(b) where b is Element of rng s : b in B } holds
X is finite
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 A90; :: thesis: verum
end;
then A92: union { H4(b) where b is Element of rng s : b in B } is finite by A91, FINSET_1:7;
{ 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 object ; :: 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
A93: x = w and
A94: s . fn <= s . w and
A95: f . n < w ;
A96: s . w in N by A80, A94, A95;
reconsider sw = s . w as Element of R ;
consider b being Element of R such that
A97: b in B and
A98: b <= sw by A87, A96;
A99: B c= N by A87;
N c= rng s
proof
let x be object ; :: 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 A100: ex u being Element of NAT st
( x = s . u & s . fn <= s . u & fn < u ) by A80;
dom s = NAT by FUNCT_2:def 1;
hence x in rng s by A100, FUNCT_1:3; :: thesis: verum
end;
then B c= rng s by A99;
then reconsider b = b as Element of rng s by A97;
A101: w in H1(b,fn) by A95, A98;
H1(b,fn) in { H4(b) where b is Element of rng s : b in B } by A97;
hence x in union { H4(b) where b is Element of rng s : b in B } by A93, A101, TARSKI:def 4; :: thesis: verum
end;
hence contradiction by A81, A92; :: thesis: verum
end;
then consider b being Element of rng s such that
A102: b in B and
A103: H1(b,fn) is infinite ;
b in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) } by A102, A103;
then the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) } in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) } ;
then ex b being Element of B st
( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) } = b & ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) ) ;
then the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) } in N by A88;
then ex j being Element of NAT st
( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,fn) is infinite ) } = s . j & s . fn <= s . j & fn < j ) by A80;
hence f . n < f . (n + 1) by A83, Def12; :: thesis: verum
end;
hence f is increasing by SEQM_3:def 6; :: 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 3;
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 Nat; :: according to DICKSON:def 2 :: thesis: [((s * f) . n),((s * f) . (n + 1))] in the InternalRel of R
n in NAT by ORDINAL1:def 12;
then A104: (s * f) . n = s . (f . n) by A16, FUNCT_1:13;
A105: (s * f) . (n + 1) = s . (f . (n + 1)) by A16, FUNCT_1:13;
consider N being Subset of the carrier of R, B being non empty Subset of the carrier of R such that
A106: N = { (s . w) where w is Element of NAT : ( s . (f . n) <= s . w & f . n < w ) } and
A107: { w where w is Element of NAT : ( s . (f . n) <= s . w & f . n < w ) } is infinite and
A108: B = the Element of { BB where BB is Element of Dickson-bases (N,R) : BB is finite } and
A109: f . (n + 1) = s mindex ( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } ,(f . n)) by A78;
set BX = { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } ;
set sfn1 = the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } ;
set BBX = { BB where BB is Element of Dickson-bases (N,R) : BB is finite } ;
consider BD being set such that
A110: BD is_Dickson-basis_of N,R and
A111: BD is finite by A1;
BD in Dickson-bases (N,R) by A1, A110, Def13;
then BD in { BB where BB is Element of Dickson-bases (N,R) : BB is finite } by A111;
then B in { BB where BB is Element of Dickson-bases (N,R) : BB is finite } by A108;
then A112: ex BB being Element of Dickson-bases (N,R) st
( BB = B & BB is finite ) ;
then A113: B is_Dickson-basis_of N,R by A1, Def13;
now :: thesis: ex b being Element of rng s st
( b in B & not H1(b,f . n) is finite )
A114: B is finite by A112;
assume A115: 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 ) } ;
A116: { H4(b) where b is Element of rng s : b in B } is finite from FRAENKEL:sch 21(A114);
now :: thesis: for X being set st X in { H4(b) where b is Element of rng s : b in B } holds
X is finite
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 A115; :: thesis: verum
end;
then A117: union { H4(b) where b is Element of rng s : b in B } is finite by A116, FINSET_1:7;
{ 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 object ; :: 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
A118: x = w and
A119: s . (f . n) <= s . w and
A120: f . n < w ;
A121: s . w in N by A106, A119, A120;
reconsider sw = s . w as Element of R ;
consider b being Element of R such that
A122: b in B and
A123: b <= sw by A113, A121;
A124: B c= N by A113;
N c= rng s
proof
let x be object ; :: 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 A125: ex u being Element of NAT st
( x = s . u & s . (f . n) <= s . u & f . n < u ) by A106;
dom s = NAT by FUNCT_2:def 1;
hence x in rng s by A125, FUNCT_1:3; :: thesis: verum
end;
then B c= rng s by A124;
then reconsider b = b as Element of rng s by A122;
A126: w in H1(b,f . n) by A120, A123;
H1(b,f . n) in { H4(b) where b is Element of rng s : b in B } by A122;
hence x in union { H4(b) where b is Element of rng s : b in B } by A118, A126, TARSKI:def 4; :: thesis: verum
end;
hence contradiction by A107, A117; :: thesis: verum
end;
then consider b being Element of rng s such that
A127: b in B and
A128: H1(b,f . n) is infinite ;
b in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } by A127, A128;
then the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } in { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } ;
then ex b being Element of B st
( b = the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } & ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) ) ;
then A129: the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } in B ;
B c= N by A113;
then the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } in N by A129;
then ex w being Element of NAT st
( the Element of { b where b is Element of B : ex b9 being Element of rng s st
( b9 = b & H1(b9,f . n) is infinite ) } = s . w & s . (f . n) <= s . w & f . n < w ) by A106;
then (s * f) . n <= (s * f) . (n + 1) by A104, A105, A109, Def12;
hence [((s * f) . n),((s * f) . (n + 1))] in the InternalRel of R ; :: thesis: verum