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