let R, S be Relation; :: thesis: for F being Function st F is_isomorphism_of R,S holds
( ( R is reflexive implies S is reflexive ) & ( R is transitive implies S is transitive ) & ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )
let F be Function; :: thesis: ( F is_isomorphism_of R,S implies ( ( R is reflexive implies S is reflexive ) & ( R is transitive implies S is transitive ) & ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) ) )
assume A1: F is_isomorphism_of R,S ; :: thesis: ( ( R is reflexive implies S is reflexive ) & ( R is transitive implies S is transitive ) & ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )
then A2: dom F = field R ;
A3: rng F = field S by A1;
A4: F is one-to-one by A1;
then A5: ( rng (F ") = dom F & dom (F ") = rng F ) by FUNCT_1:33;
thus ( R is reflexive implies S is reflexive ) :: thesis: ( ( R is transitive implies S is transitive ) & ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )
proof
assume A6: R is reflexive ; :: thesis: S is reflexive
now :: thesis: for a being object st a in field S holds
[a,a] in S
let a be object ; :: thesis: ( a in field S implies [a,a] in S )
assume A7: a in field S ; :: thesis: [a,a] in S
then (F ") . a in field R by A2, A3, A5, FUNCT_1:def 3;
then A8: [((F ") . a),((F ") . a)] in R by A6, Lm1;
a = F . ((F ") . a) by A3, A4, A7, FUNCT_1:35;
hence [a,a] in S by A1, A8; :: thesis: verum
end;
hence S is reflexive by Lm1; :: thesis: verum
end;
thus ( R is transitive implies S is transitive ) :: thesis: ( ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )
proof
assume A9: R is transitive ; :: thesis: S is transitive
now :: thesis: for a, b, c being object st [a,b] in S & [b,c] in S holds
[a,c] in S
let a, b, c be object ; :: thesis: ( [a,b] in S & [b,c] in S implies [a,c] in S )
assume that
A10: [a,b] in S and
A11: [b,c] in S ; :: thesis: [a,c] in S
A12: c in field S by A11, RELAT_1:15;
then A13: c = F . ((F ") . c) by A3, A4, FUNCT_1:35;
b in field S by A10, RELAT_1:15;
then A14: ( b = F . ((F ") . b) & (F ") . b in field R ) by A2, A3, A4, A5, FUNCT_1:35, FUNCT_1:def 3;
(F ") . c in field R by A2, A3, A5, A12, FUNCT_1:def 3;
then A15: [((F ") . b),((F ") . c)] in R by A1, A11, A13, A14;
A16: a in field S by A10, RELAT_1:15;
then A17: a = F . ((F ") . a) by A3, A4, FUNCT_1:35;
(F ") . a in field R by A2, A3, A5, A16, FUNCT_1:def 3;
then [((F ") . a),((F ") . b)] in R by A1, A10, A17, A14;
then [((F ") . a),((F ") . c)] in R by A9, A15, Lm2;
hence [a,c] in S by A1, A17, A13; :: thesis: verum
end;
hence S is transitive by Lm2; :: thesis: verum
end;
thus ( R is connected implies S is connected ) :: thesis: ( ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )
proof
assume A18: R is connected ; :: thesis: S is connected
now :: thesis: for a, b being object st a in field S & b in field S & a <> b & not [a,b] in S holds
[b,a] in S
let a, b be object ; :: thesis: ( a in field S & b in field S & a <> b & not [a,b] in S implies [b,a] in S )
assume that
A19: ( a in field S & b in field S ) and
A20: a <> b ; :: thesis: ( [a,b] in S or [b,a] in S )
A21: ( a = F . ((F ") . a) & b = F . ((F ") . b) ) by A3, A4, A19, FUNCT_1:35;
( (F ") . a in field R & (F ") . b in field R ) by A2, A3, A5, A19, FUNCT_1:def 3;
then ( [((F ") . a),((F ") . b)] in R or [((F ") . b),((F ") . a)] in R ) by A18, A20, A21, Lm4;
hence ( [a,b] in S or [b,a] in S ) by A1, A21; :: thesis: verum
end;
hence S is connected by Lm4; :: thesis: verum
end;
thus ( R is antisymmetric implies S is antisymmetric ) :: thesis: ( R is well_founded implies S is well_founded )
proof
assume A22: R is antisymmetric ; :: thesis: S is antisymmetric
now :: thesis: for a, b being object st [a,b] in S & [b,a] in S holds
a = b
let a, b be object ; :: thesis: ( [a,b] in S & [b,a] in S implies a = b )
assume that
A23: [a,b] in S and
A24: [b,a] in S ; :: thesis: a = b
A25: a in field S by A23, RELAT_1:15;
then A26: a = F . ((F ") . a) by A3, A4, FUNCT_1:35;
A27: b in field S by A23, RELAT_1:15;
then A28: b = F . ((F ") . b) by A3, A4, FUNCT_1:35;
A29: (F ") . b in field R by A2, A3, A5, A27, FUNCT_1:def 3;
(F ") . a in field R by A2, A3, A5, A25, FUNCT_1:def 3;
then ( [((F ") . a),((F ") . b)] in R & [((F ") . b),((F ") . a)] in R ) by A1, A23, A24, A26, A28, A29;
hence a = b by A22, A26, A28, Lm3; :: thesis: verum
end;
hence S is antisymmetric by Lm3; :: thesis: verum
end;
assume A30: for Y being set st Y c= field R & Y <> {} holds
ex x being object st
( x in Y & R -Seg x misses Y ) ; :: according to WELLORD1:def 2 :: thesis: S is well_founded
let Z be set ; :: according to WELLORD1:def 2 :: thesis: ( Z c= field S & Z <> {} implies ex a being object st
( a in Z & S -Seg a misses Z ) )
assume that
A31: Z c= field S and
A32: Z <> {} ; :: thesis: ex a being object st
( a in Z & S -Seg a misses Z )
A33: F " Z c= dom F by RELAT_1:132;
then consider x being object such that
A34: x in F " Z and
A35: R -Seg x misses F " Z by A2, A3, A30, A31, A32, RELAT_1:139;
take F . x ; :: thesis: ( F . x in Z & S -Seg (F . x) misses Z )
thus F . x in Z by A34, FUNCT_1:def 7; :: thesis: S -Seg (F . x) misses Z
assume not S -Seg (F . x) misses Z ; :: thesis: contradiction
then consider y being object such that
A36: y in S -Seg (F . x) and
A37: y in Z by XBOOLE_0:3;
A38: (F ") . y in dom F by A3, A5, A31, A37, FUNCT_1:def 3;
A39: [y,(F . x)] in S by A36, Th1;
A40: y = F . ((F ") . y) by A3, A4, A31, A37, FUNCT_1:35;
then (F ") . y in F " Z by A37, A38, FUNCT_1:def 7;
then not (F ") . y in R -Seg x by A35, XBOOLE_0:3;
then ( not [((F ") . y),x] in R or (F ") . y = x ) by Th1;
hence contradiction by A1, A33, A34, A36, A40, A38, A39, Th1; :: thesis: verum