let R, S be Relation; :: thesis: ( R is well-ordering & S is well-ordering & not R,S are_isomorphic & ( for a being object holds
( not a in field R or not R |_2 (R -Seg a),S are_isomorphic ) ) implies ex a being object st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )
assume that
A1: R is well-ordering and
A2: S is well-ordering ; :: thesis: ( R,S are_isomorphic or ex a being object st
( a in field R & R |_2 (R -Seg a),S are_isomorphic ) or ex a being object st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )
defpred S1[ object ] means ex b being object st
( b in field S & R |_2 (R -Seg $1),S |_2 (S -Seg b) are_isomorphic );
consider Z being set such that
A3: for a being object holds
( a in Z iff ( a in field R & S1[a] ) ) from XBOOLE_0:sch 1();
 A4: Z c= field R by A3;
defpred S2[ object , object ] means ( $2 in field S & R |_2 (R -Seg $1),S |_2 (S -Seg $2) are_isomorphic );
A5: for a, b, c being object st S2[a,b] & S2[a,c] holds
b = c
proof
let a, b, c be object ; :: thesis: ( S2[a,b] & S2[a,c] implies b = c )
assume that
A6: b in field S and
A7: R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic and
A8: ( c in field S & R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic ) ; :: thesis: b = c
S |_2 (S -Seg b),R |_2 (R -Seg a) are_isomorphic by A7, Th40;
hence b = c by A2, A6, A8, Th42, Th47; :: thesis: verum
end;
consider F being Function such that
A9: for a, b being object holds
( [a,b] in F iff ( a in field R & S2[a,b] ) ) from FUNCT_1:sch 1(A5);
 A10: Z = dom F
