let R be non empty doubleLoopStr ; ( ( for F being sequence of (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 sequence of (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;
set D = { S where S is Subset of R : S is non empty finite Subset of I } ;
consider e being object 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 Nat
for x being Element of D ex y being Element of D st S1[n,x,y]
proof
let n be
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
object such that A9:
r in I
and A10:
not
r in x9 -Ideal
;
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 sequence of D such that
A13:
( f . 0 = e9 & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) )
from RECDEF_1:sch 2(A6);
defpred S2[ 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 sequence of (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 x being Nat holds S2[x,F . x]
A18:
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[
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 A19:
k = (j + 1) + i
by NAT_1:10;
A20:
for
i being
Nat holds
F . i c< F . (i + 1)
proof
let i be
Nat;
F . i c< F . (i + 1)
consider c being
Subset of
R such that A21:
c = f . i
and A22:
F . i = c -Ideal
by A17;
consider c1 being
Subset of
R such that A23:
c1 = f . (i + 1)
and A24:
F . (i + 1) = c1 -Ideal
by A17;
A25:
c1 c= c1 -Ideal
by Def14;
consider r being
Element of
R such that A26:
r in I \ (c -Ideal)
and A27:
c1 = c \/ {r}
by A13, A21, A23;
c in D
by A21;
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 A22, A24, A27, 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 A27, XBOOLE_0:def 3;
hence
not
F . i = F . (i + 1)
by A22, A24, A26, A25, XBOOLE_0:def 5;
verum
end;
A28:
for
i being
Nat st
S3[
i] holds
S3[
i + 1]
A31:
S3[
0 ]
by A20;
A32:
for
i being
Nat holds
S3[
i]
from NAT_1:sch 2(A31, A28);
thus
F . j c< F . k
by A32, A19;
verum
end;
for i being Element of NAT holds F . i is Ideal of R
hence
contradiction
by A1, A18; verum