let R be non empty doubleLoopStr ; ( ( for F being Function of NAT,(bool the carrier of R) holds
( ex i being Element of NAT st F . i is not Ideal of R or ex j, k being Element of NAT st
( j < k & not F . j c< F . k ) ) ) implies R is Noetherian )
assume that
A1:
for F being Function of NAT,(bool the carrier of R) holds
( ex i being Element of NAT st F . i is not Ideal of R or ex j, k being Element of NAT st
( j < k & not F . j c< F . k ) )
and
A2:
not R is Noetherian
; contradiction
consider I being Ideal of R such that
A3:
not I is finitely_generated
by A2, Def27;
set D = { S where S is Subset of R : S is non empty finite Subset of I } ;
consider e being set such that
A4:
e in I
by XBOOLE_0:def 1;
reconsider e = e as Element of R by A4;
{e} c= I
by A4, ZFMISC_1:31;
then A5:
{e} in { S where S is Subset of R : S is non empty finite Subset of I }
;
{ S where S is Subset of R : S is non empty finite Subset of I } c= bool the carrier of R
then reconsider D = { S where S is Subset of R : S is non empty finite Subset of I } as non empty Subset-Family of R by A5;
reconsider e9 = {e} as Element of D by A5;
defpred S1[ set , Element of D, set ] means ex r being Element of R st
( r in I \ ($2 -Ideal) & $3 = $2 \/ {r} );
A6:
for n being Element of NAT
for x being Element of D ex y being Element of D st S1[n,x,y]
proof
let n be
Element of
NAT ;
for x being Element of D ex y being Element of D st S1[n,x,y]let x be
Element of
D;
ex y being Element of D st S1[n,x,y]
x in D
;
then consider x9 being
Subset of
R such that A7:
x9 = x
and A8:
x9 is non
empty finite Subset of
I
;
reconsider x19 =
x9 as non
empty finite Subset of
I by A8;
x9 -Ideal c= I -Ideal
by A8, Th57;
then
x9 -Ideal c= I
by Th44;
then
not
I c= x9 -Ideal
by A3, A8, XBOOLE_0:def 10;
then consider r being
set such that A9:
r in I
and A10:
not
r in x9 -Ideal
by TARSKI:def 3;
set y =
x19 \/ {r};
A11:
x19 \/ {r} c= I
then
x19 \/ {r} is
Subset of
R
by XBOOLE_1:1;
then A12:
x19 \/ {r} in D
by A11;
reconsider r =
r as
Element of
R by A9;
reconsider y =
x19 \/ {r} as
Element of
D by A12;
take
y
;
S1[n,x,y]
take
r
;
( r in I \ (x -Ideal) & y = x \/ {r} )
thus
(
r in I \ (x -Ideal) &
y = x \/ {r} )
by A7, A9, A10, XBOOLE_0:def 5;
verum
end;
consider f being Function of NAT,D such that
A13:
( f . 0 = e9 & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) )
from RECDEF_1:sch 2(A6);
defpred S2[ Element of NAT , Subset of R] means ex c being Subset of R st
( c = f . $1 & $2 = c -Ideal );
A14:
for x being Element of NAT ex y being Subset of R st S2[x,y]
consider F being Function of NAT,(bool the carrier of R) such that
A16:
for x being Element of NAT holds S2[x,F . x]
from FUNCT_2:sch 3(A14);
A17:
for j, k being Element of NAT st j < k holds
F . j c< F . k
proof
let j,
k be
Element of
NAT ;
( j < k implies F . j c< F . k )
defpred S3[
Element of
NAT ]
means F . j c< F . ((j + 1) + $1);
assume
j < k
;
F . j c< F . k
then
j + 1
<= k
by NAT_1:13;
then consider i being
Nat such that A18:
k = (j + 1) + i
by NAT_1:10;
A19:
for
i being
Element of
NAT holds
F . i c< F . (i + 1)
proof
let i be
Element of
NAT ;
F . i c< F . (i + 1)
consider c being
Subset of
R such that A20:
c = f . i
and A21:
F . i = c -Ideal
by A16;
consider c1 being
Subset of
R such that A22:
c1 = f . (i + 1)
and A23:
F . (i + 1) = c1 -Ideal
by A16;
c1 in D
by A22;
then
ex
c19 being
Subset of
R st
(
c19 = c1 &
c19 is non
empty finite Subset of
I )
;
then A24:
c1 c= c1 -Ideal
by Def15;
consider r being
Element of
R such that A25:
r in I \ (c -Ideal)
and A26:
c1 = c \/ {r}
by A13, A20, A22;
c in D
by A20;
then
ex
c9 being
Subset of
R st
(
c9 = c &
c9 is non
empty finite Subset of
I )
;
hence
F . i c= F . (i + 1)
by A21, A23, A26, Th57, XBOOLE_1:7;
XBOOLE_0:def 8 not F . i = F . (i + 1)
r in {r}
by TARSKI:def 1;
then
r in c1
by A26, XBOOLE_0:def 3;
hence
not
F . i = F . (i + 1)
by A21, A23, A25, A24, XBOOLE_0:def 5;
verum
end;
A27:
for
i being
Element of
NAT st
S3[
i] holds
S3[
i + 1]
A30:
S3[
0 ]
by A19;
A31:
for
i being
Element of
NAT holds
S3[
i]
from NAT_1:sch 1(A30, A27);
i in NAT
by ORDINAL1:def 12;
hence
F . j c< F . k
by A31, A18;
verum
end;
for i being Element of NAT holds F . i is Ideal of R
hence
contradiction
by A1, A17; verum