:: The Well Ordering Relations
:: by Grzegorz Bancerek
::
:: Received April 4, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RELAT_1, RELAT_2, XBOOLE_0, SUBSET_1, TARSKI, FUNCT_1, ZFMISC_1,
WELLORD1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1;
constructors TARSKI, SUBSET_1, FUNCT_1, RELAT_2, XTUPLE_0;
registrations FUNCT_1, RELAT_1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, FUNCT_1, RELAT_1;
equalities TARSKI, XBOOLE_0, RELAT_1;
expansions TARSKI, XBOOLE_0, FUNCT_1;
theorems TARSKI, XBOOLE_0, FUNCT_1, RELAT_1, RELAT_2, ZFMISC_1, XBOOLE_1,
XTUPLE_0;
schemes XBOOLE_0, FUNCT_1;
begin
reserve a,b,c,d,x,y,z for object, X,Y,Z for set;
reserve R,S,T for Relation;
Lm1: R is reflexive iff for x st x in field R holds [x,x] in R
by RELAT_2:def 1,def 9;
Lm2: R is transitive iff for x,y,z st [x,y] in R & [y,z] in R holds [x,z] in R
proof
thus R is transitive implies for x,y,z st [x,y] in R & [y,z] in R holds [x,z
] in R
proof
assume R is transitive;
then
A1: R is_transitive_in field R by RELAT_2:def 16;
let x,y,z;
assume that
A2: [x,y] in R and
A3: [y,z] in R;
A4: z in field R by A3,RELAT_1:15;
x in field R & y in field R by A2,RELAT_1:15;
hence thesis by A1,A2,A3,A4,RELAT_2:def 8;
end;
assume for x,y,z st [x,y] in R & [y,z] in R holds [x,z] in R;
then
for x,y,z st x in field R & y in field R & z in field R & [x,y] in R & [
y,z] in R holds [x,z] in R;
then R is_transitive_in field R by RELAT_2:def 8;
hence thesis by RELAT_2:def 16;
end;
Lm3: R is antisymmetric iff for x,y st [x,y] in R & [y,x] in R holds x = y
proof
thus R is antisymmetric implies for x,y st [x,y] in R & [y,x] in R holds x =
y
proof
assume R is antisymmetric;
then
A1: R is_antisymmetric_in field R by RELAT_2:def 12;
let x,y;
assume that
A2: [x,y] in R and
A3: [y,x] in R;
x in field R & y in field R by A2,RELAT_1:15;
hence thesis by A1,A2,A3,RELAT_2:def 4;
end;
assume for x,y st [x,y] in R & [y,x] in R holds x = y;
then
for x,y st x in field R & y in field R & [x,y] in R & [y,x] in R holds x = y;
then R is_antisymmetric_in field R by RELAT_2:def 4;
hence thesis by RELAT_2:def 12;
end;
Lm4: R is connected iff for x,y st x in field R & y in field R & x <> y holds
[x,y] in R or [y,x] in R by RELAT_2:def 6,def 14;
definition
let R; let a be object;
func R-Seg(a) -> set equals
Coim(R,a) \ {a};
coherence;
end;
theorem Th1:
x in R-Seg a iff x <> a & [x,a] in R
proof
hereby
assume
A1: x in R-Seg a;
hence x <> a by ZFMISC_1:56;
ex y being object st [x,y] in R & y in {a} by A1,RELAT_1:def 14;
hence [x,a] in R by TARSKI:def 1;
end;
assume that
A2: x <> a and
A3: [x,a] in R;
a in {a} by TARSKI:def 1;
then x in Coim(R,a) by A3,RELAT_1:def 14;
hence thesis by A2,ZFMISC_1:56;
end;
theorem Th2:
x in field R or R-Seg(x) = {}
proof
assume
A1: not x in field R;
set y = the Element of R-Seg(x);
assume R-Seg(x) <> {};
then [y,x] in R by Th1;
hence contradiction by A1,RELAT_1:15;
end;
definition
let R;
attr R is well_founded means
:Def2:
for Y st Y c= field R & Y <> {} ex a st a in Y & R-Seg a misses Y;
let X;
pred R is_well_founded_in X means
for Y st Y c= X & Y <> {} ex a st a in Y & R-Seg a misses Y;
end;
theorem
R is well_founded iff R is_well_founded_in field R;
definition
let R;
attr R is well-ordering means
R is reflexive & R is transitive & R is
antisymmetric & R is connected & R is well_founded;
let X;
pred R well_orders X means
R is_reflexive_in X & R is_transitive_in X
& R is_antisymmetric_in X & R is_connected_in X & R is_well_founded_in X;
end;
registration
cluster well-ordering ->
reflexive transitive antisymmetric connected well_founded
for Relation;
coherence;
cluster reflexive transitive antisymmetric connected well_founded
-> well-ordering for Relation;
coherence;
end;
theorem
R well_orders field R iff R is well-ordering
proof
thus R well_orders field R implies R is well-ordering
proof
assume R is_reflexive_in field R & R is_transitive_in field R & R
is_antisymmetric_in field R & R is_connected_in field R & R is_well_founded_in
field R;
hence R is reflexive & R is transitive & R is antisymmetric & R is
connected & R is well_founded by RELAT_2:def 9,def 12,def 14,def 16;
end;
assume R is reflexive & R is transitive & R is antisymmetric & R is
connected & R is well_founded;
hence R is_reflexive_in field R & R is_transitive_in field R & R
is_antisymmetric_in field R & R is_connected_in field R & R is_well_founded_in
field R by RELAT_2:def 9,def 12,def 14,def 16;
end;
theorem
R well_orders X implies for Y st Y c= X & Y <> {} ex a st a in Y & for
b st b in Y holds [a,b] in R
proof
assume
A1: R well_orders X;
then
A2: R is_reflexive_in X;
A3: R is_connected_in X by A1;
let Y;
assume that
A4: Y c= X and
A5: Y <> {};
R is_well_founded_in X by A1;
then consider a such that
A6: a in Y and
A7: R-Seg(a) misses Y by A4,A5;
take a;
thus a in Y by A6;
let b;
assume
A8: b in Y;
then not b in R-Seg(a) by A7,XBOOLE_0:3;
then a = b or not [b,a] in R by Th1;
then a <> b implies [a,b] in R by A3,A4,A6,A8,RELAT_2:def 6;
hence thesis by A2,A4,A6,RELAT_2:def 1;
end;
theorem Th6:
R is well-ordering implies for Y st Y c= field R & Y <> {} ex a
st a in Y & for b st b in Y holds [a,b] in R
proof
assume
A1: R is well-ordering;
let Y;
assume that
A2: Y c= field R and
A3: Y <> {};
consider a such that
A4: a in Y and
A5: R-Seg(a) misses Y by A1,A2,A3,Def2;
take a;
thus a in Y by A4;
let b;
assume
A6: b in Y;
then not b in R-Seg(a) by A5,XBOOLE_0:3;
then a = b or not [b,a] in R by Th1;
then a <> b implies [a,b] in R by A1,A2,A4,A6,Lm4;
hence thesis by A1,A2,A4,Lm1;
end;
theorem
for R st R is well-ordering & field R <> {} ex a st a in field R & for
b st b in field R holds [a,b] in R by Th6;
theorem
for R st R is well-ordering for a st a in field R holds (for b st b in
field R holds [b,a] in R) or ex b st b in field R & [a,b] in R & for c st c in
field R & [a,c] in R holds c = a or [b,c] in R
proof
let R;
assume
A1: R is well-ordering;
let a such that
A2: a in field R;
defpred P[object] means not [$1,a] in R;
given b such that
A3: b in field R & not [b,a] in R;
consider Z such that
A4: for c being object holds c in Z iff c in field R & P[c]
from XBOOLE_0:sch 1;
for b being object holds b in Z implies b in field R by A4;
then
A5: Z c= field R;
Z <> {} by A3,A4;
then consider d such that
A6: d in Z and
A7: for c st c in Z holds [d,c] in R by A1,A5,Th6;
take d;
thus
A8: d in field R by A4,A6;
A9: not [d,a] in R by A4,A6;
then a <> d by A6,A7;
hence [a,d] in R by A1,A2,A8,A9,Lm4;
let c;
assume that
A10: c in field R and
A11: [a,c] in R;
assume c <> a;
then not [c,a] in R by A1,A11,Lm3;
then c in Z by A4,A10;
hence thesis by A7;
end;
reserve F,G for Function;
theorem Th9:
R-Seg(a) c= field R
proof
let b be object;
assume b in R-Seg(a);
then [b,a] in R by Th1;
hence thesis by RELAT_1:15;
end;
definition
let R,Y;
func R |_2 Y -> Relation equals
R /\ [:Y,Y:];
coherence;
end;
theorem Th10:
R |_2 X = X|`R|X
proof
let x,y be object;
thus [x,y] in R |_2 X implies [x,y] in X|`R|X
proof
assume
A1: [x,y] in R |_2 X;
then
A2: [x,y] in [:X,X:] by XBOOLE_0:def 4;
then
A3: x in X by ZFMISC_1:87;
A4: y in X by A2,ZFMISC_1:87;
[x,y] in R by A1,XBOOLE_0:def 4;
then [x,y] in X|`R by A4,RELAT_1:def 12;
hence thesis by A3,RELAT_1:def 11;
end;
assume
A5: [x,y] in X|`R|X;
then
A6: [x,y] in X|`R by RELAT_1:def 11;
then
A7: [x,y] in R by RELAT_1:def 12;
A8: y in X by A6,RELAT_1:def 12;
x in X by A5,RELAT_1:def 11;
then [x,y] in [:X,X:] by A8,ZFMISC_1:87;
hence thesis by A7,XBOOLE_0:def 4;
end;
theorem Th11:
R |_2 X = X|`(R|X)
proof
thus R |_2 X = X|`R|X by Th10
.= X|`(R|X) by RELAT_1:109;
end;
Lm5: dom(X|`R) c= dom R
proof
let x be object;
assume x in dom(X|`R);
then consider y being object such that
A1: [x,y] in X|`R by XTUPLE_0:def 12;
[x,y] in R by A1,RELAT_1:def 12;
hence thesis by XTUPLE_0:def 12;
end;
theorem Th12:
x in field(R |_2 X) implies x in field R & x in X
proof
A1: dom(X|`R|X) = dom(X|`R) /\ X & rng(X|`(R|X)) = rng(R|X) /\ X
by RELAT_1:61,88;
assume x in field(R |_2 X);
then
A2: x in dom(R |_2 X) or x in rng(R |_2 X) by XBOOLE_0:def 3;
A3: dom(X|`R) c= dom R & rng(R|X) c= rng R by Lm5,RELAT_1:70;
R |_2 X = X|`R|X & R |_2 X = X|`(R|X) by Th10,Th11;
then x in dom(X|`R) & x in X or x in rng(R|X) & x in X
by A2,A1,XBOOLE_0:def 4;
hence thesis by A3,XBOOLE_0:def 3;
end;
theorem Th13:
field(R |_2 X) c= field R & field(R |_2 X) c= X
by Th12;
theorem Th14:
(R |_2 X)-Seg(a) c= R-Seg(a)
proof
let x be object;
assume
A1: x in (R |_2 X)-Seg(a);
then [x,a] in R |_2 X by Th1;
then
A2: [x,a] in R by XBOOLE_0:def 4;
x <> a by A1,Th1;
hence thesis by A2,Th1;
end;
theorem Th15:
R is reflexive implies R |_2 X is reflexive
proof
assume
A1: R is reflexive;
now
let a;
assume
A2: a in field(R |_2 X);
then a in X by Th12;
then
A3: [a,a] in [:X,X:] by ZFMISC_1:87;
a in field R by A2,Th12;
then [a,a] in R by A1,Lm1;
hence [a,a] in R |_2 X by A3,XBOOLE_0:def 4;
end;
hence thesis by Lm1;
end;
theorem Th16:
R is connected implies R |_2 Y is connected
proof
assume
A1: R is connected;
now
let a,b;
assume that
A2: a in field(R |_2 Y) & b in field(R |_2 Y) and
A3: a <> b;
a in Y & b in Y by A2,Th12;
then
A4: [a,b] in [:Y,Y:] & [b,a] in [:Y,Y:] by ZFMISC_1:87;
a in field R & b in field R by A2,Th12;
then [a,b] in R or [b,a] in R by A1,A3,Lm4;
hence [a,b] in R |_2 Y or [b,a] in R |_2 Y by A4,XBOOLE_0:def 4;
end;
hence thesis by Lm4;
end;
theorem Th17:
R is transitive implies R |_2 Y is transitive
proof
assume
A1: R is transitive;
now
let a,b,c;
assume that
A2: [a,b] in R |_2 Y and
A3: [b,c] in R |_2 Y;
[a,b] in R & [b,c] in R by A2,A3,XBOOLE_0:def 4;
then
A4: [a,c] in R by A1,Lm2;
[b,c] in [:Y,Y:] by A3,XBOOLE_0:def 4;
then
A5: c in Y by ZFMISC_1:87;
[a,b] in [:Y,Y:] by A2,XBOOLE_0:def 4;
then a in Y by ZFMISC_1:87;
then [a,c] in [:Y,Y:] by A5,ZFMISC_1:87;
hence [a,c] in R |_2 Y by A4,XBOOLE_0:def 4;
end;
hence thesis by Lm2;
end;
theorem Th18:
R is antisymmetric implies R |_2 Y is antisymmetric
proof
assume
A1: R is antisymmetric;
now
let a,b;
assume [a,b] in R |_2 Y & [b,a] in R |_2 Y;
then [a,b] in R & [b,a] in R by XBOOLE_0:def 4;
hence a = b by A1,Lm3;
end;
hence thesis by Lm3;
end;
theorem Th19:
(R |_2 X) |_2 Y = R |_2 (X /\ Y)
proof
thus (R |_2 X) |_2 Y = R /\ ([:X,X:] /\ [:Y,Y:]) by XBOOLE_1:16
.= R |_2 (X /\ Y) by ZFMISC_1:100;
end;
theorem
(R |_2 X) |_2 Y = (R |_2 Y) |_2 X
proof
thus (R |_2 X) |_2 Y = R |_2 (Y /\ X) by Th19
.= (R |_2 Y) |_2 X by Th19;
end;
theorem
(R |_2 Y) |_2 Y = R |_2 Y
proof
let a,b be object;
thus [a,b] in (R |_2 Y) |_2 Y implies [a,b] in R |_2 Y by XBOOLE_0:def 4;
assume
A1: [a,b] in R |_2 Y;
then [a,b] in [:Y,Y:] by XBOOLE_0:def 4;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem Th22:
Z c= Y implies (R |_2 Y) |_2 Z = R |_2 Z
proof
assume
A1: Z c= Y;
let a,b be object;
thus [a,b] in (R |_2 Y) |_2 Z implies [a,b] in R |_2 Z
proof
assume
A2: [a,b] in (R |_2 Y) |_2 Z;
then [a,b] in R |_2 Y by XBOOLE_0:def 4;
then
A3: [a,b] in R by XBOOLE_0:def 4;
[a,b] in [:Z,Z:] by A2,XBOOLE_0:def 4;
hence thesis by A3,XBOOLE_0:def 4;
end;
assume
A4: [a,b] in R |_2 Z;
then
A5: [a,b] in R by XBOOLE_0:def 4;
A6: [a,b] in [:Z,Z:] by A4,XBOOLE_0:def 4;
then a in Z & b in Z by ZFMISC_1:87;
then [a,b] in [:Y,Y:] by A1,ZFMISC_1:87;
then [a,b] in R |_2 Y by A5,XBOOLE_0:def 4;
hence thesis by A6,XBOOLE_0:def 4;
end;
theorem Th23:
R |_2 field R = R
proof
let x,y be object;
thus [x,y] in R |_2 field R implies [x,y] in R by XBOOLE_0:def 4;
assume
A1: [x,y] in R;
then x in field R & y in field R by RELAT_1:15;
then [x,y] in [:field R,field R:] by ZFMISC_1:87;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem Th24:
R is well_founded implies R |_2 X is well_founded
proof
assume
A1: for Y st Y c= field R & Y <> {} ex a st a in Y & R-Seg(a) misses Y;
A2: field(R |_2 X) c= field R by Th13;
let Y;
assume Y c= field(R |_2 X) & Y <> {};
then consider a such that
A3: a in Y and
A4: R-Seg(a) misses Y by A1,A2,XBOOLE_1:1;
take a;
thus a in Y by A3;
assume not thesis;
then
A5: ex b being object st b in (R |_2 X)-Seg(a) & b in Y by XBOOLE_0:3;
(R |_2 X)-Seg(a) c= R-Seg(a) by Th14;
hence contradiction by A4,A5,XBOOLE_0:3;
end;
theorem Th25:
R is well-ordering implies R |_2 Y is well-ordering
by Th15,Th16,Th17,Th18,Th24;
theorem Th26:
R is well-ordering implies R-Seg(a),R-Seg(b) are_c=-comparable
proof
assume
A1: R is well-ordering;
A2: now
assume
A3: a in field R & b in field R;
now
assume a <> b;
A4: now
assume
A5: [b,a] in R;
now
let c be object;
assume
A6: c in R-Seg(b);
then
A7: [c,b] in R by Th1;
then
A8: [c,a] in R by A1,A5,Lm2;
c <> b by A6,Th1;
then c <> a by A1,A5,A7,Lm3;
hence c in R-Seg(a) by A8,Th1;
end;
hence R-Seg(b) c= R-Seg(a);
end;
now
assume
A9: [a,b] in R;
now
let c be object;
assume
A10: c in R-Seg(a);
then
A11: [c,a] in R by Th1;
then
A12: [c,b] in R by A1,A9,Lm2;
c <> a by A10,Th1;
then c <> b by A1,A9,A11,Lm3;
hence c in R-Seg(b) by A12,Th1;
end;
hence R-Seg(a) c= R-Seg(b);
end;
hence thesis by A1,A3,A4,Lm4;
end;
hence thesis;
end;
now
assume R-Seg(a) = {} or R-Seg(b) = {};
then R-Seg(a) c= R-Seg(b) or R-Seg(b) c= R-Seg(a);
hence thesis;
end;
hence thesis by A2,Th2;
end;
theorem Th27:
R is well-ordering & b in R-Seg(a) implies (R |_2 (R-Seg(a)))
-Seg(b) = R-Seg(b)
proof
assume that
A1: R is well-ordering and
A2: b in R-Seg(a);
set S = R |_2 (R-Seg(a));
now
let c be object;
assume
A3: c in R-Seg(b);
then
A4: [c,b] in R by Th1;
A5: [b,a] in R by A2,Th1;
then
A6: [c,a] in R by A1,A4,Lm2;
A7: c <> b by A3,Th1;
then c <> a by A1,A4,A5,Lm3;
then c in R-Seg(a) by A6,Th1;
then [c,b] in [:R-Seg(a),R-Seg(a):] by A2,ZFMISC_1:87;
then [c,b] in S by A4,XBOOLE_0:def 4;
hence c in S-Seg(b) by A7,Th1;
end;
then
A8: R-Seg(b) c= S-Seg(b);
now
let c be object;
assume
A9: c in S-Seg(b);
then [c,b] in S by Th1;
then
A10: [c,b] in R by XBOOLE_0:def 4;
c <> b by A9,Th1;
hence c in R-Seg(b) by A10,Th1;
end;
then S-Seg(b) c= R-Seg(b);
hence thesis by A8;
end;
theorem Th28:
R is well-ordering & Y c= field R implies (Y = field R or (ex a
st a in field R & Y = R-Seg(a) ) iff for a st a in Y for b st [b,a] in R holds
b in Y )
proof
assume that
A1: R is well-ordering and
A2: Y c= field R;
now
given a such that
a in field R and
A3: Y = R-Seg(a);
let b such that
A4: b in Y;
A5: [b,a] in R by A3,A4,Th1;
let c such that
A6: [c,b] in R;
A7: [c,a] in R by A1,A6,A5,Lm2;
b <> a by A3,A4,Th1;
then c <> a by A1,A6,A5,Lm3;
hence c in Y by A3,A7,Th1;
end;
hence Y = field R or (ex a st a in field R & Y = R-Seg(a) ) implies for a st
a in Y for b st [b,a] in R holds b in Y by RELAT_1:15;
assume
A8: for a st a in Y for b st [b,a] in R holds b in Y;
assume Y <> field R;
then ex d being object st not ( d in field R iff d in Y ) by TARSKI:2;
then field R \ Y <> {} by A2,XBOOLE_0:def 5;
then consider a such that
A9: a in field R \ Y and
A10: for b st b in field R \ Y holds [a,b] in R by A1,Th6;
A11: now
let b be object;
assume
A12: b in R-Seg(a);
then
A13: [b,a] in R by Th1;
assume
A14: not b in Y;
b in field R by A13,RELAT_1:15;
then b in field R \ Y by A14,XBOOLE_0:def 5;
then
A15: [a,b] in R by A10;
b <> a by A12,Th1;
hence contradiction by A1,A13,A15,Lm3;
end;
take a;
thus a in field R by A9;
now
A16: not a in Y by A9,XBOOLE_0:def 5;
let b be object;
assume
A17: b in Y;
assume not b in R-Seg(a);
then
A18: not [b,a] in R or a = b by Th1;
a <> b by A9,A17,XBOOLE_0:def 5;
then [a,b] in R by A2,A1,A9,A17,A18,Lm4;
hence contradiction by A8,A17,A16;
end;
hence Y = R-Seg(a) by A11,TARSKI:2;
end;
theorem Th29:
R is well-ordering & a in field R & b in field R implies ( [a,b]
in R iff R-Seg(a) c= R-Seg(b) )
proof
assume that
A1: R is well-ordering and
A2: a in field R and
A3: b in field R;
thus [a,b] in R implies R-Seg(a) c= R-Seg(b)
proof
assume
A4: [a,b] in R;
let c be object;
assume
A5: c in R-Seg(a);
then
A6: [c,a] in R by Th1;
then
A7: [c,b] in R by A1,A4,Lm2;
c <> a by A5,Th1;
then c <> b by A1,A4,A6,Lm3;
hence thesis by A7,Th1;
end;
assume
A8: R-Seg(a) c= R-Seg(b);
now
assume
A9: a <> b;
assume not [a,b] in R;
then [b,a] in R by A2,A3,A1,A9,Lm4;
then b in R-Seg(a) by A9,Th1;
hence contradiction by A8,Th1;
end;
hence thesis by A1,A2,Lm1;
end;
theorem Th30:
R is well-ordering & a in field R & b in field R implies ( R-Seg
(a) c= R-Seg(b) iff a = b or a in R-Seg(b) )
proof
assume
A1: R is well-ordering & a in field R & b in field R;
thus R-Seg(a) c= R-Seg(b) implies a = b or a in R-Seg(b)
proof
assume R-Seg(a) c= R-Seg(b);
then [a,b] in R by A1,Th29;
hence thesis by Th1;
end;
now
assume a in R-Seg(b);
then [a,b] in R by Th1;
hence R-Seg(a) c= R-Seg(b) by A1,Th29;
end;
hence thesis;
end;
theorem Th31:
R is well-ordering & X c= field R implies field(R |_2 X) = X
proof
assume that
A1: R is well-ordering and
A2: X c= field R;
thus field(R |_2 X) c= X by Th13;
let x be object;
assume
A3: x in X;
then
A4: [x,x] in [:X,X:] by ZFMISC_1:87;
[x,x] in R by A1,A2,A3,Lm1;
then [x,x] in R |_2 X by A4,XBOOLE_0:def 4;
hence thesis by RELAT_1:15;
end;
theorem Th32:
R is well-ordering implies field(R |_2 R-Seg(a)) = R-Seg(a)
proof
R-Seg(a) c= field R by Th9;
hence thesis by Th31;
end;
theorem Th33:
R is well-ordering implies for Z st for a st a in field R & R
-Seg(a) c= Z holds a in Z holds field R c= Z
proof
assume
A1: R is well-ordering;
let Z such that
A2: for a st a in field R & R-Seg(a) c= Z holds a in Z;
A3: now
let a such that
A4: a in field R and
A5: for b st [b,a] in R & a <> b holds b in Z;
now
let b be object;
assume b in R-Seg(a);
then [b,a] in R & b <> a by Th1;
hence b in Z by A5;
end;
then R-Seg(a) c= Z;
hence a in Z by A2,A4;
end;
given a being object such that
A6: a in field R & not a in Z;
field R \ Z <> {} by A6,XBOOLE_0:def 5;
then consider a such that
A7: a in field R \ Z and
A8: for b st b in field R \ Z holds [a,b] in R by A1,Th6;
not a in Z by A7,XBOOLE_0:def 5;
then consider b such that
A9: [b,a] in R and
A10: b <> a and
A11: not b in Z by A3,A7;
b in field R by A9,RELAT_1:15;
then b in field R \ Z by A11,XBOOLE_0:def 5;
then [a,b] in R by A8;
hence contradiction by A1,A9,A10,Lm3;
end;
theorem Th34:
R is well-ordering & a in field R & b in field R & (for c st c
in R-Seg(a) holds [c,b] in R & c <> b) implies [a,b] in R
proof
assume that
A1: R is well-ordering & a in field R & b in field R and
A2: c in R-Seg(a) implies [c,b] in R & c <> b;
assume
A3: not [a,b] in R;
a <> b by A1,A3,Lm1;
then [b,a] in R by A1,A3,Lm4;
then b in R-Seg(a) by A3,Th1;
hence contradiction by A2;
end;
theorem Th35:
R is well-ordering & dom F = field R & rng F c= field R & (for a
,b st [a,b] in R & a <> b holds [F.a,F.b] in R & F.a <> F.b) implies for a st a
in field R holds [a,F.a] in R
proof
assume that
A1: R is well-ordering & dom F = field R & rng F c= field R and
A2: [a,b] in R & a <> b implies [F.a,F.b] in R & F.a <> F.b;
defpred P[object] means [$1,F.$1] in R;
consider Z such that
A3: for a being object holds a in Z iff a in field R & P[a]
from XBOOLE_0:sch 1;
now
let a;
assume
A4: a in field R;
assume
A5: R-Seg(a) c= Z;
A6: now
let b;
assume
A7: b in R-Seg(a);
then
A8: [b,F.b] in R by A3,A5;
A9: [b,a] in R & b <> a by A7,Th1;
then
A10: [F.b,F.a] in R by A2;
hence [b,F.a] in R by A1,A8,Lm2;
F.b <> F.a by A2,A9;
hence b <> F.a by A1,A8,A10,Lm3;
end;
F.a in rng F by A1,A4,FUNCT_1:def 3;
then [a,F.a] in R by A1,A4,A6,Th34;
hence a in Z by A3,A4;
end;
then
A11: field R c= Z by A1,Th33;
let a;
assume a in field R;
hence thesis by A3,A11;
end;
definition
let R,S,F;
pred F is_isomorphism_of R,S means
dom F = field R & rng F = field S
& F is one-to-one & for a,b holds [a,b] in R iff a in field R & b in field R &
[F.a,F.b] in S;
end;
theorem Th36:
F is_isomorphism_of R,S implies for a,b st [a,b] in R & a <> b
holds [F.a,F.b] in S & F.a <> F.b
proof
assume
A1: F is_isomorphism_of R,S;
then
A2: dom F = field R & F is one-to-one;
let a,b;
assume that
A3: [a,b] in R and
A4: a <> b;
a in field R & b in field R by A1,A3;
hence thesis by A1,A2,A3,A4;
end;
definition
let R,S;
pred R,S are_isomorphic means
ex F st F is_isomorphism_of R,S;
end;
theorem Th37:
id(field R) is_isomorphism_of R,R
proof
A1: now
let a,b;
thus [a,b] in R implies a in field R & b in field R & [id(field R).a,id(
field R).b] in R
proof
assume
A2: [a,b] in R;
hence
A3: a in field R & b in field R by RELAT_1:15;
then id(field R).a = a by FUNCT_1:18;
hence thesis by A2,A3,FUNCT_1:18;
end;
assume that
A4: a in field R and
A5: b in field R & [id(field R).a,id(field R).b] in R;
id(field R).a = a by A4,FUNCT_1:18;
hence [a,b] in R by A5,FUNCT_1:18;
end;
thus thesis by A1;
end;
theorem
R,R are_isomorphic
proof
take id(field R);
thus thesis by Th37;
end;
theorem Th39:
F is_isomorphism_of R,S implies F" is_isomorphism_of S,R
proof
assume
A1: F is_isomorphism_of R,S;
then
A2: F is one-to-one;
A3: rng F = field S by A1;
hence
A4: dom(F") = field S by A2,FUNCT_1:33;
dom F = field R by A1;
hence rng(F") = field R by A2,FUNCT_1:33;
thus F" is one-to-one by A2;
let a,b;
thus [a,b] in S implies a in field S & b in field S & [F".a,F".b] in R
proof
A5: dom F = rng(F") by A2,FUNCT_1:33;
assume
A6: [a,b] in S;
hence
A7: a in field S & b in field S by RELAT_1:15;
then
A8: F".a in rng(F") & F".b in rng(F") by A4,FUNCT_1:def 3;
a = F.(F".a) & b = F.(F".b) by A3,A2,A7,FUNCT_1:35;
hence thesis by A1,A6,A5,A8;
end;
assume that
A9: a in field S & b in field S and
A10: [F".a,F".b] in R;
F.(F".a) = a & F.(F".b) = b by A3,A2,A9,FUNCT_1:35;
hence thesis by A1,A10;
end;
theorem Th40:
R,S are_isomorphic implies S,R are_isomorphic
proof
given F such that
A1: F is_isomorphism_of R,S;
take F";
thus thesis by A1,Th39;
end;
theorem Th41:
F is_isomorphism_of R,S & G is_isomorphism_of S,T implies G*F
is_isomorphism_of R,T
proof
assume that
A1: dom F = field R and
A2: rng F = field S and
A3: F is one-to-one and
A4: for a,b holds [a,b] in R iff a in field R & b in field R & [F.a,F.b] in S;
assume that
A5: dom G = field S and
A6: rng G = field T and
A7: G is one-to-one and
A8: for a,b holds [a,b] in S iff a in field S & b in field S & [G.a,G.b] in T;
thus dom(G*F) = field R by A1,A2,A5,RELAT_1:27;
thus rng(G*F) = field T by A2,A5,A6,RELAT_1:28;
thus G*F is one-to-one by A3,A7;
let a,b;
thus [a,b] in R implies a in field R & b in field R & [(G*F).a,(G*F).b] in T
proof
assume
A9: [a,b] in R;
hence a in field R & b in field R by RELAT_1:15;
then
A10: (G*F).a = G.(F.a) & (G*F).b = G.(F.b) by A1,FUNCT_1:13;
[F.a,F.b] in S by A4,A9;
hence thesis by A8,A10;
end;
assume that
A11: a in field R & b in field R and
A12: [(G*F).a,(G*F).b] in T;
A13: (G*F).a = G.(F.a) & (G*F).b = G.(F.b) by A1,A11,FUNCT_1:13;
F.a in field S & F.b in field S by A1,A2,A11,FUNCT_1:def 3;
then [F.a,F.b] in S by A8,A12,A13;
hence thesis by A4,A11;
end;
theorem Th42:
R,S are_isomorphic & S,T are_isomorphic implies R,T are_isomorphic
proof
given F such that
A1: F is_isomorphism_of R,S;
given G such that
A2: G is_isomorphism_of S,T;
take G*F;
thus thesis by A1,A2,Th41;
end;
theorem Th43:
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 )
proof
assume
A1: F is_isomorphism_of R,S;
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
proof
assume
A6: R is reflexive;
now
let a;
assume
A7: a in field 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;
end;
hence thesis by Lm1;
end;
thus R is transitive implies S is transitive
proof
assume
A9: R is transitive;
now
let a,b,c;
assume that
A10: [a,b] in S and
A11: [b,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,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;
end;
hence thesis by Lm2;
end;
thus R is connected implies S is connected
proof
assume
A18: R is connected;
now
let a,b;
assume that
A19: a in field S & b in field S and
A20: a <> b;
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;
end;
hence thesis by Lm4;
end;
thus R is antisymmetric implies S is antisymmetric
proof
assume
A22: R is antisymmetric;
now
let a,b;
assume that
A23: [a,b] in S and
A24: [b,a] in S;
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;
end;
hence thesis by Lm3;
end;
assume
A30: for Y st Y c= field R & Y <> {} ex x st x in Y & R-Seg(x) misses Y;
let Z;
assume that
A31: Z c= field S and
A32: Z <> {};
A33: F"Z c= dom F by RELAT_1:132;
then consider x 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;
thus F.x in Z by A34,FUNCT_1:def 7;
assume not thesis;
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;
end;
theorem Th44:
R is well-ordering & F is_isomorphism_of R,S implies S is well-ordering
by Th43;
theorem Th45:
R is well-ordering implies for F,G st F is_isomorphism_of R,S &
G is_isomorphism_of R,S holds F = G
proof
assume
A1: R is well-ordering;
let F,G;
assume that
A2: F is_isomorphism_of R,S and
A3: G is_isomorphism_of R,S;
A4: dom F = field R by A2;
A5: S is well-ordering by A1,A2,Th44;
A6: rng F = field S by A2;
A7: G is one-to-one by A3;
A8: dom G = field R by A3;
A9: G" is_isomorphism_of S,R by A3,Th39;
then
A10: G" is one-to-one;
A11: F is one-to-one by A2;
A12: rng G = field S by A3;
A13: F" is_isomorphism_of S,R by A2,Th39;
then
A14: F" is one-to-one;
for a being object st a in field R holds F.a = G.a
proof
A15: dom(F") = field S by A6,A11,FUNCT_1:33;
then
A16: dom(F"*G) = field R by A8,A12,RELAT_1:27;
A17: now
let a,b;
assume that
A18: [a,b] in R and
A19: a <> b;
A20: [G.a,G.b] in S by A3,A18;
A21: b in field R by A18,RELAT_1:15;
then
A22: F".(G.b) = (F"*G).b by A8,FUNCT_1:13;
A23: a in field R by A18,RELAT_1:15;
then F".(G.a) = (F"*G).a by A8,FUNCT_1:13;
hence [(F"*G).a,(F"*G).b] in R by A13,A20,A22;
thus (F"*G).a <> (F"*G).b by A14,A7,A16,A19,A23,A21,FUNCT_1:def 4;
end;
A24: dom(G") = field S by A12,A7,FUNCT_1:33;
then
A25: dom(G"*F) = field R by A4,A6,RELAT_1:27;
A26: now
let a,b;
assume that
A27: [a,b] in R and
A28: a <> b;
A29: [F.a,F.b] in S by A2,A27;
A30: b in field R by A27,RELAT_1:15;
then
A31: G".(F.b) = (G"*F).b by A4,FUNCT_1:13;
A32: a in field R by A27,RELAT_1:15;
then G".(F.a) = (G"*F).a by A4,FUNCT_1:13;
hence [(G"*F).a,(G"*F).b] in R by A9,A29,A31;
thus (G"*F).a <> (G"*F).b by A11,A10,A25,A28,A32,A30,FUNCT_1:def 4;
end;
let a being object such that
A33: a in field R;
A34: F".(G.a) = (F"*G).a by A8,A33,FUNCT_1:13;
G.a in rng F by A6,A8,A12,A33,FUNCT_1:def 3;
then
A35: F.(F".(G.a)) = G.a by A11,FUNCT_1:35;
rng(F") = field R by A4,A11,FUNCT_1:33;
then rng(F"*G) = field R by A12,A15,RELAT_1:28;
then [a,(F"*G).a] in R by A1,A33,A16,A17,Th35;
then
A36: [F.a,G.a] in S by A2,A34,A35;
F.a in rng G by A4,A6,A12,A33,FUNCT_1:def 3;
then
A37: G.(G".(F.a)) = F.a by A7,FUNCT_1:35;
A38: G".(F.a) = (G"*F).a by A4,A33,FUNCT_1:13;
rng(G") = field R by A8,A7,FUNCT_1:33;
then rng(G"*F) = field R by A6,A24,RELAT_1:28;
then [a,(G"*F).a] in R by A1,A33,A25,A26,Th35;
then [G.a,F.a] in S by A3,A38,A37;
hence thesis by A5,A36,Lm3;
end;
hence thesis by A4,A8;
end;
definition
let R,S;
assume that
A1: R is well-ordering and
A2: R,S are_isomorphic;
func canonical_isomorphism_of(R,S) -> Function means
:Def9:
it is_isomorphism_of R,S;
existence by A2;
uniqueness by A1,Th45;
end;
theorem Th46:
R is well-ordering implies for a st a in field R holds
not R,R |_2 (R-Seg(a)) are_isomorphic
proof
assume
A1: R is well-ordering;
let a such that
A2: a in field R;
set S = R |_2 (R-Seg(a));
set F = canonical_isomorphism_of(R,S);
assume R,R |_2 (R-Seg(a)) are_isomorphic;
then
A3: F is_isomorphism_of R,S by A1,Def9;
then
A4: dom F = field R;
A5: F is one-to-one by A3;
A6: now
let b,c;
assume that
A7: [b,c] in R and
A8: b <> c;
[F.b,F.c] in R |_2 (R-Seg(a)) by A3,A7;
hence [F.b,F.c] in R by XBOOLE_0:def 4;
b in field R & c in field R by A7,RELAT_1:15;
hence F.b <> F.c by A4,A5,A8;
end;
A9: rng F = field S by A3;
field S = R-Seg(a) by A1,Th32;
then F.a in R-Seg(a) by A2,A4,A9,FUNCT_1:def 3;
then
A10: [F.a,a] in R & F.a <> a by Th1;
rng F c= field R by A9,Th13;
then [a,F.a] in R by A1,A2,A4,A6,Th35;
hence contradiction by A1,A10,Lm3;
end;
theorem Th47:
R is well-ordering & a in field R & b in field R & a <> b
implies not R |_2 (R-Seg(a)),R |_2 (R-Seg(b)) are_isomorphic
proof
assume that
A1: R is well-ordering and
A2: a in field R & b in field R and
A3: a <> b;
A4: now
set S = R |_2 (R-Seg(a));
assume
A5: R-Seg(b) c= R-Seg(a);
then
A6: S |_2 (R-Seg(b)) = R |_2 (R-Seg(b)) by Th22;
A7: field S = R-Seg(a) by A1,Th32;
A8: b in R-Seg(a)
proof
assume not b in R-Seg(a);
then not [b,a] in R by A3,Th1;
then [a,b] in R by A2,A3,A1,Lm4;
then a in R-Seg(b) by A3,Th1;
hence contradiction by A5,Th1;
end;
then R-Seg(b) = S-Seg(b) by A1,Th27;
hence thesis by A1,A7,A8,A6,Th25,Th46;
end;
A9: now
set S = R |_2 (R-Seg(b));
assume
A10: R-Seg(a) c= R-Seg(b);
then
A11: S |_2 (R-Seg(a)) = R |_2 (R-Seg(a)) by Th22;
A12: field S = R-Seg(b) & S is well-ordering by A1,Th25,Th32;
A13: a in R-Seg(b)
proof
assume not a in R-Seg(b);
then not [a,b] in R by A3,Th1;
then [b,a] in R by A2,A3,A1,Lm4;
then b in R-Seg(a) by A3,Th1;
hence contradiction by A10,Th1;
end;
then R-Seg(a) = S-Seg(a) by A1,Th27;
hence thesis by A13,A11,A12,Th40,Th46;
end;
R-Seg(a),R-Seg(b) are_c=-comparable by A1,Th26;
hence thesis by A9,A4;
end;
theorem Th48:
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
proof
assume that
A1: R is well-ordering and
A2: Z c= field R and
A3: F is_isomorphism_of R,S;
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)
proof
thus
A9: dom(F|Z) = field(R |_2 Z) by A2,A8,A7,RELAT_1:62;
thus
A10: rng(F|Z) = field(S |_2 (F.:Z)) by A5,RELAT_1:115;
thus F|Z is one-to-one by A6,FUNCT_1:52;
let a,b;
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)
proof
assume
A11: [a,b] in R |_2 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;
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 thesis by A12,A14,XBOOLE_0:def 4;
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);
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 thesis by A18,XBOOLE_0:def 4;
end;
hence thesis;
end;
theorem Th49:
F is_isomorphism_of R,S implies for a st a in field R ex b st b
in field S & F.:(R-Seg(a)) = S-Seg(b)
proof
assume
A1: F is_isomorphism_of R,S;
then
A2: dom F = field R;
let a;
assume
A3: a in field R;
take b = F.a;
A4: rng F = field S by A1;
hence b in field S by A3,A2,FUNCT_1:def 3;
A5: F is one-to-one by A1;
A6: for c being object holds c in S-Seg(b) implies c in F.:(R-Seg(a))
proof let c be object;
assume
A7: c in S-Seg(b);
then
A8: c <> b by Th1;
A9: [c,b] in S by A7,Th1;
then
A10: c in field S by RELAT_1:15;
then
A11: c = F.(F".c) by A4,A5,FUNCT_1:35;
rng(F") = dom F & dom(F") = rng F by A5,FUNCT_1:33;
then
A12: F".c in field R by A2,A4,A10,FUNCT_1:def 3;
then [F".c,a] in R by A1,A3,A9,A11;
then F".c in R-Seg(a) by A8,A11,Th1;
hence thesis by A2,A11,A12,FUNCT_1:def 6;
end;
for c being object holds c in F.:(R-Seg(a)) implies c in S-Seg(b)
proof let c be object;
assume c in F.:(R-Seg(a));
then consider d being object such that
A13: d in dom F and
A14: d in R-Seg(a) and
A15: c = F.d by FUNCT_1:def 6;
[d,a] in R by A14,Th1;
then
A16: [c,b] in S by A1,A15;
d <> a by A14,Th1;
then c <> b by A3,A2,A5,A13,A15;
hence thesis by A16,Th1;
end;
hence thesis by A6,TARSKI:2;
end;
theorem Th50:
R is well-ordering & F is_isomorphism_of R,S implies for a st a
in field R ex b st b in field S & R |_2 (R-Seg(a)),S |_2 (S-Seg(b))
are_isomorphic
proof
assume that
A1: R is well-ordering and
A2: F is_isomorphism_of R,S;
let a;
assume a in field R;
then consider b such that
A3: b in field S & F.:(R-Seg(a)) = S-Seg(b) by A2,Th49;
take b;
R-Seg(a) c= field R by Th9;
hence thesis by A1,A2,A3,Th48;
end;
theorem Th51:
R is well-ordering & S is well-ordering & a in field R & b in
field S & c in field S & R,S |_2 (S-Seg(b)) are_isomorphic & R |_2 (R-Seg(a)),S
|_2 (S-Seg(c)) are_isomorphic implies S-Seg(c) c= S-Seg(b) & [c,b] in S
proof
assume that
A1: R is well-ordering and
A2: S is well-ordering and
A3: a in field R and
A4: b in field S and
A5: c in field S and
A6: R,S |_2 (S-Seg(b)) are_isomorphic and
A7: R |_2 (R-Seg(a)),S |_2 (S-Seg(c)) are_isomorphic;
set Q = S |_2 (S-Seg(b));
set F1 = canonical_isomorphism_of(R,Q);
A8: F1 is_isomorphism_of R,Q by A1,A6,Def9;
then consider d such that
A9: d in field Q and
A10: F1.:(R-Seg(a)) = Q-Seg(d) by A3,Th49;
A11: S-Seg(b) = field Q by A2,Th32;
then
A12: Q-Seg(d) = S-Seg(d) by A2,A9,Th27;
A13: rng F1 = S-Seg(b) by A8,A11;
then
A14: Q-Seg(d) c= S-Seg(b) by A10,RELAT_1:111;
set T = S |_2 (S-Seg(c));
set P = R |_2 (R-Seg(a));
A15: T,P are_isomorphic by A7,Th40;
A16: d in field S by A9,Th12;
R-Seg(a) c= field R by Th9;
then P,Q |_2 (F1.:(R-Seg(a))) are_isomorphic by A1,A8,Th48;
then T,Q |_2 (Q-Seg(d)) are_isomorphic by A10,A15,Th42;
then T,S |_2 (S-Seg(d)) are_isomorphic by A10,A12,A13,Th22,RELAT_1:111;
hence S-Seg(c) c= S-Seg(b) by A2,A5,A12,A14,A16,Th47;
hence thesis by A2,A4,A5,Th29;
end;
theorem Th52:
R is well-ordering & S is well-ordering implies R,S
are_isomorphic or (ex a st a in field R & R |_2 (R-Seg(a)),S are_isomorphic )
or ex a st a in field S & R,S |_2 (S-Seg(a)) are_isomorphic
proof
assume that
A1: R is well-ordering and
A2: S is well-ordering;
defpred P[object] means
ex b st b in field S & R |_2 (R-Seg($1)),S |_2 (S-Seg(b
)) are_isomorphic;
consider Z such that
A3: for a being object holds a in Z iff a in field R & P[a]
from XBOOLE_0:sch 1;
A4: Z c= field R
by A3;
defpred P[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 P[a, b] & P[a, c] holds b = c
proof
let a,b,c be object;
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;
S |_2 (S-Seg(b)),R |_2 (R-Seg(a)) are_isomorphic by A7,Th40;
hence thesis by A2,A6,A8,Th42,Th47;
end;
consider F such that
A9: for a,b being object holds [a,b] in F iff a in field R & P[a,b]
from FUNCT_1:sch 1(A5);
A10: Z = dom F
proof
thus for a being object holds a in Z implies a in dom F
proof let a be object;
assume
A11: a in Z;
then consider b 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 thesis by XTUPLE_0:def 12;
end;
let a be object;
assume a in dom F;
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 thesis by A3,A14;
end;
A15: rng F c= field S
proof
let a be object;
assume a in rng F;
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 thesis by A9;
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;
thus
A18: F is one-to-one
proof
let a,b be object;
assume that
A19: a in dom F and
A20: b in dom F and
A21: F.a = F.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 thesis by A1,A24,A23,Th42,Th47;
end;
let a,b;
set P = R |_2 (R-Seg(a));
A25: field P = R-Seg(a) & P 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)
proof
assume
A26: [a,b] in R |_2 (dom F);
hence
A27: a in field(R |_2 (dom F)) & b in field(R |_2 (dom F)) by RELAT_1:15;
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
set P = R |_2 (R-Seg(b));
A41: field P = R-Seg(b) & P is well-ordering by A1,Th25,Th32;
assume a <> b;
then
A42: a in R-Seg(b) by A35,Th1;
then P-Seg(a) = R-Seg(a) by A1,Th27;
then P |_2(P-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 thesis by A37,XBOOLE_0:def 4;
end;
a = b implies thesis
proof
assume a = b;
then [F.a,F.b] in S by A2,A30,Lm1;
hence thesis by A37,XBOOLE_0:def 4;
end;
hence thesis by A40;
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);
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);
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 P-Seg(b) = R-Seg(b) by A1,Th27;
then
A59: P |_2 (P-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;
end;
A61: now
given a such that
A62: a in field R and
A63: Z = R-Seg(a);
given b such that
A64: b in field S and
A65: rng F = S-Seg(b);
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;
end;
A66: now
let a such that
A67: a in Z;
consider c 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 such that
A70: [b,a] in R;
A71: a in field R by A3,A67;
now
set Q = S |_2 (S-Seg(c));
set P = R |_2 (R-Seg(a));
P is well-ordering by A1,Th25;
then
A72: canonical_isomorphism_of(P,Q) is_isomorphism_of P,Q by A69,Def9;
assume a <> b;
then
A73: b in R-Seg(a) by A70,Th1;
then
A74: P-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: P |_2 (R-Seg(b)) = R |_2 (R-Seg(b)) by Th22;
field P = R-Seg(a) by A1,Th32;
then consider d such that
A77: d in field Q and
A78: P |_2 (P-Seg(b)),Q |_2 (Q-Seg(d)) are_isomorphic by A1,A72,A73,Th25,Th50;
A79: S-Seg(c) = field Q by A2,Th32;
then
A80: Q-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;
end;
hence b in Z by A67;
end;
A82: R |_2 Z,S |_2 (rng F) are_isomorphic by A10,A17;
A83: now
assume
A84: Z = field R;
given a such that
A85: a in field S and
A86: rng F = S-Seg(a);
take a;
thus a in field S by A85;
thus R,S |_2 (S-Seg(a)) are_isomorphic by A82,A84,A86,Th23;
end;
A87: now
let a such that
A88: a 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 such that
A92: [b,a] in S;
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
set Q = S |_2 (S-Seg(a));
set P = R |_2 (R-Seg(c));
assume a <> b;
then
A95: b in S-Seg(a) by A92,Th1;
then
A96: Q-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: Q |_2 (S-Seg(b)) = S |_2 (S-Seg(b)) by Th22;
Q,P are_isomorphic & Q is well-ordering by A2,A93,Th25,Th40;
then
A99: canonical_isomorphism_of(Q,P) is_isomorphism_of Q,P by Def9;
field Q = S-Seg(a) by A2,Th32;
then consider d such that
A100: d in field P and
A101: Q |_2 (Q-Seg(b)),P |_2 (P-Seg(d)) are_isomorphic by A2,A99,A95,Th25,Th50;
A102: R-Seg(c) = field P by A1,Th32;
then
A103: P-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;
end;
hence b in rng F by A88;
end;
A105: now
assume
A106: rng F = field S;
given a such that
A107: a in field R and
A108: Z = R-Seg(a);
take a;
thus a in field R by A107;
thus R |_2 (R-Seg(a)),S are_isomorphic by A82,A106,A108,Th23;
end;
now
assume
A109: Z = field R & rng F = field S;
R |_2 field R = R & S |_2 field S = S by Th23;
hence R,S are_isomorphic by A10,A17,A109;
end;
hence thesis by A1,A2,A4,A15,A66,A87,A61,A83,A105,Th28;
end;
theorem
Y c= field R & R is well-ordering implies R,R |_2 Y are_isomorphic or
ex a st a in field R & R |_2 (R-Seg(a)),R |_2 Y are_isomorphic
proof
assume that
A1: Y c= field R and
A2: R is well-ordering;
A3: now
given a such that
A4: a in field(R |_2 Y) and
A5: R,(R |_2 Y) |_2 ((R |_2 Y)-Seg(a)) are_isomorphic;
consider F such that
A6: F is_isomorphism_of R,(R |_2 Y) |_2 ((R |_2 Y)-Seg(a)) by A5;
A7: now
let c,b;
assume
A8: [c,b] in R & c <> b;
then [F.c,F.b] in (R |_2 Y) |_2 ((R |_2 Y)-Seg(a)) by A6;
then [F.c,F.b] in R |_2 Y by XBOOLE_0:def 4;
hence [F.c,F.b] in R & F.c <> F.b by A6,A8,Th36,XBOOLE_0:def 4;
end;
A9: field(R |_2 Y) = Y by A1,A2,Th31;
field((R |_2 Y) |_2 ((R |_2 Y)-Seg(a))) = (R |_2 Y)-Seg(a) by A2,Th25,Th32;
then
A10: rng F = (R |_2 Y)-Seg(a) by A6;
A11: dom F = field R by A6;
then
A12: F.a in rng F by A1,A4,A9,FUNCT_1:def 3;
then
A13: F.a <> a by A10,Th1;
[F.a,a] in R |_2 Y by A10,A12,Th1;
then
A14: [F.a,a] in R by XBOOLE_0:def 4;
(R |_2 Y)-Seg(a) c= Y by A9,Th9;
then rng F c= field R by A1,A10;
then [a,F.a] in R by A1,A2,A4,A9,A11,A7,Th35;
hence contradiction by A13,A14,A2,Lm3;
end;
R |_2 Y is well-ordering by A2,Th25;
hence thesis by A2,A3,Th52;
end;
:: from AMISTD_3, 2010.01.10, A.T.
theorem
R,S are_isomorphic & R is well-ordering implies S is well-ordering
by Th44;