let Z be set ; :: thesis: for R, S being Relation
for F being Function st R is well-ordering & Z c= field R & F is_isomorphism_of R,S holds
( F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) & R |_2 Z,S |_2 (F .: Z) are_isomorphic )
let R, S be Relation; :: thesis: for F being Function st R is well-ordering & Z c= field R & F is_isomorphism_of R,S holds
( F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) & R |_2 Z,S |_2 (F .: Z) are_isomorphic )
let F be Function; :: thesis: ( R is well-ordering & Z c= field R & F is_isomorphism_of R,S implies ( F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) & R |_2 Z,S |_2 (F .: Z) are_isomorphic ) )
assume that
A1: R is well-ordering and
A2: Z c= field R and
A3: F is_isomorphism_of R,S ; :: thesis: ( F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) & R |_2 Z,S |_2 (F .: Z) are_isomorphic )
A4: F .: Z c= rng F by RELAT_1:111;
A5: F .: Z = field (S |_2 (F .: Z)) by A1, A3, A4, Th31, Th44;
A6: F is one-to-one by A3;
A7: Z = field (R |_2 Z) by A1, A2, Th31;
A8: dom F = field R by A3;
thus F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) :: thesis: R |_2 Z,S |_2 (F .: Z) are_isomorphic
proof
thus A9: dom (F | Z) = field (R |_2 Z) by A2, A8, A7, RELAT_1:62; :: according to WELLORD1:def 7 :: thesis: ( rng (F | Z) = field (S |_2 (F .: Z)) & F | Z is one-to-one & ( for a, b being object holds
( [a,b] in R |_2 Z iff ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ) ) ) )
thus A10: rng (F | Z) = field (S |_2 (F .: Z)) by A5, RELAT_1:115; :: thesis: ( F | Z is one-to-one & ( for a, b being object holds
( [a,b] in R |_2 Z iff ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ) ) ) )
thus F | Z is one-to-one by A6, FUNCT_1:52; :: thesis: for a, b being object holds
( [a,b] in R |_2 Z iff ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ) )
let a, b be object ; :: thesis: ( [a,b] in R |_2 Z iff ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ) )
thus ( [a,b] in R |_2 Z implies ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ) ) :: thesis: ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) implies [a,b] in R |_2 Z )
proof
assume A11: [a,b] in R |_2 Z ; :: thesis: ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) )
then [a,b] in R by XBOOLE_0:def 4;
then A12: [(F . a),(F . b)] in S by A3;
thus A13: ( a in field (R |_2 Z) & b in field (R |_2 Z) ) by A11, RELAT_1:15; :: thesis: [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z)
then ( (F | Z) . a in rng (F | Z) & (F | Z) . b in rng (F | Z) ) by A9, FUNCT_1:def 3;
then A14: [((F | Z) . a),((F | Z) . b)] in [:(F .: Z),(F .: Z):] by A5, A10, ZFMISC_1:87;
( F . a = (F | Z) . a & F . b = (F | Z) . b ) by A9, A13, FUNCT_1:47;
hence [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) by A12, A14, XBOOLE_0:def 4; :: thesis: verum
end;
assume that
A15: ( a in field (R |_2 Z) & b in field (R |_2 Z) ) and
A16: [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ; :: thesis: [a,b] in R |_2 Z
( F . a = (F | Z) . a & F . b = (F | Z) . b ) by A9, A15, FUNCT_1:47;
then A17: [(F . a),(F . b)] in S by A16, XBOOLE_0:def 4;
A18: [a,b] in [:Z,Z:] by A7, A15, ZFMISC_1:87;
( a in field R & b in field R ) by A15, Th12;
then [a,b] in R by A3, A17;
hence [a,b] in R |_2 Z by A18, XBOOLE_0:def 4; :: thesis: verum
end;
hence R |_2 Z,S |_2 (F .: Z) are_isomorphic ; :: thesis: verum