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