let F be preordered Field; :: thesis: for P being Preordering of F ex Q being Preordering of F st
( P c= Q & Q is maximal )
let P be Preordering of F; :: thesis: ex Q being Preordering of F st
( P c= Q & Q is maximal )
set S = { O where O is Preordering of F : P c= O } ;
set R = RelIncl { O where O is Preordering of F : P c= O } ;
A2: ( field (RelIncl { O where O is Preordering of F : P c= O } ) = { O where O is Preordering of F : P c= O } & ( for Y, Z being set st Y in { O where O is Preordering of F : P c= O } & Z in { O where O is Preordering of F : P c= O } holds
( [Y,Z] in RelIncl { O where O is Preordering of F : P c= O } iff Y c= Z ) ) ) by WELLORD2:def 1;
A3: { O where O is Preordering of F : P c= O } has_upper_Zorn_property_wrt RelIncl { O where O is Preordering of F : P c= O }
proof
now :: thesis: for Y being set st Y c= { O where O is Preordering of F : P c= O } & (RelIncl { O where O is Preordering of F : P c= O } ) |_2 Y is being_linear-order holds
ex x being set st
( x in { O where O is Preordering of F : P c= O } & ( for y being set st y in Y holds
[y,x] in RelIncl { O where O is Preordering of F : P c= O } ) )
let Y be set ; :: thesis: ( Y c= { O where O is Preordering of F : P c= O } & (RelIncl { O where O is Preordering of F : P c= O } ) |_2 Y is being_linear-order implies ex x being set st
( b2 in { b3 where O is Preordering of F : P c= b3 } & ( for y being set st b3 in x holds
[b3,y] in RelIncl { b4 where O is Preordering of F : P c= b4 } ) ) )
assume AS: ( Y c= { O where O is Preordering of F : P c= O } & (RelIncl { O where O is Preordering of F : P c= O } ) |_2 Y is being_linear-order ) ; :: thesis: ex x being set st
( b2 in { b3 where O is Preordering of F : P c= b3 } & ( for y being set st b3 in x holds
[b3,y] in RelIncl { b4 where O is Preordering of F : P c= b4 } ) )
H1: now :: thesis: for z being set st z in { O where O is Preordering of F : P c= O } holds
( P c= z & z is Preordering of F )
let z be set ; :: thesis: ( z in { O where O is Preordering of F : P c= O } implies ( P c= z & z is Preordering of F ) )
assume z in { O where O is Preordering of F : P c= O } ; :: thesis: ( P c= z & z is Preordering of F )
then consider p being Preordering of F such that
H: ( z = p & P c= p ) ;
thus ( P c= z & z is Preordering of F ) by H; :: thesis: verum
end;
H2: ( P in { O where O is Preordering of F : P c= O } & (RelIncl { O where O is Preordering of F : P c= O } ) |_2 Y = (RelIncl { O where O is Preordering of F : P c= O } ) /\ [:Y,Y:] ) ;
H3: (RelIncl { O where O is Preordering of F : P c= O } ) |_2 Y is connected by AS, ORDERS_1:def 6;
H5: now :: thesis: for z1, z2 being set st z1 in Y & z2 in Y & not z1 c= z2 holds
z2 c= z1
let z1, z2 be set ; :: thesis: ( z1 in Y & z2 in Y & not b1 c= b2 implies b2 c= b1 )
assume HH0: ( z1 in Y & z2 in Y ) ; :: thesis: ( b1 c= b2 or b2 c= b1 )
per cases ( z1 = z2 or z1 <> z2 ) ;
suppose z1 = z2 ; :: thesis: ( b1 c= b2 or b2 c= b1 )
hence ( z1 c= z2 or z2 c= z1 ) ; :: thesis: verum
end;
suppose HH1: z1 <> z2 ; :: thesis: ( b1 c= b2 or b2 c= b1 )
( z1 in field ((RelIncl { O where O is Preordering of F : P c= O } ) |_2 Y) & z2 in field ((RelIncl { O where O is Preordering of F : P c= O } ) |_2 Y) ) by HH0, A2, AS, ORDERS_1:71;
then ( [z1,z2] in (RelIncl { O where O is Preordering of F : P c= O } ) |_2 Y or [z2,z1] in (RelIncl { O where O is Preordering of F : P c= O } ) |_2 Y ) by H3, HH1, RELAT_2:def 6, RELAT_2:def 14;
then ( [z1,z2] in RelIncl { O where O is Preordering of F : P c= O } or [z2,z1] in RelIncl { O where O is Preordering of F : P c= O } ) by XBOOLE_0:def 4;
hence ( z1 c= z2 or z2 c= z1 ) by HH0, AS, WELLORD2:def 1; :: thesis: verum
end;
end;
end;
set M = union Y;
per cases ( Y = {} or Y <> {} ) ;
suppose Y = {} ; :: thesis: ex x being set st
( b2 in { b3 where O is Preordering of F : P c= b3 } & ( for y being set st b3 in x holds
[b3,y] in RelIncl { b4 where O is Preordering of F : P c= b4 } ) )
then for y being set st y in Y holds
[y,P] in RelIncl { O where O is Preordering of F : P c= O } ;
hence ex x being set st
( x in { O where O is Preordering of F : P c= O } & ( for y being set st y in Y holds
[y,x] in RelIncl { O where O is Preordering of F : P c= O } ) ) by H2; :: thesis: verum
end;
suppose H: Y <> {} ; :: thesis: ex x being set st
( b2 in { b3 where O is Preordering of F : P c= b3 } & ( for y being set st b3 in x holds
[b3,y] in RelIncl { b4 where O is Preordering of F : P c= b4 } ) )
A7: union Y c= the carrier of F
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in union Y or o in the carrier of F )
assume o in union Y ; :: thesis: o in the carrier of F
then consider s being set such that
H: ( o in s & s in Y ) by TARSKI:def 4;
s is Preordering of F by H1, H, AS;
hence o in the carrier of F by H; :: thesis: verum
end;
A8a: ex s being set st
( 0. F in s & s in Y )
proof
set s = the Element of Y;
the Element of Y in Y by H;
then the Element of Y is Preordering of F by AS, H1;
hence ex s being set st
( 0. F in s & s in Y ) by H, REALALG1:25; :: thesis: verum
end;
then A8: 0. F in union Y by TARSKI:def 4;
reconsider M = union Y as non empty Subset of F by A7, A8a, TARSKI:def 4;
A6: M is Preordering of F
proof
A10: M + M c= M
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in M + M or o in M )
assume o in M + M ; :: thesis: o in M
then consider a, b being Element of F such that
A11: ( o = a + b & a in M & b in M ) ;
consider sa being set such that
A12: ( a in sa & sa in Y ) by A11, TARSKI:def 4;
consider sb being set such that
A13: ( b in sb & sb in Y ) by A11, TARSKI:def 4;
reconsider sa = sa, sb = sb as Preordering of F by A12, A13, AS, H1;
A16: ( sa + sa c= sa & sb + sb c= sb ) by REALALG1:def 14;
per cases ( sa c= sb or sb c= sa ) by A12, A13, H5;
suppose sa c= sb ; :: thesis: o in M
then a + b in sb + sb by A12, A13;
hence o in M by A16, A11, A13, TARSKI:def 4; :: thesis: verum
end;
suppose sb c= sa ; :: thesis: o in M
then a + b in sa + sa by A12, A13;
hence o in M by A16, A11, A12, TARSKI:def 4; :: thesis: verum
end;
end;
end;
A11: M * M c= M
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in M * M or o in M )
assume o in M * M ; :: thesis: o in M
then consider a, b being Element of F such that
A11: ( o = a * b & a in M & b in M ) ;
consider sa being set such that
A12: ( a in sa & sa in Y ) by A11, TARSKI:def 4;
consider sb being set such that
A13: ( b in sb & sb in Y ) by A11, TARSKI:def 4;
reconsider sa = sa, sb = sb as Preordering of F by A12, A13, AS, H1;
A16: ( sa * sa c= sa & sb * sb c= sb ) by REALALG1:def 14;
per cases ( sa c= sb or sb c= sa ) by A12, A13, H5;
suppose sa c= sb ; :: thesis: o in M
then a * b in sb * sb by A12, A13;
hence o in M by A11, A13, A16, TARSKI:def 4; :: thesis: verum
end;
suppose sb c= sa ; :: thesis: o in M
then a * b in sa * sa by A12, A13;
hence o in M by A16, A11, A12, TARSKI:def 4; :: thesis: verum
end;
end;
end;
A12: M /\ (- M) = {(0. F)}
proof
A13: now :: thesis: for o being object st o in {(0. F)} holds
o in M /\ (- M)
let o be object ; :: thesis: ( o in {(0. F)} implies o in M /\ (- M) )
assume o in {(0. F)} ; :: thesis: o in M /\ (- M)
then A14: o = - (0. F) by TARSKI:def 1;
then o in - M by A8;
hence o in M /\ (- M) by A14, A8; :: thesis: verum
end;
now :: thesis: for o being object st o in M /\ (- M) holds
o in {(0. F)}
let o be object ; :: thesis: ( o in M /\ (- M) implies b1 in {(0. F)} )
assume A14: o in M /\ (- M) ; :: thesis: b1 in {(0. F)}
then A14a: ( o in M & o in - M ) by XBOOLE_0:def 4;
then consider so being set such that
A15: ( o in so & so in Y ) by TARSKI:def 4;
consider p being Element of F such that
A16: ( o = - p & p in M ) by A14a;
consider sp being set such that
A17: ( p in sp & sp in Y ) by A16, TARSKI:def 4;
reconsider so = so, sp = sp as Preordering of F by AS, A15, A17, H1;
reconsider o1 = o as Element of F by A14;
per cases ( so c= sp or sp c= so ) by A15, A17, H5;
suppose A19: so c= sp ; :: thesis: b1 in {(0. F)}
o in - sp by A16, A17;
then o in sp /\ (- sp) by A19, A15;
hence o in {(0. F)} by REALALG1:def 14; :: thesis: verum
end;
suppose sp c= so ; :: thesis: b1 in {(0. F)}
then o in - so by A16, A17;
then o in so /\ (- so) by A15;
hence o in {(0. F)} by REALALG1:def 7; :: thesis: verum
end;
end;
end;
hence M /\ (- M) = {(0. F)} by A13, TARSKI:2; :: thesis: verum
end;
SQ F c= M
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in SQ F or o in M )
assume A13: o in SQ F ; :: thesis: o in M
set s = the Element of Y;
the Element of Y in Y by H;
then A15: P c= the Element of Y by H1, AS;
SQ F c= P by REALALG1:def 14;
then o in the Element of Y by A13, A15;
hence o in M by H, TARSKI:def 4; :: thesis: verum
end;
hence M is Preordering of F by A10, A11, A12, REALALG1:def 14; :: thesis: verum
end;
P c= M
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in P or o in M )
assume H0: o in P ; :: thesis: o in M
set s = the Element of Y;
the Element of Y in Y by H;
then P c= the Element of Y by H1, AS;
hence o in M by H0, H, TARSKI:def 4; :: thesis: verum
end;
then A4: M in { O where O is Preordering of F : P c= O } by A6;
now :: thesis: for y being set st y in Y holds
[y,M] in RelIncl { O where O is Preordering of F : P c= O }
let y be set ; :: thesis: ( y in Y implies [y,M] in RelIncl { O where O is Preordering of F : P c= O } )
assume A5: y in Y ; :: thesis: [y,M] in RelIncl { O where O is Preordering of F : P c= O }
then y c= M by TARSKI:def 4;
hence [y,M] in RelIncl { O where O is Preordering of F : P c= O } by AS, A4, A5, WELLORD2:def 1; :: thesis: verum
end;
hence ex x being set st
( x in { O where O is Preordering of F : P c= O } & ( for y being set st y in Y holds
[y,x] in RelIncl { O where O is Preordering of F : P c= O } ) ) by A4; :: thesis: verum
end;
end;
end;
hence { O where O is Preordering of F : P c= O } has_upper_Zorn_property_wrt RelIncl { O where O is Preordering of F : P c= O } by ORDERS_1:def 10; :: thesis: verum
end;
( RelIncl { O where O is Preordering of F : P c= O } is_reflexive_in { O where O is Preordering of F : P c= O } & RelIncl { O where O is Preordering of F : P c= O } is_transitive_in { O where O is Preordering of F : P c= O } ) by WELLORD2:19, WELLORD2:20;
then RelIncl { O where O is Preordering of F : P c= O } partially_orders { O where O is Preordering of F : P c= O } by WELLORD2:21, ORDERS_1:def 8;
then consider x being set such that
M: x is_maximal_in RelIncl { O where O is Preordering of F : P c= O } by A2, A3, ORDERS_1:63;
x in field (RelIncl { O where O is Preordering of F : P c= O } ) by M, ORDERS_1:def 12;
then consider O being Preordering of F such that
M1: ( x = O & P c= O ) by A2;
M4: O in { O where O is Preordering of F : P c= O } by M1;
now :: thesis: for Q being Preordering of F st O c= Q holds
O = Q
let Q be Preordering of F; :: thesis: ( O c= Q implies O = Q )
assume M2: O c= Q ; :: thesis: O = Q
then P c= Q by M1;
then M5: Q in { O where O is Preordering of F : P c= O } ;
then M3: Q in field (RelIncl { O where O is Preordering of F : P c= O } ) by WELLORD2:def 1;
[O,Q] in RelIncl { O where O is Preordering of F : P c= O } by M4, M2, M5, WELLORD2:def 1;
hence O = Q by M3, M1, M, ORDERS_1:def 12; :: thesis: verum
end;
hence ex Q being Preordering of F st
( P c= Q & Q is maximal ) by M1, defmax; :: thesis: verum