let X be set ; :: thesis: for R being Relation st R well_orders X holds
( field (R |_2 X) = X & R |_2 X is well-ordering )
let R be Relation; :: thesis: ( R well_orders X implies ( field (R |_2 X) = X & R |_2 X is well-ordering ) )
assume that
A1: R is_reflexive_in X and
A2: R is_transitive_in X and
A3: R is_antisymmetric_in X and
A4: R is_connected_in X and
A5: R is_well_founded_in X ; :: according to WELLORD1:def 5 :: thesis: ( field (R |_2 X) = X & R |_2 X is well-ordering )
A6: R |_2 X is_antisymmetric_in X
proof
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
A7: ( x in X & y in X ) and
A8: ( [x,y] in R |_2 X & [y,x] in R |_2 X ) ; :: thesis: x = y
( [x,y] in R & [y,x] in R ) by A8, XBOOLE_0:def 4;
hence x = y by A3, A7; :: thesis: verum
end;
A9: R |_2 X is_well_founded_in X
proof
let Y be set ; :: according to WELLORD1:def 3 :: thesis: ( not Y c= X or Y = {} or ex b1 being object st
( b1 in Y & (R |_2 X) -Seg b1 misses Y ) )
assume ( Y c= X & Y <> {} ) ; :: thesis: ex b1 being object st
( b1 in Y & (R |_2 X) -Seg b1 misses Y )
then consider a being object such that
A10: a in Y and
A11: R -Seg a misses Y by A5;
take a ; :: thesis: ( a in Y & (R |_2 X) -Seg a misses Y )
thus a in Y by A10; :: thesis: (R |_2 X) -Seg a misses Y
assume not (R |_2 X) -Seg a misses Y ; :: thesis: contradiction
then consider x being object such that
A12: x in (R |_2 X) -Seg a and
A13: x in Y by XBOOLE_0:3;
[x,a] in R |_2 X by A12, WELLORD1:1;
then A14: [x,a] in R by XBOOLE_0:def 4;
x <> a by A12, WELLORD1:1;
then x in R -Seg a by A14, WELLORD1:1;
hence contradiction by A11, A13, XBOOLE_0:3; :: thesis: verum
end;
A15: R |_2 X is_transitive_in X
proof
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
A16: x in X and
A17: y in X and
A18: z in X and
A19: ( [x,y] in R |_2 X & [y,z] in R |_2 X ) ; :: thesis: [x,z] in R |_2 X
( [x,y] in R & [y,z] in R ) by A19, XBOOLE_0:def 4;
then A20: [x,z] in R by A2, A16, A17, A18;
[x,z] in [:X,X:] by A16, A18, ZFMISC_1:87;
hence [x,z] in R |_2 X by A20, XBOOLE_0:def 4; :: thesis: verum
end;
A21: R |_2 X is_connected_in X
proof
let x, y be object ; :: according to RELAT_2:def 6 :: thesis: ( not x in X or not y in X or x = y or [x,y] in R |_2 X or [y,x] in R |_2 X )
assume that
A22: ( x in X & y in X ) and
A23: x <> y ; :: thesis: ( [x,y] in R |_2 X or [y,x] in R |_2 X )
A24: ( [x,y] in [:X,X:] & [y,x] in [:X,X:] ) by A22, ZFMISC_1:87;
( [x,y] in R or [y,x] in R ) by A4, A22, A23;
hence ( [x,y] in R |_2 X or [y,x] in R |_2 X ) by A24, XBOOLE_0:def 4; :: thesis: verum
end;
thus A25: field (R |_2 X) = X :: thesis: R |_2 X is well-ordering
proof
thus field (R |_2 X) c= X by WELLORD1:13; :: according to XBOOLE_0:def 10 :: thesis: X c= field (R |_2 X)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in field (R |_2 X) )
assume x in X ; :: thesis: x in field (R |_2 X)
then ( [x,x] in R & [x,x] in [:X,X:] ) by A1, ZFMISC_1:87;
then [x,x] in R |_2 X by XBOOLE_0:def 4;
hence x in field (R |_2 X) by RELAT_1:15; :: thesis: verum
end;
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 x in X ; :: thesis: [x,x] in R |_2 X
then ( [x,x] in R & [x,x] in [:X,X:] ) by A1, ZFMISC_1:87;
hence [x,x] in R |_2 X by XBOOLE_0:def 4; :: thesis: verum
end;
then R |_2 X well_orders X by A15, A6, A21, A9;
hence R |_2 X is well-ordering by A25, WELLORD1:4; :: thesis: verum