let R be Relation; :: thesis: for X being set st R partially_orders X & field R = X holds
ex P being Relation st
( R c= P & P linearly_orders X & field P = X )
let X be set ; :: thesis: ( R partially_orders X & field R = X implies ex P being Relation st
( R c= P & P linearly_orders X & field P = X ) )
assume that
A1: R partially_orders X and
A2: field R = X ; :: thesis: ex P being Relation st
( R c= P & P linearly_orders X & field P = X )
defpred S1[ set ] means ex P being Relation st
( $1 = P & R c= P & P partially_orders X & field P = X );
consider Rel being set such that
A3: for x being set holds
( x in Rel iff ( x in bool [:X,X:] & S1[x] ) ) from XBOOLE_0:sch 1();
 A4: for Z being set st Z <> {} & Z c= Rel & Z is c=-linear holds
union Z in Rel
proof
reconsider T = [:X,X:] as Relation ;
let Z be set ; :: thesis: ( Z <> {} & Z c= Rel & Z is c=-linear implies union Z in Rel )
assume that
A5: Z <> {} and
A6: Z c= Rel and
A7: Z is c=-linear ; :: thesis: union Z in Rel
A8: union (bool [:X,X:]) = T by ZFMISC_1:81;
Z c= bool [:X,X:]
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Z or x in bool [:X,X:] )
assume x in Z ; :: thesis: x in bool [:X,X:]
hence x in bool [:X,X:] by A3, A6; :: thesis: verum
end;
then A9: union Z c= union (bool [:X,X:]) by ZFMISC_1:77;
then reconsider S = union Z as Relation ;
set y = the Element of Z;
the Element of Z in Rel by A5, A6, TARSKI:def 3;
then consider P being Relation such that
A10: the Element of Z = P and
A11: R c= P and
A12: P partially_orders X and
field P = X by A3;
A13: S is_antisymmetric_in X
proof
let x be set ; :: according to RELAT_2:def 4 :: thesis: for b1 being set holds
( not x in X or not b1 in X or not [x,b1] in S or not [b1,x] in S or x = b1 )
let y be set ; :: thesis: ( not x in X or not y in X or not [x,y] in S or not [y,x] in S or x = y )
assume that
A14: x in X and
A15: y in X and
A16: [x,y] in S and
A17: [y,x] in S ; :: thesis: x = y
consider X1 being set such that
A18: [x,y] in X1 and
A19: X1 in Z by A16, TARSKI:def 4;
consider P1 being Relation such that
A20: X1 = P1 and
R c= P1 and
A21: P1 partially_orders X and
field P1 = X by A3, A6, A19;
consider X2 being set such that
A22: [y,x] in X2 and
A23: X2 in Z by A17, TARSKI:def 4;
X1,X2 are_c=-comparable by A7, A19, A23, ORDINAL1:def 8;
then A24: ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def 9;
consider P2 being Relation such that
A25: X2 = P2 and
R c= P2 and
A26: P2 partially_orders X and
field P2 = X by A3, A6, A23;
A27: P2 is_antisymmetric_in X by A26, Def7;
P1 is_antisymmetric_in X by A21, Def7;
hence x = y by A14, A15, A18, A22, A24, A20, A25, A27, RELAT_2:def 4; :: thesis: verum
end;
A28: S is_transitive_in X
proof
let x be set ; :: according to RELAT_2:def 8 :: thesis: for b1, b2 being set holds
( not x in X or not b1 in X or not b2 in X or not [x,b1] in S or not [b1,b2] in S or [x,b2] in S )
let y, z be set ; :: thesis: ( not x in X or not y in X or not z in X or not [x,y] in S or not [y,z] in S or [x,z] in S )
assume that
A29: x in X and
A30: y in X and
A31: z in X and
A32: [x,y] in S and
A33: [y,z] in S ; :: thesis: [x,z] in S
consider X1 being set such that
A34: [x,y] in X1 and
A35: X1 in Z by A32, TARSKI:def 4;
consider P1 being Relation such that
A36: X1 = P1 and
R c= P1 and
A37: P1 partially_orders X and
field P1 = X by A3, A6, A35;
consider X2 being set such that
A38: [y,z] in X2 and
A39: X2 in Z by A33, TARSKI:def 4;
X1,X2 are_c=-comparable by A7, A35, A39, ORDINAL1:def 8;
then A40: ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def 9;
consider P2 being Relation such that
A41: X2 = P2 and
R c= P2 and
A42: P2 partially_orders X and
field P2 = X by A3, A6, A39;
A43: P2 is_transitive_in X by A42, Def7;
P1 is_transitive_in X by A37, Def7;
then ( [x,z] in P1 or [x,z] in P2 ) by A29, A30, A31, A34, A38, A40, A36, A41, A43, RELAT_2:def 8;
hence [x,z] in S by A35, A39, A36, A41, TARSKI:def 4; :: thesis: verum
end;
A44: P is_reflexive_in X by A12, Def7;
S is_reflexive_in X
proof
let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in X or [x,x] in S )
assume x in X ; :: thesis: [x,x] in S
then [x,x] in P by A44, RELAT_2:def 1;
hence [x,x] in S by A5, A10, TARSKI:def 4; :: thesis: verum
end;
then A45: S partially_orders X by A28, A13, Def7;
A46: field S c= X
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in field S or x in X )
A47: now
assume x in dom S ; :: thesis: ( not x in field S or x in X )
then consider y being set such that
A48: [x,y] in S by RELAT_1:def 4;
consider Y being set such that
A49: [x,y] in Y and
A50: Y in Z by A48, TARSKI:def 4;
ex P being Relation st
( Y = P & R c= P & P partially_orders X & field P = X ) by A3, A6, A50;
hence ( not x in field S or x in X ) by A49, RELAT_1:15; :: thesis: verum
end;
A51: now
assume x in rng S ; :: thesis: ( not x in field S or x in X )
then consider y being set such that
A52: [y,x] in S by RELAT_1:def 5;
consider Y being set such that
A53: [y,x] in Y and
A54: Y in Z by A52, TARSKI:def 4;
ex P being Relation st
( Y = P & R c= P & P partially_orders X & field P = X ) by A3, A6, A54;
hence ( not x in field S or x in X ) by A53, RELAT_1:15; :: thesis: verum
end;
assume x in field S ; :: thesis: x in X
hence x in X by A47, A51, XBOOLE_0:def 3; :: thesis: verum
end;
A55: R c= S
proof
let x be set ; :: according to RELAT_1:def 3 :: thesis: for b1 being set holds
( not [x,b1] in R or [x,b1] in S )
let y be set ; :: thesis: ( not [x,y] in R or [x,y] in S )
assume [x,y] in R ; :: thesis: [x,y] in S
hence [x,y] in S by A5, A10, A11, TARSKI:def 4; :: thesis: verum
end;
then X c= field S by A2, RELAT_1:16;
then field S = X by A46, XBOOLE_0:def 10;
hence union Z in Rel by A3, A9, A8, A55, A45; :: thesis: verum
end;
R c= [:X,X:] by A2, Lm4;
then Rel <> {} by A1, A2, A3;
then consider Y being set such that
A56: Y in Rel and
A57: for Z being set st Z in Rel & Z <> Y holds
not Y c= Z by A4, Th177;
consider P being Relation such that
A58: Y = P and
A59: R c= P and
A60: P partially_orders X and
A61: field P = X by A3, A56;
take P ; :: thesis: ( R c= P & P linearly_orders X & field P = X )
thus R c= P by A59; :: thesis: ( P linearly_orders X & field P = X )
thus A62: ( P is_reflexive_in X & P is_transitive_in X & P is_antisymmetric_in X ) by A60, Def7; :: according to ORDERS_1:def 8 :: thesis: ( P is_connected_in X & field P = X )
thus P is_connected_in X :: thesis: field P = X
proof
let x be set ; :: according to RELAT_2:def 6 :: thesis: for b1 being set holds
( not x in X or not b1 in X or x = b1 or [x,b1] in P or [b1,x] in P )
let y be set ; :: thesis: ( not x in X or not y in X or x = y or [x,y] in P or [y,x] in P )
assume that
A63: x in X and
A64: y in X and
x <> y and
A65: not [x,y] in P and
A66: not [y,x] in P ; :: thesis: contradiction
defpred S2[ set , set ] means ( [$1,$2] in P or ( [$1,x] in P & [y,$2] in P ) );
consider Q being Relation such that
A67: for z, u being set holds
( [z,u] in Q iff ( z in X & u in X & S2[z,u] ) ) from RELAT_1:sch 1();
 A68: field Q c= X
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in field Q or z in X )
A69: now
assume z in dom Q ; :: thesis: ( not z in field Q or z in X )
then ex u being set st [z,u] in Q by RELAT_1:def 4;
hence ( not z in field Q or z in X ) by A67; :: thesis: verum
end;
A70: now
assume z in rng Q ; :: thesis: ( not z in field Q or z in X )
then ex u being set st [u,z] in Q by RELAT_1:def 5;
hence ( not z in field Q or z in X ) by A67; :: thesis: verum
end;
assume z in field Q ; :: thesis: z in X
hence z in X by A69, A70, XBOOLE_0:def 3; :: thesis: verum
end;
A71: P c= Q
proof
let z be set ; :: according to RELAT_1:def 3 :: thesis: for b1 being set holds
( not [z,b1] in P or [z,b1] in Q )
let u be set ; :: thesis: ( not [z,u] in P or [z,u] in Q )
assume A72: [z,u] in P ; :: thesis: [z,u] in Q
then A73: u in field P by RELAT_1:15;
z in field P by A72, RELAT_1:15;
hence [z,u] in Q by A61, A67, A72, A73; :: thesis: verum
end;
then X c= field Q by A61, RELAT_1:16;
then A74: field Q = X by A68, XBOOLE_0:def 10;
A75: Q is_transitive_in X
proof
let a, b, c be set ; :: according to RELAT_2:def 8 :: thesis: ( not a in X or not b in X or not c in X or not [a,b] in Q or not [b,c] in Q or [a,c] in Q )
assume that
A76: a in X and
A77: b in X and
A78: c in X and
A79: [a,b] in Q and
A80: [b,c] in Q ; :: thesis: [a,c] in Q
A81: ( [b,c] in P or ( [b,x] in P & [y,c] in P ) ) by A67, A80;
( [a,b] in P or ( [a,x] in P & [y,b] in P ) ) by A67, A79;
then ( [a,c] in P or ( [a,x] in P & [y,c] in P ) or ( [a,x] in P & [y,c] in P ) or [y,x] in P ) by A62, A63, A64, A76, A77, A78, A81, RELAT_2:def 8;
hence [a,c] in Q by A66, A67, A76, A78; :: thesis: verum
end;
A82: Q is_antisymmetric_in X
proof
let a, b be set ; :: according to RELAT_2:def 4 :: thesis: ( not a in X or not b in X or not [a,b] in Q or not [b,a] in Q or a = b )
assume that
A83: a in X and
A84: b in X and
A85: [a,b] in Q and
A86: [b,a] in Q ; :: thesis: a = b
A87: ( [b,a] in P or ( [b,x] in P & [y,a] in P ) ) by A67, A86;
( [a,b] in P or ( [a,x] in P & [y,b] in P ) ) by A67, A85;
then ( a = b or ( [a,x] in P & [y,a] in P ) or [y,x] in P ) by A62, A63, A64, A83, A84, A87, RELAT_2:def 4, RELAT_2:def 8;
hence a = b by A62, A63, A64, A66, A83, RELAT_2:def 8; :: thesis: verum
end;
Q is_reflexive_in X
proof
let z be set ; :: according to RELAT_2:def 1 :: thesis: ( not z in X or [z,z] in Q )
assume A88: z in X ; :: thesis: [z,z] in Q
then [z,z] in P by A62, RELAT_2:def 1;
hence [z,z] in Q by A67, A88; :: thesis: verum
end;
then A89: Q partially_orders X by A75, A82, Def7;
A90: Q c= [:X,X:]
proof
let y be set ; :: according to RELAT_1:def 3 :: thesis: for b1 being set holds
( not [y,b1] in Q or [y,b1] in [:X,X:] )
let z be set ; :: thesis: ( not [y,z] in Q or [y,z] in [:X,X:] )
assume A91: [y,z] in Q ; :: thesis: [y,z] in [:X,X:]
then A92: z in X by A67;
y in X by A67, A91;
hence [y,z] in [:X,X:] by A92, ZFMISC_1:87; :: thesis: verum
end;
R c= Q by A59, A71, XBOOLE_1:1;
then Q in Rel by A3, A90, A74, A89;
then A93: Q = P by A57, A58, A71;
A94: [y,y] in P by A62, A64, RELAT_2:def 1;
[x,x] in P by A62, A63, RELAT_2:def 1;
hence contradiction by A63, A64, A65, A67, A93, A94; :: thesis: verum
end;
thus field P = X by A61; :: thesis: verum