let A be non degenerated commutative Ring; :: thesis: for J being proper Ideal of A
for f being Element of A st not f in sqrt J holds
Ideals (A,J,f) has_upper_Zorn_property_wrt RelIncl (Ideals (A,J,f))
let J be proper Ideal of A; :: thesis: for f being Element of A st not f in sqrt J holds
Ideals (A,J,f) has_upper_Zorn_property_wrt RelIncl (Ideals (A,J,f))
let f be Element of A; :: thesis: ( not f in sqrt J implies Ideals (A,J,f) has_upper_Zorn_property_wrt RelIncl (Ideals (A,J,f)) )
assume A1: not f in sqrt J ; :: thesis: Ideals (A,J,f) has_upper_Zorn_property_wrt RelIncl (Ideals (A,J,f))
set S = Ideals (A,J,f);
set P = RelIncl (Ideals (A,J,f));
A2: field (RelIncl (Ideals (A,J,f))) = Ideals (A,J,f) by WELLORD2:def 1;
for Y being set st Y c= Ideals (A,J,f) & (RelIncl (Ideals (A,J,f))) |_2 Y is being_linear-order holds
ex x being set st
( x in Ideals (A,J,f) & ( for y being set st y in Y holds
[y,x] in RelIncl (Ideals (A,J,f)) ) )

proof

let Y be set ; :: thesis: ( Y c= Ideals (A,J,f) & (RelIncl (Ideals (A,J,f))) |_2 Y is being_linear-order implies ex x being set st
( x in Ideals (A,J,f) & ( for y being set st y in Y holds
[y,x] in RelIncl (Ideals (A,J,f)) ) ) )
assume that
A3: Y c= Ideals (A,J,f) and
A4: (RelIncl (Ideals (A,J,f))) |_2 Y is being_linear-order ; :: thesis: ex x being set st
( x in Ideals (A,J,f) & ( for y being set st y in Y holds
[y,x] in RelIncl (Ideals (A,J,f)) ) )

per cases ( Y is empty or not Y is empty ) ;

suppose A5: Y is empty ; :: thesis: ex x being set st
( x in Ideals (A,J,f) & ( for y being set st y in Y holds
[y,x] in RelIncl (Ideals (A,J,f)) ) )

take x = J; :: thesis: ( x in Ideals (A,J,f) & ( for y being set st y in Y holds
[y,x] in RelIncl (Ideals (A,J,f)) ) )
thus ( x in Ideals (A,J,f) & ( for y being set st y in Y holds
[y,x] in RelIncl (Ideals (A,J,f)) ) ) by A5, A1, Th7; :: thesis: verum

end;

suppose not Y is empty ; :: thesis: ex x being set st
( x in Ideals (A,J,f) & ( for y being set st y in Y holds
[y,x] in RelIncl (Ideals (A,J,f)) ) )

then consider e being object such that
A6: e in Y ;
take x = union Y; :: thesis: ( x in Ideals (A,J,f) & ( for y being set st y in Y holds
[y,x] in RelIncl (Ideals (A,J,f)) ) )
for a being object st a in x holds
a in the carrier of A

proof

let a be object ; :: thesis: ( a in x implies a in the carrier of A )
assume a in x ; :: thesis: a in the carrier of A
then consider Z being set such that
A7: a in Z and
A8: Z in Y by TARSKI:def 4;
Z in Ideals (A,J,f) by A3, A8;
then ex A1 being Subset of A st
( Z = A1 & A1 is proper Ideal of A & J c= A1 & A1 /\ (multClSet (J,f)) = {} ) ;
hence a in the carrier of A by A7; :: thesis: verum

end;

then x c= the carrier of A ;
then reconsider B = x as Subset of A ;
A9: B is left-ideal

proof

let p, a be Element of A; :: according to IDEAL_1:def 2 :: thesis: ( not a in B or p * a in B )
assume a in B ; :: thesis: p * a in B
then consider Aa being set such that
A10: a in Aa and
A11: Aa in Y by TARSKI:def 4;
Aa in Ideals (A,J,f) by A3, A11;
then consider Ia being Subset of A such that
A12: Aa = Ia and
A13: Ia is proper Ideal of A and
J c= Ia and
Ia /\ (multClSet (J,f)) = {} ;
( p * a in Ia & Ia c= B ) by A10, A11, A12, A13, IDEAL_1:def 2, ZFMISC_1:74;
hence p * a in B ; :: thesis: verum

end;

A14: B is proper

proof