proof
thus for a being object st a in Z holds
a in dom F :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: dom F c= Z
proof
let a be object ; :: thesis: ( a in Z implies a in dom F )
assume A11: a in Z ; :: thesis: a in dom F
then consider b being object such that
A12: ( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic ) by A3;
a in field R by A3, A11;
then [a,b] in F by A9, A12;
hence a in dom F by XTUPLE_0:def 12; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom F or a in Z )
assume a in dom F ; :: thesis: a in Z
then consider b being object such that
A13: [a,b] in F by XTUPLE_0:def 12;
A14: R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic by A9, A13;
( a in field R & b in field S ) by A9, A13;
hence a in Z by A3, A14; :: thesis: verum
end;
A15: rng F c= field S
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng F or a in field S )
assume a in rng F ; :: thesis: a in field S
then consider b being object such that
A16: ( b in dom F & a = F . b ) by FUNCT_1:def 3;
[b,a] in F by A16, FUNCT_1:1;
hence a in field S by A9; :: thesis: verum
end;
A17: F is_isomorphism_of R |_2 (dom F),S |_2 (rng F)
proof
thus ( dom F = field (R |_2 (dom F)) & rng F = field (S |_2 (rng F)) ) by A1, A2, A4, A15, A10, Th31; :: according to WELLORD1:def 7 :: thesis: ( F is one-to-one & ( for a, b being object holds
( [a,b] in R |_2 (dom F) iff ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) ) ) ) )
thus A18: F is one-to-one :: thesis: for a, b being object holds
( [a,b] in R |_2 (dom F) iff ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) ) )
proof
let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in dom F or not b in dom F or not F . a = F . b or a = b )
assume that
A19: a in dom F and
A20: b in dom F and
A21: F . a = F . b ; :: thesis: a = b
A22: [b,(F . b)] in F by A20, FUNCT_1:1;
then R |_2 (R -Seg b),S |_2 (S -Seg (F . a)) are_isomorphic by A9, A21;
then A23: S |_2 (S -Seg (F . a)),R |_2 (R -Seg b) are_isomorphic by Th40;
[a,(F . a)] in F by A19, FUNCT_1:1;
then A24: ( a in field R & R |_2 (R -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic ) by A9;
b in field R by A9, A22;
hence a = b by A1, A24, A23, Th42, Th47; :: thesis: verum
end;
let a, b be object ; :: thesis: ( [a,b] in R |_2 (dom F) iff ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) ) )
set P = R |_2 (R -Seg a);
A25: ( field (R |_2 (R -Seg a)) = R -Seg a & R |_2 (R -Seg a) is well-ordering ) by A1, Th25, Th32;
thus ( [a,b] in R |_2 (dom F) implies ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) ) ) :: thesis: ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) implies [a,b] in R |_2 (dom F) )
proof
assume A26: [a,b] in R |_2 (dom F) ; :: thesis: ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) )
hence A27: ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) ) by RELAT_1:15; :: thesis: [(F . a),(F . b)] in S |_2 (rng F)
then A28: a in dom F by Th12;
then A29: [a,(F . a)] in F by FUNCT_1:1;
then A30: F . a in field S by A9;
A31: b in dom F by A27, Th12;
then A32: [b,(F . b)] in F by FUNCT_1:1;
then A33: b in field R by A9;
A34: ( F . b in field S & R |_2 (R -Seg b),S |_2 (S -Seg (F . b)) are_isomorphic ) by A9, A32;
A35: [a,b] in R by A26, XBOOLE_0:def 4;
A36: F . b in rng F by A31, FUNCT_1:def 3;
F . a in rng F by A28, FUNCT_1:def 3;
then A37: [(F . a),(F . b)] in [:(rng F),(rng F):] by A36, ZFMISC_1:87;
a in field R by A9, A29;
then A38: R -Seg a c= R -Seg b by A1, A33, A35, Th29;
A39: R |_2 (R -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic by A9, A29;
A40: now :: thesis: ( a <> b implies [(F . a),(F . b)] in S |_2 (rng F) )
set P = R |_2 (R -Seg b);
A41: ( field (R |_2 (R -Seg b)) = R -Seg b & R |_2 (R -Seg b) is well-ordering ) by A1, Th25, Th32;
assume a <> b ; :: thesis: [(F . a),(F . b)] in S |_2 (rng F)
then A42: a in R -Seg b by A35, Th1;
then (R |_2 (R -Seg b)) -Seg a = R -Seg a by A1, Th27;
then (R |_2 (R -Seg b)) |_2 ((R |_2 (R -Seg b)) -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic by A39, A38, Th22;
then [(F . a),(F . b)] in S by A2, A30, A34, A42, A41, Th51;
hence [(F . a),(F . b)] in S |_2 (rng F) by A37, XBOOLE_0:def 4; :: thesis: verum
end;
( a = b implies [(F . a),(F . b)] in S |_2 (rng F) )
proof
assume a = b ; :: thesis: [(F . a),(F . b)] in S |_2 (rng F)
then [(F . a),(F . b)] in S by A2, A30, Lm1;
hence [(F . a),(F . b)] in S |_2 (rng F) by A37, XBOOLE_0:def 4; :: thesis: verum
end;
hence [(F . a),(F . b)] in S |_2 (rng F) by A40; :: thesis: verum
end;
assume that
A43: a in field (R |_2 (dom F)) and
A44: b in field (R |_2 (dom F)) and
A45: [(F . a),(F . b)] in S |_2 (rng F) ; :: thesis: [a,b] in R |_2 (dom F)
A46: [(F . a),(F . b)] in S by A45, XBOOLE_0:def 4;
A47: a in dom F by A43, Th12;
then A48: [a,(F . a)] in F by FUNCT_1:1;
then A49: a in field R by A9;
assume not [a,b] in R |_2 (dom F) ; :: thesis: contradiction
then A50: ( not [a,b] in R or not [a,b] in [:(dom F),(dom F):] ) by XBOOLE_0:def 4;
then A51: a <> b by A1, A47, A49, Lm1, ZFMISC_1:87;
A52: b in dom F by A44, Th12;
then A53: [b,(F . b)] in F by FUNCT_1:1;
then A54: R |_2 (R -Seg b),S |_2 (S -Seg (F . b)) are_isomorphic by A9;
A55: b in field R by A9, A53;
then A56: [b,a] in R by A1, A47, A52, A50, A49, A51, Lm4, ZFMISC_1:87;
then A57: R -Seg b c= R -Seg a by A1, A49, A55, Th29;
A58: b in R -Seg a by A47, A52, A50, A56, Th1, ZFMISC_1:87;
then (R |_2 (R -Seg a)) -Seg b = R -Seg b by A1, Th27;
then A59: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b),S |_2 (S -Seg (F . b)) are_isomorphic by A54, A57, Th22;
A60: F . b in field S by A9, A53;
( F . a in field S & R |_2 (R -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic ) by A9, A48;
then [(F . b),(F . a)] in S by A2, A60, A58, A25, A59, Th51;
then F . a = F . b by A2, A46, Lm3;
hence contradiction by A18, A47, A52, A51; :: thesis: verum
end;
A61: now :: thesis: ( ex a being object st
( a in field R & Z = R -Seg a ) implies for b being object holds
( not b in field S or not rng F = S -Seg b ) )
given a being object such that A62: a in field R and
A63: Z = R -Seg a ; :: thesis: for b being object holds
( not b in field S or not rng F = S -Seg b )
given b being object such that A64: b in field S and
A65: rng F = S -Seg b ; :: thesis: contradiction
R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic by A10, A17, A63, A65;
then a in Z by A3, A62, A64;
hence contradiction by A63, Th1; :: thesis: verum
end;
A66: now :: thesis: for a being object st a in Z holds
for b being object st [b,a] in R holds
b in Z
let a be object ; :: thesis: ( a in Z implies for b being object st [b,a] in R holds
b in Z )
assume A67: a in Z ; :: thesis: for b being object st [b,a] in R holds
b in Z
consider c being object such that
A68: c in field S and
A69: R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic by A3, A67;
let b be object ; :: thesis: ( [b,a] in R implies b in Z )
assume A70: [b,a] in R ; :: thesis: b in Z
A71: a in field R by A3, A67;
now :: thesis: ( a <> b implies b in Z )
set Q = S |_2 (S -Seg c);
set P = R |_2 (R -Seg a);
R |_2 (R -Seg a) is well-ordering by A1, Th25;
then A72: canonical_isomorphism_of ((R |_2 (R -Seg a)),(S |_2 (S -Seg c))) is_isomorphism_of R |_2 (R -Seg a),S |_2 (S -Seg c) by A69, Def9;
assume a <> b ; :: thesis: b in Z
then A73: b in R -Seg a by A70, Th1;
then A74: (R |_2 (R -Seg a)) -Seg b = R -Seg b by A1, Th27;
A75: b in field R by A70, RELAT_1:15;
then R -Seg b c= R -Seg a by A1, A71, A73, Th30;
then A76: (R |_2 (R -Seg a)) |_2 (R -Seg b) = R |_2 (R -Seg b) by Th22;
field (R |_2 (R -Seg a)) = R -Seg a by A1, Th32;
then consider d being object such that
A77: d in field (S |_2 (S -Seg c)) and
A78: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b),(S |_2 (S -Seg c)) |_2 ((S |_2 (S -Seg c)) -Seg d) are_isomorphic by A1, A72, A73, Th25, Th50;
A79: S -Seg c = field (S |_2 (S -Seg c)) by A2, Th32;
then A80: (S |_2 (S -Seg c)) -Seg d = S -Seg d by A2, A77, Th27;
[d,c] in S by A77, A79, Th1;
then A81: d in field S by RELAT_1:15;
then S -Seg d c= S -Seg c by A2, A68, A77, A79, Th30;
then R |_2 (R -Seg b),S |_2 (S -Seg d) are_isomorphic by A78, A74, A80, A76, Th22;
hence b in Z by A3, A75, A81; :: thesis: verum
end;
hence b in Z by A67; :: thesis: verum
end;
A82: R |_2 Z,S |_2 (rng F) are_isomorphic by A10, A17;
A83: now :: thesis: ( Z = field R & ex a being object st
( a in field S & rng F = S -Seg a ) implies ex a being object st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )
assume A84: Z = field R ; :: thesis: ( ex a being object st
( a in field S & rng F = S -Seg a ) implies ex a being object st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )
given a being object such that A85: a in field S and
A86: rng F = S -Seg a ; :: thesis: ex a being object st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic )
take a = a; :: thesis: ( a in field S & R,S |_2 (S -Seg a) are_isomorphic )
thus a in field S by A85; :: thesis: R,S |_2 (S -Seg a) are_isomorphic
thus R,S |_2 (S -Seg a) are_isomorphic by A82, A84, A86, Th23; :: thesis: verum
end;
A87: now :: thesis: for a being object st a in rng F holds
for b being object st [b,a] in S holds
b in rng F
let a be object ; :: thesis: ( a in rng F implies for b being object st [b,a] in S holds
b in rng F )
assume A88: a in rng F ; :: thesis: for b being object st [b,a] in S holds
b in rng F
consider c being object such that
A89: ( c in dom F & a = F . c ) by A88, FUNCT_1:def 3;
A90: [c,a] in F by A89, FUNCT_1:1;
then A91: a in field S by A9;
let b be object ; :: thesis: ( [b,a] in S implies b in rng F )
assume A92: [b,a] in S ; :: thesis: b in rng F
A93: R |_2 (R -Seg c),S |_2 (S -Seg a) are_isomorphic by A9, A90;
A94: c in field R by A9, A90;
now :: thesis: ( a <> b implies b in rng F )
set Q = S |_2 (S -Seg a);
set P = R |_2 (R -Seg c);
assume a <> b ; :: thesis: b in rng F
then A95: b in S -Seg a by A92, Th1;
then A96: (S |_2 (S -Seg a)) -Seg b = S -Seg b by A2, Th27;
A97: b in field S by A92, RELAT_1:15;
then S -Seg b c= S -Seg a by A2, A91, A95, Th30;
then A98: (S |_2 (S -Seg a)) |_2 (S -Seg b) = S |_2 (S -Seg b) by Th22;
( S |_2 (S -Seg a),R |_2 (R -Seg c) are_isomorphic & S |_2 (S -Seg a) is well-ordering ) by A2, A93, Th25, Th40;
then A99: canonical_isomorphism_of ((S |_2 (S -Seg a)),(R |_2 (R -Seg c))) is_isomorphism_of S |_2 (S -Seg a),R |_2 (R -Seg c) by Def9;
field (S |_2 (S -Seg a)) = S -Seg a by A2, Th32;
then consider d being object such that
A100: d in field (R |_2 (R -Seg c)) and
A101: (S |_2 (S -Seg a)) |_2 ((S |_2 (S -Seg a)) -Seg b),(R |_2 (R -Seg c)) |_2 ((R |_2 (R -Seg c)) -Seg d) are_isomorphic by A2, A99, A95, Th25, Th50;
A102: R -Seg c = field (R |_2 (R -Seg c)) by A1, Th32;
then A103: (R |_2 (R -Seg c)) -Seg d = R -Seg d by A1, A100, Th27;
[d,c] in R by A100, A102, Th1;
then A104: d in field R by RELAT_1:15;
then R -Seg d c= R -Seg c by A1, A94, A100, A102, Th30;
then S |_2 (S -Seg b),R |_2 (R -Seg d) are_isomorphic by A101, A96, A103, A98, Th22;
then R |_2 (R -Seg d),S |_2 (S -Seg b) are_isomorphic by Th40;
then [d,b] in F by A9, A97, A104;
then ( d in dom F & b = F . d ) by FUNCT_1:1;
hence b in rng F by FUNCT_1:def 3; :: thesis: verum
end;
hence b in rng F by A88; :: thesis: verum
end;
A105: now :: thesis: ( rng F = field S & ex a being object st
( a in field R & Z = R -Seg a ) implies ex a being object st
( a in field R & R |_2 (R -Seg a),S are_isomorphic ) )
assume A106: rng F = field S ; :: thesis: ( ex a being object st
( a in field R & Z = R -Seg a ) implies ex a being object st
( a in field R & R |_2 (R -Seg a),S are_isomorphic ) )
given a being object such that A107: a in field R and
A108: Z = R -Seg a ; :: thesis: ex a being object st
( a in field R & R |_2 (R -Seg a),S are_isomorphic )
take a = a; :: thesis: ( a in field R & R |_2 (R -Seg a),S are_isomorphic )
thus a in field R by A107; :: thesis: R |_2 (R -Seg a),S are_isomorphic
thus R |_2 (R -Seg a),S are_isomorphic by A82, A106, A108, Th23; :: thesis: verum
end;
now :: thesis: ( Z = field R & rng F = field S implies R,S are_isomorphic )
assume A109: ( Z = field R & rng F = field S ) ; :: thesis: R,S are_isomorphic
( R |_2 (field R) = R & S |_2 (field S) = S ) by Th23;
hence R,S are_isomorphic by A10, A17, A109; :: thesis: verum
end;
hence ( R,S are_isomorphic or ex a being object st
( a in field R & R |_2 (R -Seg a),S are_isomorphic ) or ex a being object st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) ) by A1, A2, A4, A15, A66, A87, A61, A83, A105, Th28; :: thesis: verum