let R be non empty doubleLoopStr ; :: thesis: ( ( 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
; :: thesis: contradiction
consider I being Ideal of R such that
A3:
not I is finitely_generated
by A2, Def27;
consider e being set such that
A4:
e in I
by XBOOLE_0:def 1;
reconsider e = e as Element of R by A4;
set D = { S where S is Subset of R : S is non empty finite Subset of I } ;
{e} c= I
by A4, ZFMISC_1:37;
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 e' = {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 ;
:: thesis: for x being Element of D ex y being Element of D st S1[n,x,y]let x be
Element of
D;
:: thesis: ex y being Element of D st S1[n,x,y]
x in D
;
then consider x' being
Subset of
R such that A7:
x' = x
and A8:
x' is non
empty finite Subset of
I
;
A9:
I <> x' -Ideal
by A3, A8;
x' -Ideal c= I -Ideal
by A8, Th57;
then
x' -Ideal c= I
by Th44;
then
not
I c= x' -Ideal
by A9, XBOOLE_0:def 10;
then consider r being
set such that A10:
(
r in I & not
r in x' -Ideal )
by TARSKI:def 3;
reconsider x1' =
x' as non
empty finite Subset of
I by A8;
set y =
x1' \/ {r};
A11:
x1' \/ {r} c= I
then
x1' \/ {r} is
Subset of
R
by XBOOLE_1:1;
then
x1' \/ {r} in D
by A11;
then reconsider y =
x1' \/ {r} as
Element of
D ;
take
y
;
:: thesis: S1[n,x,y]
reconsider r =
r as
Element of
R by A10;
take
r
;
:: thesis: ( r in I \ (x -Ideal ) & y = x \/ {r} )
thus
(
r in I \ (x -Ideal ) &
y = x \/ {r} )
by A7, A10, XBOOLE_0:def 5;
:: thesis: verum
end;
consider f being Function of NAT ,D such that
A12:
( f . 0 = e' & ( 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 );
A13:
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
A15:
for x being Element of NAT holds S2[x,F . x]
from FUNCT_2:sch 3(A13);
A16:
for i being Element of NAT holds F . i is Ideal of R
for j, k being Element of NAT st j < k holds
F . j c< F . k
proof
let j,
k be
Element of
NAT ;
:: thesis: ( j < k implies F . j c< F . k )
defpred S3[
Element of
NAT ]
means F . j c< F . ((j + 1) + $1);
A17:
for
i being
Element of
NAT holds
F . i c< F . (i + 1)
proof
let i be
Element of
NAT ;
:: thesis: F . i c< F . (i + 1)
consider c being
Subset of
R such that A18:
c = f . i
and A19:
F . i = c -Ideal
by A15;
c in D
by A18;
then consider c' being
Subset of
R such that A20:
c' = c
and A21:
c' is non
empty finite Subset of
I
;
consider c1 being
Subset of
R such that A22:
c1 = f . (i + 1)
and A23:
F . (i + 1) = c1 -Ideal
by A15;
c1 in D
by A22;
then consider c1' being
Subset of
R such that A24:
c1' = c1
and A25:
c1' is non
empty finite Subset of
I
;
consider r being
Element of
R such that A26:
r in I \ (c -Ideal )
and A27:
c1 = c \/ {r}
by A12, A18, A22;
thus
F . i c= F . (i + 1)
by A19, A20, A21, A23, A27, Th57, XBOOLE_1:7;
:: according to XBOOLE_0:def 8 :: thesis: not F . i = F . (i + 1)
A28:
c1 c= c1 -Ideal
by A24, A25, Def15;
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 A19, A23, A26, A28, XBOOLE_0:def 5;
:: thesis: verum
end;
then A29:
S3[
0 ]
;
A30:
for
i being
Element of
NAT st
S3[
i] holds
S3[
i + 1]
A36:
for
i being
Element of
NAT holds
S3[
i]
from NAT_1:sch 1(A29, A30);
assume
j < k
;
:: thesis: F . j c< F . k
then
j + 1
<= k
by NAT_1:13;
then consider i being
Nat such that A37:
k = (j + 1) + i
by NAT_1:10;
i in NAT
by ORDINAL1:def 13;
hence
F . j c< F . k
by A36, A37;
:: thesis: verum
end;
hence
contradiction
by A1, A16; :: thesis: verum