:: Zermelo's Theorem
:: by Bogdan Nowak and S{\l}awomir Bia{\l}ecki
::
:: Received October 27, 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, FUNCT_1, XBOOLE_0, ZFMISC_1, SUBSET_1, WELLORD1,
RELAT_2, TARSKI;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1,
WELLORD1;
constructors TARSKI, SUBSET_1, RELAT_2, WELLORD1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1;
requirements SUBSET, BOOLE;
definitions TARSKI, WELLORD1;
equalities TARSKI, WELLORD1;
expansions TARSKI, WELLORD1;
theorems TARSKI, FUNCT_1, RELAT_1, RELAT_2, ZFMISC_1, WELLORD1, ENUMSET1,
XBOOLE_0, XBOOLE_1, XTUPLE_0;
schemes TARSKI, FUNCT_1, RELAT_1, XBOOLE_0, XFAMILY;
begin
reserve a,b,x,y,z,z1,z2,z3,y1,y3,y4,A,B,C,D,G,M,N,X,Y,Z,W0,W00 for set,
R,S,T, W,W1,W2 for Relation,
F,H,H1 for Function;
theorem Th1:
for x being object holds
x in field R iff ex y being object st ([x,y] in R or [y,x] in R)
proof let x be object;
x in (dom R \/ rng R) iff x in dom R or x in rng R by XBOOLE_0:def 3;
hence thesis by RELAT_1:def 6,XTUPLE_0:def 12,def 13;
end;
theorem Th2:
X <> {} & Y <> {} & W = [: X,Y :] implies field W = X \/ Y
proof
set a = the Element of X,b = the Element of Y;
assume that
A1: X <> {} and
A2: Y <> {} and
A3: W = [: X,Y :];
A4: for x being object holds x in field W implies x in X \/ Y
proof let x be object;
assume x in field W;
then consider y being object such that
A5: [x,y] in W or [y,x] in W by Th1;
A6: [y,x] in W implies x in X \/ Y
proof
assume [y,x] in W;
then x in Y by A3,ZFMISC_1:87;
hence thesis by XBOOLE_0:def 3;
end;
[x,y] in W implies x in X \/ Y
proof
assume [x,y] in W;
then x in X by A3,ZFMISC_1:87;
hence thesis by XBOOLE_0:def 3;
end;
hence thesis by A5,A6;
end;
for x being object holds x in X \/ Y implies x in field W
proof let x be object;
A7: x in X implies x in field W
proof
assume x in X;
then [x,b] in W by A2,A3,ZFMISC_1:87;
hence thesis by Th1;
end;
A8: x in Y implies x in field W
proof
assume x in Y;
then [a,x] in W by A1,A3,ZFMISC_1:87;
hence thesis by Th1;
end;
assume x in X \/ Y;
hence thesis by A7,A8,XBOOLE_0:def 3;
end;
hence thesis by A4,TARSKI:2;
end;
scheme
RSeparation { A()-> set, P[Relation] } :
ex B st for R being Relation holds R in B iff R in A() & P[R];
defpred p[object,object] means $1 = $2 & ex S st S = $2 & P[S];
A1: for y,t,v being object st p[y,t] & p[y,v] holds t = v;
consider B such that
A2: for t being object holds t in B
iff ex y being object st y in A() & p[y,t]
from TARSKI:sch 1(A1);
take B;
let R;
R in B implies ex T st T in A() & T = R & P[R]
proof
assume R in B;
then consider y being object such that
A3: y in A() and
A4: y = R and
A5: ex S st S = R & P[S] by A2;
reconsider y as Relation by A4;
take y;
thus thesis by A3,A4,A5;
end;
hence R in B implies R in A() & P[R];
thus thesis by A2;
end;
theorem Th3:
for x,y,W st x in field W & y in field W & W is well-ordering
holds not x in W-Seg(y) implies [y,x] in W
proof
let x,y,W;
assume that
A1: x in field W and
A2: y in field W and
A3: W is well-ordering;
W is connected by A3;
then W is_connected_in field W by RELAT_2:def 14;
then
A4: x<>y implies [x,y] in W or [y,x] in W by A1,A2,RELAT_2:def 6;
W is reflexive by A3;
then
A5: W is_reflexive_in field W by RELAT_2:def 9;
assume not x in W-Seg(y);
hence thesis by A1,A5,A4,RELAT_2:def 1,WELLORD1:1;
end;
theorem Th4:
for x,y,W st x in field W & y in field W & W is well-ordering
holds x in W-Seg(y) implies not [y,x] in W
proof
let x,y,W;
assume that
A1: x in field W & y in field W and
A2: W is well-ordering;
W is antisymmetric by A2;
then
A3: W is_antisymmetric_in field W by RELAT_2:def 12;
assume x in W-Seg(y);
then
A4: x<>y & [x,y] in W by WELLORD1:1;
assume [y,x] in W;
hence contradiction by A1,A3,A4,RELAT_2:def 4;
end;
theorem Th5:
for F,D st (for X st X in D holds not F.X in X & F.X in union D)
ex R st field R c= union D & R is well-ordering & not field R in D & for y st y
in field R holds R-Seg(y) in D & F.(R-Seg(y)) = y
proof
let F,D;
assume
A1: for X st X in D holds not F.X in X & F.X in union D;
defpred P[Relation] means $1 is well-ordering & for y st y in field $1 holds
$1-Seg(y) in D & F.($1-Seg(y)) = y;
set W0=bool [: union D, union D :];
consider G such that
A2: W in G iff W in W0 & P[W] from RSeparation;
defpred P[object,object] means ex W st [$1,$2] in W & W in G;
consider S such that
A3: for x,y being object holds
[x,y] in S iff x in union D & y in union D & P[x,y] from RELAT_1:
sch 1;
take R = S;
A4: x in field R implies x in union D & ex W st x in field W & W in G
proof
assume x in field R;
then consider y being object such that
A5: [x,y] in R or [y,x] in R by Th1;
(x in union D & y in union D & ex S st [x,y] in S & S in G) or (y in
union D & x in union D & ex S st [y,x] in S & S in G) by A3,A5;
then consider S such that
A6: ( [x,y] in S or [y,x] in S)& S in G;
thus x in union D by A3,A5;
take S;
thus thesis by A6,Th1;
end;
then for x being object holds x in field R implies x in union D;
hence field R c= union D;
A7: for W1,W2 holds W1 in G & W2 in G implies ((W1 c= W2 & for x st x in
field W1 holds W1-Seg(x) = W2-Seg(x) ) or (W2 c= W1 & for x st x in field W2
holds W2-Seg(x) = W1-Seg(x) ))
proof
let W1,W2;
assume that
A8: W1 in G and
A9: W2 in G;
A10: W2 is well-ordering by A2,A9;
defpred P[set] means $1 in field W2 & W1 |_2 (W1-Seg($1)) = W2 |_2 (W2-Seg
($1));
consider C such that
A11: x in C iff x in field W1 & P[x] from XFAMILY:sch 1;
A12: W1 is well-ordering by A2,A8;
A13: x in C implies W1-Seg(x) = W2-Seg(x)
proof
assume
A14: x in C;
for y being object holds y in W1-Seg(x) iff y in W2-Seg(x)
proof
let y be object;
field (W1 |_2(W1-Seg(x))) = W1-Seg(x) & field (W2 |_2(W2-Seg(x)))
= W2-Seg(x ) by A12,A10,WELLORD1:32;
hence thesis by A11,A14;
end;
hence thesis by TARSKI:2;
end;
A15: x in C implies W1-Seg(x) c= C
proof
assume
A16: x in C;
for y being object holds y in W1-Seg(x) implies y in C
proof let y be object;
assume
A17: y in W1-Seg(x);
then
A18: y in W2-Seg(x) by A13,A16;
then
A19: [y,x] in W2 by WELLORD1:1;
then
A20: y in field W2 by RELAT_1:15;
A21: W1-Seg(y)=(W1 |_2 (W1-Seg(x)))-Seg(y) by A12,A17,WELLORD1:27
.=(W2 |_2 (W2-Seg(x)))-Seg(y) by A11,A16
.=W2-Seg(y) by A10,A18,WELLORD1:27;
A22: [y,x] in W1 by A17,WELLORD1:1;
then
A23: y in field W1 by RELAT_1:15;
x in field W2 by A19,RELAT_1:15;
then
A24: W2-Seg(y) c= W2-Seg(x) by A10,A18,A20,WELLORD1:30;
x in field W1 by A22,RELAT_1:15;
then W1-Seg(y) c= W1-Seg(x) by A12,A17,A23,WELLORD1:30;
then W1 |_2 (W1-Seg(y)) = (W1 |_2 (W1-Seg(x))) |_2 (W1-Seg(y)) by
WELLORD1:22
.= (W2 |_2 (W2-Seg(x))) |_2 (W2-Seg(y)) by A11,A16,A21
.= W2 |_2 (W2-Seg(y)) by A24,WELLORD1:22;
hence thesis by A11,A23,A20;
end;
hence thesis;
end;
A25: for y1 being object holds
y1 in field W1 & not y1 in C implies ex y3 st y3 in field W1 & C=W1
-Seg(y3) & not y3 in C
proof let y1 be object;
set Y = field W1 \ C;
assume y1 in field W1 & not y1 in C;
then Y <> {} by XBOOLE_0:def 5;
then consider a being object such that
A26: a in Y and
A27: for b being object st b in Y holds [a,b] in W1 by A12,WELLORD1:6;
take y3=a;
for x being object holds x in C iff x in W1-Seg(y3)
proof let x be object;
thus x in C implies x in W1-Seg(y3)
proof
assume that
A28: x in C and
A29: not x in W1-Seg(y3);
x in field W1 by A11,A28;
then
A30: [y3,x] in W1 by A12,A26,A29,Th3;
A31: W1-Seg(x) c= C by A15,A28;
y3 <> x implies y3 in C
by A30,WELLORD1:1,A31;
hence contradiction by A26,A28,XBOOLE_0:def 5;
end;
thus x in W1-Seg(y3) implies x in C
proof
assume that
A32: x in W1-Seg(y3) and
A33: not x in C;
[x,y3] in W1 by A32,WELLORD1:1;
then
A34: x in field W1 by RELAT_1:15;
then x in Y by A33,XBOOLE_0:def 5;
then [y3,x] in W1 by A27;
hence contradiction by A12,A26,A32,A34,Th4;
end;
end;
hence thesis by A26,TARSKI:2,XBOOLE_0:def 5;
end;
A35: x in C implies W2-Seg(x) c= C
proof
assume
A36: x in C;
let y be object;
assume
A37: y in W2-Seg(x);
then
A38: y in W1-Seg(x) by A13,A36;
then
A39: [y,x] in W1 by WELLORD1:1;
then
A40: y in field W1 by RELAT_1:15;
A41: W2-Seg(y)=(W2 |_2 (W2-Seg(x)))-Seg(y) by A10,A37,WELLORD1:27
.=(W1 |_2 (W1-Seg(x)))-Seg(y) by A11,A36
.=W1-Seg(y) by A12,A38,WELLORD1:27;
A42: [y,x] in W2 by A37,WELLORD1:1;
then
A43: y in field W2 by RELAT_1:15;
x in field W1 by A39,RELAT_1:15;
then
A44: W1-Seg(y) c= W1-Seg(x) by A12,A38,A40,WELLORD1:30;
x in field W2 by A42,RELAT_1:15;
then W2-Seg(y) c= W2-Seg(x) by A10,A37,A43,WELLORD1:30;
then W2 |_2 (W2-Seg(y)) = (W2 |_2 (W2-Seg(x))) |_2 (W2-Seg(y)) by
WELLORD1:22
.= (W1 |_2 (W1-Seg(x))) |_2 (W1-Seg(y)) by A11,A36,A41
.= W1 |_2 (W1-Seg(y)) by A44,WELLORD1:22;
hence thesis by A11,A43,A40;
end;
A45: y1 in field W2 & not y1 in C implies ex y3 st y3 in field W2 & C=W2
-Seg(y3) & not y3 in C
proof
set Y = field W2 \ C;
assume y1 in field W2 & not y1 in C;
then Y <> {} by XBOOLE_0:def 5;
then consider a being object such that
A46: a in Y and
A47: for b being object st b in Y holds [a,b] in W2 by A10,WELLORD1:6;
take y3=a;
for x being object holds x in C iff x in W2-Seg(y3)
proof let x be object;
thus x in C implies x in W2-Seg(y3)
proof
assume that
A48: x in C and
A49: not x in W2-Seg(y3);
x in field W2 by A11,A48;
then
A50: [y3,x] in W2 by A10,A46,A49,Th3;
A51: W2-Seg(x) c= C by A35,A48;
y3 <> x implies y3 in C
by A50,WELLORD1:1,A51;
hence contradiction by A46,A48,XBOOLE_0:def 5;
end;
thus x in W2-Seg(y3) implies x in C
proof
assume that
A52: x in W2-Seg(y3) and
A53: not x in C;
[x,y3] in W2 by A52,WELLORD1:1;
then
A54: x in field W2 by RELAT_1:15;
then x in Y by A53,XBOOLE_0:def 5;
then [y3,x] in W2 by A47;
hence contradiction by A10,A46,A52,A54,Th4;
end;
end;
hence thesis by A46,TARSKI:2,XBOOLE_0:def 5;
end;
A55: C = field W1 or C = field W2
proof
assume not C = field W1;
then ex x being object
st not (x in C implies x in field W1) or not (x in field W1
implies x in C) by TARSKI:2;
then consider y3 such that
A56: y3 in field W1 and
A57: C=W1-Seg(y3) and
A58: not y3 in C by A11,A25;
assume not C = field W2;
then ex x being object
st not (x in C implies x in field W2) or not (x in field W2
implies x in C) by TARSKI:2;
then consider y4 such that
A59: y4 in field W2 and
A60: C=W2-Seg(y4) and
not y4 in C by A11,A45;
A61: y3 = F.(W2-Seg(y4)) by A2,A8,A56,A57,A60
.= y4 by A2,A9,A59;
for z being object holds
z in W1 |_2 (W1-Seg(y3)) iff z in W2 |_2 (W2-Seg(y3))
proof let z be object;
A62: z in W1 & z in [: W1-Seg(y3),W1-Seg(y3) :] implies z in W2 & z in
[: W2-Seg(y3),W2-Seg(y3) :]
proof
assume that
A63: z in W1 and
A64: z in [: W1-Seg(y3),W1-Seg(y3) :];
consider z1,z2 being object such that
A65: z1 in W1-Seg(y3) and
A66: z2 in W1-Seg(y3) and
A67: z=[z1,z2] by A64,ZFMISC_1:def 2;
z1 in W1-Seg(z2) or z1=z2 & not z1 in W1-Seg(z2) by A63,A67,
WELLORD1:1;
then
A68: z1 in W2-Seg(z2) or z1=z2 & not z1 in W2-Seg(z2) by A13,A57,A66;
z1 in field W2 by A11,A57,A65;
hence thesis by A10,A57,A60,A61,A64,A67,A68,Th3,WELLORD1:1;
end;
z in W2 & z in [: W2-Seg(y3),W2-Seg(y3) :] implies z in W1 & z
in [: W1-Seg(y3),W1-Seg(y3) :]
proof
assume that
A69: z in W2 and
A70: z in [: W2-Seg(y3),W2-Seg(y3) :];
consider z1,z2 being object such that
A71: z1 in W2-Seg(y3) and
A72: z2 in W2-Seg(y3) and
A73: z=[z1,z2] by A70,ZFMISC_1:def 2;
z1 in W2-Seg(z2) or z1=z2 & not z1 in W2-Seg(z2) by A69,A73,
WELLORD1:1;
then
A74: z1 in W1-Seg(z2) or z1=z2 & not z1 in W1-Seg(z2) by A13,A60,A61,A72;
z1 in field W1 by A11,A60,A61,A71;
hence thesis by A12,A57,A60,A61,A70,A73,A74,Th3,WELLORD1:1;
end;
hence thesis by A62,XBOOLE_0:def 4;
end;
then W1 |_2 (W1-Seg(y3)) = W2 |_2 (W2-Seg(y3)) by TARSKI:2;
hence contradiction by A11,A56,A58,A59,A61;
end;
A75: C = field W2 implies (W2 c= W1 & for x st x in field W2 holds W2-Seg
(x) = W1-Seg(x) )
proof
assume
A76: C = field W2;
for z1,z2 being object holds [z1,z2] in W2 implies [z1,z2] in W1
proof let z1,z2 be object;
assume
A77: [z1,z2] in W2;
then
A78: z1 in W2-Seg(z2) or z1=z2 & not z1 in W2-Seg(z2) by WELLORD1:1;
z1 in C by A76,A77,RELAT_1:15;
then
A79: z1 in field W1 by A11;
z2 in C by A76,A77,RELAT_1:15;
then z1 in W1-Seg(z2) or z1=z2 & not z1 in W1-Seg(z2) by A13,A78;
hence thesis by A12,A79,Th3,WELLORD1:1;
end;
hence thesis by A13,A76,RELAT_1:def 3;
end;
C = field W1 implies (W1 c= W2 & for x st x in field W1 holds W1-Seg
(x) = W2-Seg(x) )
proof
assume
A80: C = field W1;
for z1,z2 being object holds [z1,z2] in W1 implies [z1,z2] in W2
proof let z1,z2 be object;
assume
A81: [z1,z2] in W1;
then
A82: z1 in W1-Seg(z2) or z1=z2 & not z1 in W1-Seg(z2) by WELLORD1:1;
z1 in C by A80,A81,RELAT_1:15;
then
A83: z1 in field W2 by A11;
z2 in C by A80,A81,RELAT_1:15;
then z1 in W2-Seg(z2) or z1=z2 & not z1 in W2-Seg(z2) by A13,A82;
hence thesis by A10,A83,Th3,WELLORD1:1;
end;
hence thesis by A13,A80,RELAT_1:def 3;
end;
hence thesis by A55,A75;
end;
A84: for x,y being object holds
x in field R & y in field R & [x,y] in R & [y,x] in R implies x=y
proof let x,y be object;
assume that
x in field R and
y in field R and
A85: [x,y] in R and
A86: [y,x] in R;
consider W1 such that
A87: [x,y] in W1 and
A88: W1 in G by A3,A85;
consider W2 such that
A89: [y,x] in W2 and
A90: W2 in G by A3,A86;
A91: W2 c= W1 implies x=y
proof
W1 is well-ordering by A2,A88;
then W1 well_orders field W1 by WELLORD1:4;
then
A92: W1 is_antisymmetric_in field W1;
assume
A93: W2 c= W1;
then x in field W1 & y in field W1 by A89,RELAT_1:15;
hence thesis by A87,A89,A93,A92,RELAT_2:def 4;
end;
W1 c= W2 implies x=y
proof
W2 is well-ordering by A2,A90;
then W2 well_orders field W2 by WELLORD1:4;
then
A94: W2 is_antisymmetric_in field W2;
assume
A95: W1 c= W2;
then x in field W2 & y in field W2 by A87,RELAT_1:15;
hence thesis by A87,A89,A95,A94,RELAT_2:def 4;
end;
hence thesis by A7,A88,A90,A91;
end;
then
A96: R is_antisymmetric_in field R by RELAT_2:def 4;
A97: W in G implies field W c= field R
proof
assume
A98: W in G;
let x be object;
assume x in field W;
then consider y being object such that
A99: [x,y] in W or [y,x] in W by Th1;
A100: [y,x] in W implies [y,x] in R
proof
assume
A101: [y,x] in W;
W in W0 by A2,A98;
then ex z1,z2 being object st
z1 in union D & z2 in union D & [y,x]=[z1,z2] by A101,
ZFMISC_1:84;
hence thesis by A3,A98,A101;
end;
[x,y] in W implies [x,y] in R
proof
assume
A102: [x,y] in W;
W in W0 by A2,A98;
then ex z1,z2 being object
st z1 in union D & z2 in union D & [x,y]=[z1,z2] by A102,
ZFMISC_1:84;
hence thesis by A3,A98,A102;
end;
hence thesis by A99,A100,Th1;
end;
A103: for y st y in field R holds R-Seg(y) in D & F.(R-Seg(y)) = y
proof
let y;
assume
A104: y in field R;
then consider W such that
A105: y in field W and
A106: W in G by A4;
A107: y in union D by A4,A104;
A108: field W c= field R by A97,A106;
A109: for x being object holds x in W-Seg(y) implies x in R-Seg(y)
proof let x be object;
assume
A110: x in W-Seg(y);
then
A111: [x,y] in W by WELLORD1:1;
then x in field W by RELAT_1:15;
then x in union D by A4,A108;
then
A112: [x,y] in R by A3,A106,A107,A111;
not x =y by A110,WELLORD1:1;
hence thesis by A112,WELLORD1:1;
end;
for x being object holds x in R-Seg(y) implies x in W-Seg(y)
proof let x be object;
assume
A113: x in R-Seg(y);
then [x,y] in R by WELLORD1:1;
then consider W1 such that
A114: [x,y] in W1 and
A115: W1 in G by A3;
A116: y in field W1 by A114,RELAT_1:15;
not x =y by A113,WELLORD1:1;
then x in W1-Seg(y) by A114,WELLORD1:1;
hence thesis by A7,A105,A106,A115,A116;
end;
then W-Seg(y) = R-Seg(y) by A109,TARSKI:2;
hence thesis by A2,A105,A106;
end;
A117: for x,y being object holds
x in field R & y in field R & x <>y implies [x,y] in R or [y,x] in R
proof let x,y be object;
assume that
A118: x in field R and
A119: y in field R and
A120: x <>y;
consider W2 such that
A121: y in field W2 and
A122: W2 in G by A4,A119;
consider W1 such that
A123: x in field W1 and
A124: W1 in G by A4,A118;
A125: x in union D & y in union D by A4,A118,A119;
A126: W2 c= W1 implies [x,y] in R or [y,x] in R
proof
W1 is well-ordering by A2,A124;
then W1 well_orders field W1 by WELLORD1:4;
then
A127: W1 is_connected_in field W1;
assume W2 c= W1;
then field W2 c= field W1 by RELAT_1:16;
then [x,y] in W1 or [y,x] in W1 by A120,A123,A121,A127,RELAT_2:def 6;
hence thesis by A3,A124,A125;
end;
W1 c= W2 implies [x,y] in R or [y,x] in R
proof
W2 is well-ordering by A2,A122;
then W2 well_orders field W2 by WELLORD1:4;
then
A128: W2 is_connected_in field W2;
assume W1 c= W2;
then field W1 c= field W2 by RELAT_1:16;
then [x,y] in W2 or [y,x] in W2 by A120,A123,A121,A128,RELAT_2:def 6;
hence thesis by A3,A125,A122;
end;
hence thesis by A7,A124,A122,A126;
end;
then
A129: R is_connected_in field R by RELAT_2:def 6;
A130: R is_well_founded_in field R
proof
let Y;
assume that
A131: Y c= field R and
A132: Y <> {};
set y = the Element of Y;
y in field R by A131,A132;
then consider W such that
A133: y in field W and
A134: W in G by A4;
W is well-ordering by A2,A134;
then W well_orders field W by WELLORD1:4;
then
A135: W is_well_founded_in field W;
set A = Y /\ field W;
A136: A c= field W by XBOOLE_1:17;
A <> {} by A132,A133,XBOOLE_0:def 4;
then consider a being object such that
A137: a in A and
A138: W-Seg(a) misses A by A135,A136;
ex b being object st b in Y & R-Seg(b) misses Y
proof
take b= a;
thus b in Y by A137,XBOOLE_0:def 4;
assume not thesis;
then consider x being object such that
A139: x in R-Seg(b) and
A140: x in Y by XBOOLE_0:3;
[x,b] in R by A139,WELLORD1:1;
then consider W1 such that
A141: [x,b] in W1 and
A142: W1 in G by A3;
A143: b in field W1 by A141,RELAT_1:15;
x<>b by A139,WELLORD1:1;
then x in W1-Seg(b) by A141,WELLORD1:1;
then
A144: x in W-Seg(a) by A7,A134,A136,A137,A142,A143;
then [x,a] in W by WELLORD1:1;
then x in field W by RELAT_1:15;
then x in A by A140,XBOOLE_0:def 4;
hence contradiction by A138,A144,XBOOLE_0:3;
end;
hence thesis;
end;
A145: for x,y,z being object holds
x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R
implies [x,z] in R
proof let x,y,z be object;
assume that
x in field R and
y in field R and
z in field R and
A146: [x,y] in R and
A147: [y,z] in R;
A148: x in union D & z in union D by A3,A146,A147;
consider W1 such that
A149: [x,y] in W1 and
A150: W1 in G by A3,A146;
consider W2 such that
A151: [y,z] in W2 and
A152: W2 in G by A3,A147;
ex W st [x,y] in W & [y,z] in W & W in G
proof
take W = W2;
A153: not x in W1-Seg(y) implies [x,y] in W
proof
A154: W1 is well-ordering by A2,A150;
then W1 well_orders field W1 by WELLORD1:4;
then
A155: W1 is_antisymmetric_in field W1;
W is well-ordering by A2,A152;
then W well_orders field W by WELLORD1:4;
then
A156: W is_reflexive_in field W;
A157: x in field W1 & y in field W1 by A149,RELAT_1:15;
assume not x in W1-Seg(y);
then [y,x] in W1 by A157,A154,Th3;
then
A158: x=y by A149,A157,A155,RELAT_2:def 4;
y in field W by A151,RELAT_1:15;
hence thesis by A158,A156,RELAT_2:def 1;
end;
y in field W1 & y in field W by A149,A151,RELAT_1:15;
then W1-Seg(y) = W-Seg(y) by A7,A150,A152;
hence thesis by A151,A152,A153,WELLORD1:1;
end;
then consider W such that
A159: [x,y] in W and
A160: [y,z] in W and
A161: W in G;
A162: z in field W by A160,RELAT_1:15;
W is well-ordering by A2,A161;
then W well_orders field W by WELLORD1:4;
then
A163: W is_transitive_in field W;
x in field W & y in field W by A159,RELAT_1:15;
then [x,z] in W by A159,A160,A163,A162,RELAT_2:def 8;
hence thesis by A3,A148,A161;
end;
then
A164: R is_transitive_in field R by RELAT_2:def 8;
A165:
for x being object holds x in field R implies [x,x] in R
proof let x be object;
assume
A166: x in field R;
then consider W such that
A167: x in field W and
A168: W in G by A4;
W is well-ordering by A2,A168;
then W well_orders field W by WELLORD1:4;
then W is_reflexive_in field W;
then
A169: [x,x] in W by A167,RELAT_2:def 1;
x in union D by A4,A166;
hence thesis by A3,A168,A169;
end;
A170: not field R in D
proof
set a0=F.(field R);
reconsider W3 = [: field R,{ a0 } :] as Relation;
reconsider W4 = { [a0,a0]} as Relation;
reconsider W1=R \/ [: field R,{ a0 }:] \/ {[ a0,a0 ]} as Relation;
{[ a0,a0 ]} c= W1 & [ a0,a0 ] in {[ a0,a0 ]} by TARSKI:def 1,XBOOLE_1:7;
then
A171: a0 in field W1 by RELAT_1:15;
field W4 = {a0,a0} by RELAT_1:17;
then
A172: field W4 = {a0}\/{a0} by ENUMSET1:1;
A173: field R = {} implies field W1 =field R \/ { a0 }
proof
assume
A174: field R = {};
A175: field W3 = {}
proof
set z3 = the Element of field W3;
assume field W3 <> {};
then ex z2 being object st [z3,z2] in W3 or [z2,z3] in W3 by Th1;
hence contradiction by A174,ZFMISC_1:90;
end;
field W1 =field (R \/ W3) \/ field W4 by RELAT_1:18;
then field W1 =field R \/ {} \/ {a0} by A172,A175,RELAT_1:18;
hence thesis;
end;
A176: field R <> {} implies field W1 =field R \/ { a0 }
proof
assume field R <> {};
then
A177: field W3 = field R \/ { a0 } by Th2;
field W1 =field (R \/ W3) \/ field W4 by RELAT_1:18;
then
field W1 =field R \/ (field R \/ { a0 }) \/ {a0} by A172,A177,RELAT_1:18;
then field W1 =(field R \/ field R) \/ { a0 } \/ {a0} by XBOOLE_1:4;
then field W1 =(field R \/ field R) \/ ({ a0 } \/ {a0}) by XBOOLE_1:4;
hence thesis;
end;
A178: x in field W1 implies x in field R or x = a0
proof
assume x in field W1;
then x in field R or x in {a0} by A176,A173,XBOOLE_0:def 3;
hence thesis by TARSKI:def 1;
end;
A179: for x,y being object holds
[x,y] in W1 iff [x,y] in R or [x,y] in W3 or [x,y] in W4
proof let x,y be object;
[x,y] in W1 iff ([x,y] in (R \/ W3) or [x,y] in W4) by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
for x,y being object holds
x in field W1 & y in field W1 & x <>y implies [x,y] in W1 or [y,x] in W1
proof let x,y be object;
assume that
A180: x in field W1 and
A181: y in field W1 and
A182: x <>y;
A183: not x in field R implies [x,y] in W1 or [y,x] in W1
proof
assume not x in field R;
then
A184: x = a0 by A178,A180;
A185: y in field R implies [x,y] in W1 or [y,x] in W1
proof
assume y in field R;
then [y,x] in W3 by A184,ZFMISC_1:106;
hence thesis by A179;
end;
y = a0 implies [x,y] in W1 or [y,x] in W1
proof
assume y = a0;
then [x,y] in W4 by A184,TARSKI:def 1;
hence thesis by A179;
end;
hence thesis by A178,A181,A185;
end;
A186: not y in field R implies [x,y] in W1 or [y,x] in W1
proof
assume not y in field R;
then
A187: y = a0 by A178,A181;
A188: x in field R implies [y,x] in W1 or [x,y] in W1
proof
assume x in field R;
then [x,y] in W3 by A187,ZFMISC_1:106;
hence thesis by A179;
end;
x = a0 implies [y,x] in W1 or [x,y] in W1
proof
assume x = a0;
then [y,x] in W4 by A187,TARSKI:def 1;
hence thesis by A179;
end;
hence thesis by A178,A180,A188;
end;
x in field R & y in field R implies [x,y] in W1 or [y,x] in W1
proof
assume x in field R & y in field R;
then [x,y] in R or [y,x] in R by A117,A182;
hence thesis by A179;
end;
hence thesis by A183,A186;
end;
then
A189: W1 is_connected_in field W1 by RELAT_2:def 6;
assume
A190: field R in D;
for x,y being object
holds [x,y] in W1 implies [x,y] in [: union D, union D :]
proof
let x,y be object;
assume
A191: [x,y] in W1;
then y in field W1 by RELAT_1:15;
then y in field R or y=a0 by A178;
then
A192: y in union D by A1,A4,A190;
x in field W1 by A191,RELAT_1:15;
then x in field R or x=a0 by A178;
then x in union D by A1,A4,A190;
hence thesis by A192,ZFMISC_1:def 2;
end;
then
A193: W1 c= [: union D,union D :] by RELAT_1:def 3;
A194: not a0 in field R by A1,A190;
A195: for x,y being object holds
[x,y] in W1 & y in field R implies [x,y] in R & x in field R
proof let x,y be object;
assume that
A196: [x,y] in W1 and
A197: y in field R;
A198: not [x,y] in W4
proof
assume [x,y] in W4;
then [x,y] = [a0,a0] by TARSKI:def 1;
hence contradiction by A194,A197,XTUPLE_0:1;
end;
not [x,y] in W3 by A194,A197,ZFMISC_1:106;
hence [x,y] in R by A179,A196,A198;
[x,y] in R or [x,y] in W3 or [x,y] in W4 by A179,A196;
hence thesis by A198,RELAT_1:15,ZFMISC_1:106;
end;
for x,y being object holds
x in field W1 & y in field W1 & [x,y] in W1 & [y,x] in W1 implies x= y
proof let x,y be object;
assume that
A199: x in field W1 and
A200: y in field W1 and
A201: [x,y] in W1 and
A202: [y,x] in W1;
A203: x in field R implies x=y
proof
assume
A204: x in field R;
then
A205: [y,x] in R by A195,A202;
A206: y in field R by A195,A202,A204;
then [x,y] in R by A195,A201;
hence thesis by A84,A204,A205,A206;
end;
A207: y in field R implies x=y
proof
assume
A208: y in field R;
then
A209: [x,y] in R by A195,A201;
A210: x in field R by A195,A201,A208;
then [y,x] in R by A195,A202;
hence thesis by A84,A208,A209,A210;
end;
y in field R or y =a0 by A178,A200;
hence thesis by A178,A199,A203,A207;
end;
then
A211: W1 is_antisymmetric_in field W1 by RELAT_2:def 4;
A212: y in field R implies W1-Seg(y) = R-Seg(y)
proof
assume
A213: y in field R;
A214: for x being object holds x in W1-Seg(y) implies x in R-Seg(y)
proof let x be object;
assume
A215: x in W1-Seg(y);
then [x,y] in W1 by WELLORD1:1;
then
A216: [x,y] in R by A195,A213;
x<>y by A215,WELLORD1:1;
hence thesis by A216,WELLORD1:1;
end;
for x being object holds x in R-Seg(y) implies x in W1-Seg(y)
proof let x be object;
assume
A217: x in R-Seg(y);
then [x,y] in R by WELLORD1:1;
then
A218: [x,y] in W1 by A179;
x<>y by A217,WELLORD1:1;
hence thesis by A218,WELLORD1:1;
end;
hence thesis by A214,TARSKI:2;
end;
A219: W1 is_well_founded_in field W1
proof
let Y;
assume that
A220: Y c= field W1 and
A221: Y <> {};
A222: not Y c=field R implies ex a st a in Y & W1-Seg(a) misses Y
proof
assume not Y c= field R;
A223: not (field R) /\ Y = {} implies ex a st a in Y & W1-Seg(a) misses Y
proof
set X = (field R) /\ Y;
A224: X c= field R by XBOOLE_1:17;
assume not (field R) /\ Y = {};
then consider y being object such that
A225: y in X and
A226: R-Seg(y) misses X by A130,A224;
A227: R-Seg(y) /\ Y c= R-Seg(y) /\ X
proof
let x be object;
assume
A228: x in R-Seg(y) /\ Y;
then
A229: x in Y by XBOOLE_0:def 4;
A230: x in R-Seg(y) by A228,XBOOLE_0:def 4;
then [x,y] in R by WELLORD1:1;
then x in field R by RELAT_1:15;
then x in X by A229,XBOOLE_0:def 4;
hence thesis by A230,XBOOLE_0:def 4;
end;
R-Seg(y) /\ X = {} by A226,XBOOLE_0:def 7;
then W1-Seg(y) /\ Y = {} by A212,A224,A225,A227;
then
A231: W1-Seg(y) misses Y by XBOOLE_0:def 7;
y in Y by A225,XBOOLE_0:def 4;
hence thesis by A231;
end;
(field R) /\ Y = {} implies ex a st a in Y & W1-Seg(a) misses Y
proof
set y = the Element of Y;
A232: W1-Seg(a0) c= field R
proof
let z be object;
assume
A233: z in W1-Seg(a0);
then [z,a0] in W1 by WELLORD1:1;
then
A234: z in field W1 by RELAT_1:15;
z <> a0 by A233,WELLORD1:1;
hence thesis by A178,A234;
end;
A235: y in field W1 by A220,A221;
assume
A236: (field R) /\ Y = {};
then not y in field R by A221,XBOOLE_0:def 4;
then y = a0 by A178,A235;
then W1-Seg(y) /\ Y = {} by A236,A232,XBOOLE_1:3,26;
then W1-Seg(y) misses Y by XBOOLE_0:def 7;
hence thesis by A221;
end;
hence thesis by A223;
end;
Y c= field R implies ex a st a in Y & W1-Seg(a) misses Y
proof
assume
A237: Y c= field R;
then consider b being object such that
A238: b in Y & R-Seg(b) misses Y by A130,A221;
take b;
thus thesis by A212,A237,A238;
end;
hence thesis by A222;
end;
A239: for y st y in field W1 holds W1-Seg(y) in D & F.(W1-Seg(y)) = y
proof
let y;
A240: y in field R implies W1-Seg(y) = R-Seg(y)
proof
assume
A241: y in field R;
A242: for x being object holds x in W1-Seg(y) implies x in R-Seg(y)
proof let x be object;
A243: [x,y] in W4 implies [x,y] = [a0,a0] by TARSKI:def 1;
assume
A244: x in W1-Seg(y);
then [x,y] in W1 by WELLORD1:1;
then [x,y] in (R \/ W3) or [x,y] in W4 by XBOOLE_0:def 3;
then
A245: [x,y] in R or [x,y] in W3 or [x,y] in W4 by XBOOLE_0:def 3;
not x=y by A244,WELLORD1:1;
hence thesis by A194,A241,A245,A243,WELLORD1:1,XTUPLE_0:1
,ZFMISC_1:106;
end;
for x being object holds x in R-Seg(y) implies x in W1-Seg(y)
proof let x be object;
assume
A246: x in R-Seg(y);
then [x,y] in R by WELLORD1:1;
then [x,y] in R \/ W3 by XBOOLE_0:def 3;
then
A247: [x,y] in W1 by XBOOLE_0:def 3;
not x=y by A246,WELLORD1:1;
hence thesis by A247,WELLORD1:1;
end;
hence thesis by A242,TARSKI:2;
end;
A248: for x being object holds x in W1-Seg(a0) implies x in field R
proof let x be object;
assume
A249: x in W1-Seg(a0);
then [x,a0] in W1 by WELLORD1:1;
then
A250: x in field W1 by RELAT_1:15;
not x=a0 by A249,WELLORD1:1;
hence thesis by A178,A250;
end;
A251: for x being object holds x in field R implies x in W1-Seg(a0)
proof let x be object;
assume
A252: x in field R;
then [x,a0] in W3 by ZFMISC_1:106;
then [x,a0] in R \/ W3 by XBOOLE_0:def 3;
then [x,a0] in W1 by XBOOLE_0:def 3;
hence thesis by A194,A252,WELLORD1:1;
end;
assume y in field W1;
then y in field R or y=a0 by A178;
hence thesis by A103,A190,A240,A248,A251,TARSKI:2;
end;
for x,y,z being object holds
x in field W1 & y in field W1 & z in field W1 & [x,y] in W1 & [y,z]
in W1 implies [x,z] in W1
proof let x,y,z be object;
assume that
A253: x in field W1 and
y in field W1 and
A254: z in field W1 and
A255: [x,y] in W1 and
A256: [y,z] in W1;
A257: z = a0 implies [x,z] in W1
proof
assume
A258: z = a0;
A259: x = a0 implies [x,z] in W1
proof
assume x = a0;
then [x,z] in W4 by A258,TARSKI:def 1;
hence thesis by A179;
end;
x in field R implies [x,z] in W1
proof
assume x in field R;
then [x,z] in W3 by A258,ZFMISC_1:106;
hence thesis by A179;
end;
hence thesis by A178,A253,A259;
end;
z in field R implies [x,z] in W1
proof
assume
A260: z in field R;
then
A261: [y,z] in R by A195,A256;
A262: y in field R by A195,A256,A260;
then [x,y] in R & x in field R by A195,A255;
then [x,z] in R by A145,A260,A261,A262;
hence thesis by A179;
end;
hence thesis by A178,A254,A257;
end;
then
A263: W1 is_transitive_in field W1 by RELAT_2:def 8;
for x being object holds x in field W1 implies [x,x] in W1
proof let x be object;
A264: x = a0 implies [x,x] in W1
proof
A265: [a0,a0] in W4 by TARSKI:def 1;
assume x=a0;
hence thesis by A179,A265;
end;
A266: x in field R implies [x,x] in W1 by A165,A179;
assume x in field W1;
hence thesis by A178,A266,A264;
end;
then W1 is_reflexive_in field W1 by RELAT_2:def 1;
then W1 well_orders field W1 by A263,A211,A189,A219;
then W1 is well-ordering by WELLORD1:4;
then W1 in G by A2,A193,A239;
then field W1 c= field R by A97;
hence contradiction by A1,A190,A171;
end;
R is_reflexive_in field R by A165,RELAT_2:def 1;
then R well_orders field R by A164,A96,A129,A130;
hence thesis by A103,A170,WELLORD1:4;
end;
theorem
for N ex R st R is well-ordering & field R = N
proof
let N;
consider M such that
A1: N in M & for X,Y holds X in M & Y c= X implies Y in M and
A2: for X holds X in M implies bool X in M and
A3: for X holds X c= M implies X,M are_equipotent or X in M by ZFMISC_1:112;
defpred P[set] means not $1,M are_equipotent;
consider D such that
A4: A in D iff A in bool M & P[A] from XFAMILY:sch 1;
A5: union D c= M
proof
let x be object;
assume x in union D;
then consider A such that
A6: x in A and
A7: A in D by TARSKI:def 4;
A in bool M by A4,A7;
hence thesis by A6;
end;
set F = id D;
for Z st Z in D holds not F.Z in Z & F.Z in union D
proof
let Z;
assume
A8: Z in D;
not Z in Z;
hence not F.Z in Z by A8,FUNCT_1:18;
X in D implies X in union D
proof
A9: X in { X } by TARSKI:def 1;
assume X in D;
then
A10: X in bool M & not X,M are_equipotent by A4;
A11: not { X },M are_equipotent
proof
A12: X <> bool X
proof
assume X = bool X;
then not X in bool X;
hence contradiction by ZFMISC_1:def 1;
end;
assume { X },M are_equipotent;
then consider Z such that
for x being object st x in { X }
ex y being object st y in M & [x,y] in Z and
A13: for y being object st y in M
ex x being object st x in { X } & [x,y] in Z and
A14: for x,z1,y,z2 being object st [x,z1] in Z & [y,z2] in Z
holds x = y iff z1 = z2;
bool X in M by A2,A3,A10;
then consider y being object such that
A15: y in {X} and
A16: [y,bool X] in Z by A13;
consider x being object such that
A17: x in {X} and
A18: [x,X] in Z by A3,A10,A13;
x=X by A17,TARSKI:def 1;
then y=x by A15,TARSKI:def 1;
hence contradiction by A14,A12,A18,A16;
end;
X in M by A3,A10;
then for x being object holds x in {X} implies x in M by TARSKI:def 1;
then { X } c= M;
then { X } in D by A4,A11;
hence thesis by A9,TARSKI:def 4;
end;
then Z in union D by A8;
hence thesis by A8,FUNCT_1:18;
end;
then consider S such that
A19: field S c= union D and
A20: S is well-ordering and
A21: not field S in D and
for y st y in field S holds S-Seg(y) in D & F.(S-Seg(y)) = y by Th5;
not field S c= M or field S,M are_equipotent by A4,A21;
then consider Z such that
A22: for x being object st x in field S
ex y being object st y in M & [x,y] in Z and
A23: for y being object st y in M
ex x being object st x in field S & [x,y] in Z and
A24: for x,z1,y,z2 being object
st [x,z1] in Z & [y,z2] in Z holds x = y iff z1 = z2
by A5,A19;
defpred Q[object,object] means [$2,$1] in Z;
A25: for x being object st x in M ex y being object st Q[x,y]
proof
let x be object;
assume x in M;
then ex y being object st y in field S & [y,x] in Z by A23;
hence thesis;
end;
A26: for x,z1,z2 being object st x in M & Q[x,z1] & Q[x,z2]
holds z1 = z2 by A24;
consider H such that
A27: dom H = M and
A28: for x being object st x in M holds Q[x, H.x] from FUNCT_1:sch 2(A26,A25);
defpred R[object,object] means $2={$1};
defpred P[object] means ex x,y being object st $1=[x,y] & [H.x,H.y] in S;
consider W0 such that
A29: for z being object holds z in W0 iff z in [: M,M :] & P[z]
from XBOOLE_0:sch 1;
A30: for x being object holds x in field S implies x in rng H
proof let x be object;
assume x in field S;
then consider y being object such that
A31: y in M and
A32: [x,y] in Z by A22;
set z1= H.y;
z1 in rng H & [z1,y] in Z by A27,A28,A31,FUNCT_1:def 3;
hence thesis by A24,A32;
end;
for z1,z2 being object
st z1 in dom H & z2 in dom H & H.z1 = H.z2 holds z1 = z2
proof
let z1,z2 be object;
assume that
A33: z1 in dom H & z2 in dom H and
A34: H.z1 = H.z2;
[H.z1,z1] in Z & [H.z2,z2] in Z by A27,A28,A33;
hence thesis by A24,A34;
end;
then
A35: H is one-to-one by FUNCT_1:def 4;
for z being object st z in W0 ex x,y being object st z=[x,y]
proof let z be object;
assume z in W0;
then ex z1,z2 being object st z=[z1,z2] & [H.z1,H.z2] in S by A29;
hence thesis;
end;
then reconsider W0 as Relation by RELAT_1:def 1;
A36: for z being object holds z in field W0 implies z in M
proof let z be object;
assume z in field W0;
then consider z1 being object such that
A37: [z,z1] in W0 or [z1,z] in W0 by Th1;
A38: [z1,z] in W0 implies z in M
proof
assume [z1,z] in W0;
then [z1,z] in [: M,M :] by A29;
hence thesis by ZFMISC_1:87;
end;
[z,z1] in W0 implies z in M
proof
assume [z,z1] in W0;
then [z,z1] in [: M,M :] by A29;
hence thesis by ZFMISC_1:87;
end;
hence thesis by A37,A38;
end;
A39: for x being object st x in N ex y being object st R[x,y];
A40: for x,z1,z2 being object st x in N & R[x,z1] & R[x,z2] holds z1 = z2;
consider H1 such that
A41: dom H1 = N and
A42: for x being object st x in N holds R[x, H1.x]
from FUNCT_1:sch 2(A40,A39);
for z1,z2 being object
st z1 in dom H1 & z2 in dom H1 & H1.z1 = H1.z2 holds z1 = z2
proof
let z1,z2 be object;
assume that
A43: z1 in dom H1 and
A44: z2 in dom H1 and
A45: H1.z1 = H1.z2;
H1.z1={z1} by A41,A42,A43;
then
A46: z1 in H1.z2 by A45,TARSKI:def 1;
H1.z2={z2} by A41,A42,A44;
hence thesis by A46,TARSKI:def 1;
end;
then
A47: H1 is one-to-one by FUNCT_1:def 4;
set S1=W0 |_2 rng H1;
for x being object holds x in rng H implies x in field S
proof let x be object;
assume x in rng H;
then consider z1 being object such that
A48: z1 in dom H & x = H.z1 by FUNCT_1:def 3;
( ex z2 being object st z2 in field S & [z2,z1] in Z)& [x,z1] in Z
by A23,A27,A28,A48;
hence thesis by A24;
end;
then
A49: rng H = field S by A30,TARSKI:2;
for z being object holds z in M implies z in field W0
proof let z be object;
assume
A50: z in M;
ex z1 being object st [z,z1] in W0 or [z1,z] in W0
proof
H.z in field S by A27,A49,A50,FUNCT_1:def 3;
then consider z2 being object such that
A51: [H.z,z2] in S or [z2,H.z] in S by Th1;
A52: [H.z,z2] in S implies ex z1 being object st [z,z1] in W0 or [z1,z] in W0
proof
assume
A53: [H.z,z2] in S;
then z2 in rng H by A49,RELAT_1:15;
then consider z3 being object such that
A54: z3 in dom H and
A55: z2=H.z3 by FUNCT_1:def 3;
take z3;
[z,z3] in [: M,M :] by A27,A50,A54,ZFMISC_1:87;
hence thesis by A29,A53,A55;
end;
[z2,H.z] in S implies ex z1 being object st [z,z1] in W0 or [z1,z] in W0
proof
assume
A56: [z2,H.z] in S;
then z2 in rng H by A49,RELAT_1:15;
then consider z3 being object such that
A57: z3 in dom H and
A58: z2=H.z3 by FUNCT_1:def 3;
take z3;
[z3,z] in [: M,M :] by A27,A50,A57,ZFMISC_1:87;
hence thesis by A29,A56,A58;
end;
hence thesis by A51,A52;
end;
hence thesis by Th1;
end;
then
A59: field W0 = M by A36,TARSKI:2;
for a,b being object
holds [a,b] in W0 iff a in field W0 & b in field W0 & [H.a,H.b ] in S
proof
let a,b be object;
A60: [a,b] in W0 implies a in field W0 & b in field W0 & [H.a,H.b] in S
proof
assume
A61: [a,b] in W0;
then
A62: [a,b] in [: M,M :] by A29;
consider x,y being object such that
A63: [a,b] = [x,y] and
A64: [H.x,H.y] in S by A29,A61;
a=x by A63,XTUPLE_0:1;
hence thesis by A59,A62,A63,A64,XTUPLE_0:1,ZFMISC_1:87;
end;
a in field W0 & b in field W0 & [H.a,H.b] in S implies [a,b] in W0
proof
assume that
A65: a in field W0 & b in field W0 and
A66: [H.a,H.b] in S;
[a,b] in [: M,M :] by A59,A65,ZFMISC_1:87;
hence thesis by A29,A66;
end;
hence thesis by A60;
end;
then H is_isomorphism_of W0,S by A27,A35,A49,A59;
then
A67: (H") is_isomorphism_of S, W0 by WELLORD1:39;
then W0 is well-ordering by A20,WELLORD1:44;
then
A68: S1 is well-ordering by WELLORD1:25;
defpred P[object] means
ex x,y being object st $1=[x,y] & [H1.x,H1.y] in S1;
consider W00 such that
A69: for z being object holds z in W00 iff z in [: N,N :] & P[z]
from XBOOLE_0:sch 1;
for z being object st z in W00 ex x,y being object st z=[x,y]
proof let z be object;
assume z in W00;
then ex z1,z2 being object st z=[z1,z2] & [H1.z1,H1.z2] in S1 by A69;
hence thesis;
end;
then reconsider W00 as Relation by RELAT_1:def 1;
A70: for z being object holds z in field W00 implies z in N
proof let z be object;
assume z in field W00;
then consider z1 being object such that
A71: [z,z1] in W00 or [z1,z] in W00 by Th1;
A72: [z1,z] in W00 implies z in N
proof
assume [z1,z] in W00;
then [z1,z] in [: N,N :] by A69;
hence thesis by ZFMISC_1:87;
end;
[z,z1] in W00 implies z in N
proof
assume [z,z1] in W00;
then [z,z1] in [: N,N :] by A69;
hence thesis by ZFMISC_1:87;
end;
hence thesis by A71,A72;
end;
rng H1 c= M
proof
let x be object;
assume x in rng H1;
then consider y being object such that
A73: y in dom H1 and
A74: x = H1.y by FUNCT_1:def 3;
for z1 being object holds z1 in { y } implies z1 in N
by A41,A73,TARSKI:def 1;
then
A75: { y } c= N;
x = { y } by A41,A42,A73,A74;
hence thesis by A1,A75;
end;
then
A76: field S1 = rng H1 by A20,A59,A67,WELLORD1:31,44;
for z being object holds z in N implies z in field W00
proof let z be object;
assume
A77: z in N;
ex z1 being object st [z,z1] in W00 or [z1,z] in W00
proof
H1.z in field S1 by A41,A76,A77,FUNCT_1:def 3;
then consider z2 being object such that
A78: [H1.z,z2] in S1 or [z2,H1.z] in S1 by Th1;
A79: [H1.z,z2] in S1 implies
ex z1 being object st [z,z1] in W00 or [z1,z] in W00
proof
assume
A80: [H1.z,z2] in S1;
then z2 in rng H1 by A76,RELAT_1:15;
then consider z3 being object such that
A81: z3 in dom H1 and
A82: z2=H1.z3 by FUNCT_1:def 3;
take z3;
[z,z3] in [: N,N :] by A41,A77,A81,ZFMISC_1:87;
hence thesis by A69,A80,A82;
end;
[z2,H1.z] in S1 implies
ex z1 being object st [z,z1] in W00 or [z1,z] in W00
proof
assume
A83: [z2,H1.z] in S1;
then z2 in rng H1 by A76,RELAT_1:15;
then consider z3 being object such that
A84: z3 in dom H1 and
A85: z2=H1.z3 by FUNCT_1:def 3;
take z3;
[z3,z] in [: N,N :] by A41,A77,A84,ZFMISC_1:87;
hence thesis by A69,A83,A85;
end;
hence thesis by A78,A79;
end;
hence thesis by Th1;
end;
then
A86: field W00 = N by A70,TARSKI:2;
for a,b being object
holds [a,b] in W00 iff a in field W00 & b in field W00 & [H1.a
,H1.b] in S1
proof
let a,b be object;
A87: [a,b] in W00 implies a in field W00 & b in field W00 & [H1.a,H1.b] in S1
proof
assume
A88: [a,b] in W00;
then
A89: [a,b] in [: N,N :] by A69;
consider x,y being object such that
A90: [a,b] = [x,y] and
A91: [H1.x,H1.y] in S1 by A69,A88;
a=x by A90,XTUPLE_0:1;
hence thesis by A86,A89,A90,A91,XTUPLE_0:1,ZFMISC_1:87;
end;
a in field W00 & b in field W00 & [H1.a,H1.b] in S1 implies [a,b] in W00
proof
assume that
A92: a in field W00 & b in field W00 and
A93: [H1.a,H1.b] in S1;
[a,b] in [: N,N :] by A86,A92,ZFMISC_1:87;
hence thesis by A69,A93;
end;
hence thesis by A87;
end;
then H1 is_isomorphism_of W00,S1 by A41,A47,A76,A86;
then (H1") is_isomorphism_of S1, W00 by WELLORD1:39;
hence thesis by A68,A86,WELLORD1:44;
end;