set S = { A where A is Ideal of R : ( I c= A & A is proper ) } ;
set P = RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } ;
A2: field (RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } ) = { A where A is Ideal of R : ( I c= A & A is proper ) } by WELLORD2:def 1;
A3: { A where A is Ideal of R : ( I c= A & A is proper ) } has_upper_Zorn_property_wrt RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) }
proof
let Y be set ; :: according to ORDERS_1:def 10 :: thesis: ( not Y c= { A where A is Ideal of R : ( I c= A & A is proper ) } or not (RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } ) |_2 Y is being_linear-order or ex b1 being set st
( b1 in { A where A is Ideal of R : ( I c= A & A is proper ) } & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } ) ) ) )
assume that
A4: Y c= { A where A is Ideal of R : ( I c= A & A is proper ) } and
A5: (RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } ) |_2 Y is being_linear-order ; :: thesis: ex b1 being set st
( b1 in { A where A is Ideal of R : ( I c= A & A is proper ) } & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } ) ) )
per cases ( Y is empty or not Y is empty ) ;
suppose A6: Y is empty ; :: thesis: ex b1 being set st
( b1 in { A where A is Ideal of R : ( I c= A & A is proper ) } & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } ) ) )
take x = I; :: thesis: ( x in { A where A is Ideal of R : ( I c= A & A is proper ) } & ( for b1 being set holds
( not b1 in Y or [b1,x] in RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } ) ) )
thus x in { A where A is Ideal of R : ( I c= A & A is proper ) } ; :: thesis: for b1 being set holds
( not b1 in Y or [b1,x] in RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } )
thus for b1 being set holds
( not b1 in Y or [b1,x] in RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } ) by A6; :: thesis: verum
end;
suppose H: not Y is empty ; :: thesis: ex b1 being set st
( b1 in { A where A is Ideal of R : ( I c= A & A is proper ) } & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } ) ) )
set e = the Element of Y;
take x = union Y; :: thesis: ( x in { A where A is Ideal of R : ( I c= A & A is proper ) } & ( for b1 being set holds
( not b1 in Y or [b1,x] in RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } ) ) )
x c= the carrier of R
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in x or a in the carrier of R )
assume a in x ; :: thesis: a in the carrier of R
then consider Z being set such that
A9: a in Z and
A10: Z in Y by TARSKI:def 4;
Z in { A where A is Ideal of R : ( I c= A & A is proper ) } by A4, A10;
then ex A being Ideal of R st
( Z = A & I c= A & A is proper ) ;
hence a in the carrier of R by A9; :: thesis: verum
end;
then reconsider B = x as Subset of R ;
A11: B is right-ideal
proof
let p, a be Element of R; :: according to IDEAL_1:def 3 :: thesis: ( not a in B or a * p in B )
assume a in B ; :: thesis: a * p in B
then consider Aa being set such that
A12: a in Aa and
A13: Aa in Y by TARSKI:def 4;
Aa in { A where A is Ideal of R : ( I c= A & A is proper ) } by A4, A13;
then consider Ia being Ideal of R such that
A14: Aa = Ia and
( I c= Ia & Ia is proper ) ;
( a * p in Ia & Ia c= B ) by A12, A13, A14, IDEAL_1:def 3, ZFMISC_1:74;
hence a * p in B ; :: thesis: verum
end;
A15: B is left-ideal
proof
let p, a be Element of R; :: 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
A16: a in Aa and
A17: Aa in Y by TARSKI:def 4;
Aa in { A where A is Ideal of R : ( I c= A & A is proper ) } by A4, A17;
then consider Ia being Ideal of R such that
A18: Aa = Ia and
( I c= Ia & Ia is proper ) ;
( p * a in Ia & Ia c= B ) by A16, A17, A18, IDEAL_1:def 2, ZFMISC_1:74;
hence p * a in B ; :: thesis: verum
end;
A19: now :: thesis: B is proper
assume not B is proper ; :: thesis: contradiction
then 1. R in B by A15, IDEAL_1:19;
then consider Aa being set such that
A20: 1. R in Aa and
A21: Aa in Y by TARSKI:def 4;
Aa in { A where A is Ideal of R : ( I c= A & A is proper ) } by A4, A21;
then ex Ia being Ideal of R st
( Aa = Ia & I c= Ia & Ia is proper ) ;
hence contradiction by A20, IDEAL_1:19; :: thesis: verum
end;
A22: B is add-closed
proof
A23: field ((RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } ) |_2 Y) = Y by A2, A4, ORDERS_1:71;
let a, b be Element of R; :: according to IDEAL_1:def 1 :: thesis: ( not a in B or not b in B or a + b in B )
A24: now :: thesis: for A being Ideal of R st a in A & b in A & A in Y holds
a + b in B
let A be Ideal of R; :: thesis: ( a in A & b in A & A in Y implies a + b in B )
assume ( a in A & b in A ) ; :: thesis: ( A in Y implies a + b in B )
then A25: a + b in A by IDEAL_1:def 1;
assume A in Y ; :: thesis: a + b in B
hence a + b in B by A25, 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
A26: a in Aa and
A27: Aa in Y by TARSKI:def 4;
Aa in { A where A is Ideal of R : ( I c= A & A is proper ) } by A4, A27;
then A28: ex Ia being Ideal of R st
( Aa = Ia & I c= Ia & Ia is proper ) ;
assume b in B ; :: thesis: a + b in B
then consider Ab being set such that
A29: b in Ab and
A30: Ab in Y by TARSKI:def 4;
( [Aa,Ab] in (RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } ) |_2 Y or [Ab,Aa] in (RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } ) |_2 Y or Aa = Ab ) by A27, A30, A23, A5, RELAT_2:def 14, RELAT_2:def 6;
then ( [Aa,Ab] in RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } or [Ab,Aa] in RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } or Aa = Ab ) by XBOOLE_0:def 4;
then A31: ( Aa c= Ab or Ab c= Aa ) by A4, A27, A30, WELLORD2:def 1;
Ab in { A where A is Ideal of R : ( I c= A & A is proper ) } by A4, A30;
then ex Ib being Ideal of R st
( Ab = Ib & I c= Ib & Ib is proper ) ;
hence a + b in B by A26, A27, A29, A30, A24, A28, A31; :: thesis: verum
end;
A40: I c= x
proof
now :: thesis: for o being object st o in I holds
o in x
let o be object ; :: thesis: ( o in I implies o in x )
assume H1: o in I ; :: thesis: o in x
the Element of Y in { A where A is Ideal of R : ( I c= A & A is proper ) } by A4, H;
then consider A being Ideal of R such that
K: ( the Element of Y = A & I c= A & A is proper ) ;
thus o in x by K, H1, H, TARSKI:def 4; :: thesis: verum
end;
hence I c= x ; :: thesis: verum
end;
the Element of Y in { A where A is Ideal of R : ( I c= A & A is proper ) } by A4, H;
then consider A being Ideal of R such that
A32: the Element of Y = A and
( I c= A & A is proper ) ;
ex q being object st q in A by XBOOLE_0:def 1;
then not B is empty by H, A32, TARSKI:def 4;
hence A33: x in { A where A is Ideal of R : ( I c= A & A is proper ) } by A22, A11, A19, A40; :: thesis: for b1 being set holds
( not b1 in Y or [b1,x] in RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } )
let y be set ; :: thesis: ( not y in Y or [y,x] in RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } )
assume A34: y in Y ; :: thesis: [y,x] in RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) }
then y c= x by ZFMISC_1:74;
hence [y,x] in RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } by A4, A33, A34, WELLORD2:def 1; :: thesis: verum
end;
end;
end;
RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } partially_orders { A where A is Ideal of R : ( I c= A & A is proper ) } by WELLORD2:21, WELLORD2:19, WELLORD2:20;
then consider x being set such that
A4: x is_maximal_in RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } by A2, A3, ORDERS_1:63;
consider H being Ideal of R such that
A6: x = H and
A7: ( I c= H & H is proper ) by A2, A4;
take H ; :: thesis: ( I c= H & H is maximal )
thus I c= H by A7; :: thesis: H is maximal
now :: thesis: for J being Ideal of R holds
( not H c= J or J = H or not J is proper )
let J be Ideal of R; :: thesis: ( not H c= J or J = H or not J is proper )
assume A10: H c= J ; :: thesis: ( J = H or not J is proper )
then A8: I c= J by A7;
now :: thesis: ( J is proper implies H = J )
assume J is proper ; :: thesis: H = J
then A9: J in { A where A is Ideal of R : ( I c= A & A is proper ) } by A8;
then [H,J] in RelIncl { A where A is Ideal of R : ( I c= A & A is proper ) } by A10, A2, A4, A6, WELLORD2:def 1;
hence H = J by A2, A4, A6, A9; :: thesis: verum
end;
hence ( J = H or not J is proper ) ; :: thesis: verum
end;
then H is quasi-maximal by RING_1:def 3;
hence H is maximal by A7; :: thesis: verum