let R be Relation; :: thesis: for X being set st R partially_orders X holds
R |_2 X is Order of X
let X be set ; :: thesis: ( R partially_orders X implies R |_2 X is Order of X )
set S = R |_2 X;
A1: field (R |_2 X) c= X by WELLORD1:13;
rng (R |_2 X) c= field (R |_2 X) by XBOOLE_1:7;
then A2: rng (R |_2 X) c= X by A1;
dom (R |_2 X) c= field (R |_2 X) by XBOOLE_1:7;
then dom (R |_2 X) c= X by A1;
then reconsider S = R |_2 X as Relation of X by A2, RELSET_1:4;
assume A3: R partially_orders X ; :: thesis: R |_2 X is Order of X
A4: R |_2 X is_antisymmetric_in X
proof
A5: R is_antisymmetric_in X by A3;
let x, y be object ; :: according to RELAT_2:def 4 :: thesis: ( not x in X or not y in X or not [x,y] in R |_2 X or not [y,x] in R |_2 X or x = y )
assume that
A6: x in X and
A7: y in X and
A8: [x,y] in R |_2 X and
A9: [y,x] in R |_2 X ; :: thesis: x = y
A10: [y,x] in R by A9, XBOOLE_0:def 4;
[x,y] in R by A8, XBOOLE_0:def 4;
hence x = y by A6, A7, A10, A5; :: thesis: verum
end;
A11: R |_2 X is_transitive_in X
proof
A12: R is_transitive_in X by A3;
let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in X or not y in X or not z in X or not [x,y] in R |_2 X or not [y,z] in R |_2 X or [x,z] in R |_2 X )
assume that
A13: x in X and
A14: y in X and
A15: z in X and
A16: [x,y] in R |_2 X and
A17: [y,z] in R |_2 X ; :: thesis: [x,z] in R |_2 X
A18: [x,z] in [:X,X:] by A13, A15, ZFMISC_1:87;
A19: [y,z] in R by A17, XBOOLE_0:def 4;
[x,y] in R by A16, XBOOLE_0:def 4;
then [x,z] in R by A13, A14, A15, A19, A12;
hence [x,z] in R |_2 X by A18, XBOOLE_0:def 4; :: thesis: verum
end;
A20: R is_reflexive_in X by A3;
A21: R |_2 X is_reflexive_in X
proof
let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in X or [x,x] in R |_2 X )
assume A22: x in X ; :: thesis: [x,x] in R |_2 X
then A23: [x,x] in [:X,X:] by ZFMISC_1:87;
[x,x] in R by A20, A22;
hence [x,x] in R |_2 X by A23, XBOOLE_0:def 4; :: thesis: verum
end;
then A24: field S = X by Th13;
dom S = X by A21, Th13;
hence R |_2 X is Order of X by A21, A24, A4, A11, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16; :: thesis: verum