let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N holds
( S is weakly_standard iff ex f being sequence of NAT st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) ) ) )
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: ( S is weakly_standard iff ex f being sequence of NAT st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) ) ) )
hereby :: thesis: ( ex f being sequence of NAT st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) ) ) implies S is weakly_standard )
assume S is weakly_standard ; :: thesis: ex f being sequence of NAT st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) ) )
then consider f being sequence of NAT such that
A1: f is bijective and
A2: for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ;
thus ex f being sequence of NAT st
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) ) ) :: thesis: verum
proof
take f ; :: thesis: ( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) ) )
thus f is bijective by A1; :: thesis: for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) )
thus for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) by A1, A2, Th3; :: thesis: verum
end;
end;
given f being sequence of NAT such that A3: f is bijective and
A4: for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) ; :: thesis: S is weakly_standard
take f ; :: according to AMI_WSTD:def 3 :: thesis: ( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) )
thus f is bijective by A3; :: thesis: for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S )
thus for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) by A3, A4, Th3; :: thesis: verum