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 ) )

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

( ( 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

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 ) )
assume A6:
R is reflexive
; :: thesis: S is reflexive

end;now :: thesis: for a being object st a in field S holds

[a,a] in S

hence
S is reflexive
by Lm1; :: thesis: verum[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;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

proof

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 ) )
assume A9:
R is transitive
; :: thesis: S is transitive

end;now :: thesis: for a, b, c being object st [a,b] in S & [b,c] in S holds

[a,c] in S

hence
S is transitive
by Lm2; :: thesis: verum[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;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

proof

thus
( R is antisymmetric implies S is antisymmetric )
:: thesis: ( R is well_founded implies S is well_founded )
assume A18:
R is connected
; :: thesis: S is connected

end;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

hence
S is connected
by Lm4; :: thesis: verum[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;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

proof

assume A30:
for Y being set st Y c= field R & Y <> {} holds
assume A22:
R is antisymmetric
; :: thesis: S is antisymmetric

end;now :: thesis: for a, b being object st [a,b] in S & [b,a] in S holds

a = b

hence
S is antisymmetric
by Lm3; :: thesis: veruma = 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;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

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