assume not B is proper ; :: thesis: contradiction
then consider Aa being set such that
A16: 1. A in Aa and
A17: Aa in Y by TARSKI:def 4;
Aa in Ideals (A,J,f) by A3, A17;
then ex Ia being Subset of A st
( Aa = Ia & Ia is proper Ideal of A & J c= Ia & Ia /\ (multClSet (J,f)) = {} ) ;
hence contradiction by A16, IDEAL_1:19; :: thesis: verum

end;

A18: B is add-closed

proof

A19: field ((RelIncl (Ideals (A,J,f))) |_2 Y) = Y by A2, A3, ORDERS_1:71;
let a, b be Element of A; :: according to IDEAL_1:def 1 :: thesis: ( not a in B or not b in B or a + b in B )

A20: now :: thesis: for A1 being Ideal of A st a in A1 & b in A1 & A1 in Y holds
a + b in B

let A1 be Ideal of A; :: thesis: ( a in A1 & b in A1 & A1 in Y implies a + b in B )
assume ( a in A1 & b in A1 ) ; :: thesis: ( A1 in Y implies a + b in B )
then A21: a + b in A1 by IDEAL_1:def 1;
assume A1 in Y ; :: thesis: a + b in B
hence a + b in B by A21, TARSKI:def 4; :: thesis: verum

end;

assume a in B ; :: thesis: ( not b in B or a + b in B )
then consider Aa being set such that
A22: a in Aa and
A23: Aa in Y by TARSKI:def 4;
Aa in Ideals (A,J,f) by A3, A23;
then A24: ex Ia being Subset of A st
( Aa = Ia & Ia is proper Ideal of A & J c= Ia & Ia /\ (multClSet (J,f)) = {} ) ;
assume b in B ; :: thesis: a + b in B
then consider Ab being set such that
A25: b in Ab and
A26: Ab in Y by TARSKI:def 4;
( [Aa,Ab] in (RelIncl (Ideals (A,J,f))) |_2 Y or [Ab,Aa] in (RelIncl (Ideals (A,J,f))) |_2 Y or Aa = Ab ) by A4, A23, A26, A19, RELAT_2:def 6, RELAT_2:def 14;
then ( [Aa,Ab] in RelIncl (Ideals (A,J,f)) or [Ab,Aa] in RelIncl (Ideals (A,J,f)) or Aa = Ab ) by XBOOLE_0:def 4;
then A27: ( Aa c= Ab or Ab c= Aa ) by A3, A23, A26, WELLORD2:def 1;
Ab in Ideals (A,J,f) by A3, A26;
then ex Ib being Subset of A st
( Ab = Ib & Ib is proper Ideal of A & J c= Ib & Ib /\ (multClSet (J,f)) = {} ) ;
hence a + b in B by A22, A23, A25, A26, A20, A24, A27; :: thesis: verum

end;

e in Ideals (A,J,f) by A3, A6;
then consider A1 being Subset of A such that
A28: A1 = e and
A29: A1 is proper Ideal of A and
A30: J c= A1 and
A1 /\ (multClSet (J,f)) = {} ;
ex q being object st q in A1 by XBOOLE_0:def 1, A29;
then A32: ( not B is empty & J c= B ) by A6, A28, A30, TARSKI:def 4;
A33: B /\ (multClSet (J,f)) = {}

proof

assume B /\ (multClSet (J,f)) <> {} ; :: thesis: contradiction
then consider y being object such that
A35: y in B /\ (multClSet (J,f)) by XBOOLE_0:def 1;
( y in B & y in multClSet (J,f) ) by A35, XBOOLE_0:def 4;
then consider Aa being set such that
A36: y in Aa and
A37: Aa in Y by TARSKI:def 4;
Aa in Ideals (A,J,f) by A3, A37;
then consider Ia being Subset of A such that
A38: Aa = Ia and
( Ia is proper Ideal of A & J c= Ia ) and
A39: Ia /\ (multClSet (J,f)) = {} ;
y in multClSet (J,f) by A35, XBOOLE_0:def 4;
hence contradiction by A39, A38, A36, XBOOLE_0:def 4; :: thesis: verum

end;

thus A41: x in Ideals (A,J,f) by A9, A14, A18, A32, A33; :: thesis: for y being set st y in Y holds
[y,x] in RelIncl (Ideals (A,J,f))
let y be set ; :: thesis: ( y in Y implies [y,x] in RelIncl (Ideals (A,J,f)) )
assume A42: y in Y ; :: thesis: [y,x] in RelIncl (Ideals (A,J,f))
then y c= x by ZFMISC_1:74;
hence [y,x] in RelIncl (Ideals (A,J,f)) by A3, A41, A42, WELLORD2:def 1; :: thesis: verum

end;

end;

end;

hence Ideals (A,J,f) has_upper_Zorn_property_wrt RelIncl (Ideals (A,J,f)) ; :: thesis: verum