let X be Subset of NAT; ( X is infinite implies ex N being increasing sequence of NAT st rng N c= X )
assume A1:
X is infinite
; ex N being increasing sequence of NAT st rng N c= X
reconsider BX = bool X as non empty set by ZFMISC_1:def 1;
reconsider N0 = min* X as Element of NAT ;
reconsider Y0 = X as Element of BX by ZFMISC_1:def 1;
defpred S1[ object , object , set , object , set ] means ( $5 = $3 \ {$2} & $4 = min* $5 );
A2:
for n being Nat
for x being Element of NAT
for y being Element of BX ex x1 being Element of NAT ex y1 being Element of BX st S1[n,x,y,x1,y1]
proof
let n be
Nat;
for x being Element of NAT
for y being Element of BX ex x1 being Element of NAT ex y1 being Element of BX st S1[n,x,y,x1,y1]let x be
Element of
NAT ;
for y being Element of BX ex x1 being Element of NAT ex y1 being Element of BX st S1[n,x,y,x1,y1]let y be
Element of
BX;
ex x1 being Element of NAT ex y1 being Element of BX st S1[n,x,y,x1,y1]
reconsider y1 =
y \ {x} as
Element of
BX by XBOOLE_1:1;
set x1 =
min* y1;
take
min* y1
;
ex y1 being Element of BX st S1[n,x,y, min* y1,y1]
take
y1
;
S1[n,x,y, min* y1,y1]
thus
S1[
n,
x,
y,
min* y1,
y1]
;
verum
end;
consider N being sequence of NAT, Y being sequence of BX such that
A3:
( N . 0 = N0 & Y . 0 = Y0 & ( for n being Nat holds S1[n,N . n,Y . n,N . (n + 1),Y . (n + 1)] ) )
from RECDEF_2:sch 3(A2);
defpred S2[ Nat] means ( N . $1 = min* (Y . $1) & N . $1 in Y . $1 & Y . $1 is infinite & Y . $1 c= NAT );
A4:
S2[ 0 ]
by A1, A3, NAT_1:def 1;
A5:
for i being Nat st S2[i] holds
S2[i + 1]
A9:
for i being Nat holds S2[i]
from NAT_1:sch 2(A4, A5);
A11:
rng N c= X
for i being Nat holds N . i < N . (i + 1)
then
N is increasing
;
hence
ex N being increasing sequence of NAT st rng N c= X
by A11; verum