let N be set ; :: thesis: ex R being Relation st
( R is well-ordering & field R = N )
consider M being set such that
A1: ( N in M & ( for X, Y being set st X in M & Y c= X holds
Y in M ) ) and
A2: for X being set st X in M holds
bool X in M and
A3: for X being set holds
( not X c= M or X,M are_equipotent or X in M ) by ZFMISC_1:112;
defpred S1[ set ] means not $1,M are_equipotent ;
consider D being set such that
A4: for A being set holds
( A in D iff ( A in bool M & S1[A] ) ) from XFAMILY:sch 1();
 A5: union D c= M
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union D or x in M )
assume x in union D ; :: thesis: x in M
then consider A being set such that
A6: x in A and
A7: A in D by TARSKI:def 4;
A in bool M by A4, A7;
hence x in M by A6; :: thesis: verum
end;
set F = id D;
for Z being set st Z in D holds
( not (id D) . Z in Z & (id D) . Z in union D )
proof
let Z be set ; :: thesis: ( Z in D implies ( not (id D) . Z in Z & (id D) . Z in union D ) )
assume A8: Z in D ; :: thesis: ( not (id D) . Z in Z & (id D) . Z in union D )
not Z in Z ;
hence not (id D) . Z in Z by A8, FUNCT_1:18; :: thesis: (id D) . Z in union D
for X being set st X in D holds
X in union D
proof
let X be set ; :: thesis: ( X in D implies X in union D )
A9: X in {X} by TARSKI:def 1;
assume X in D ; :: thesis: X in union 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 assume {X},M are_equipotent ; :: thesis: contradiction
then consider Z being set such that
for x being object st x in {X} holds
ex y being object st
( y in M & [x,y] in Z ) and
A13: for y being object st y in M holds
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; :: thesis: verum
end;
X in M by A3, A10;
then for x being object st x in {X} holds
x in M by TARSKI:def 1;
then {X} c= M ;
then {X} in D by A4, A11;
hence X in union D by A9, TARSKI:def 4; :: thesis: verum
end;
then Z in union D by A8;
hence (id D) . Z in union D by A8, FUNCT_1:18; :: thesis: verum
end;
then consider S being Relation such that
A19: field S c= union D and
A20: S is well-ordering and
A21: not field S in D and
for y being set st y in field S holds
( S -Seg y in D & (id D) . (S -Seg y) = y ) by Th5;
( not field S c= M or field S,M are_equipotent ) by A4, A21;
then consider Z being set such that
A22: for x being object st x in field S holds
ex y being object st
( y in M & [x,y] in Z ) and
A23: for y being object st y in M holds
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 S2[ object , object ] means [$2,$1] in Z;
A25: for x being object st x in M holds
ex y being object st S2[x,y]
proof
let x be object ; :: thesis: ( x in M implies ex y being object st S2[x,y] )
assume x in M ; :: thesis: ex y being object st S2[x,y]
then ex y being object st
( y in field S & [y,x] in Z ) by A23;
hence ex y being object st S2[x,y] ; :: thesis: verum
end;
A26: for x, z1, z2 being object st x in M & S2[x,z1] & S2[x,z2] holds
z1 = z2 by A24;
consider H being Function such that
A27: dom H = M and
A28: for x being object st x in M holds
S2[x,H . x] from FUNCT_1:sch 2(A26, A25);
 defpred S3[ object , object ] means $2 = {$1};
defpred S4[ object ] means ex x, y being object st
( $1 = [x,y] & [(H . x),(H . y)] in S );
consider W0 being set such that
A29: for z being object holds
( z in W0 iff ( z in [:M,M:] & S4[z] ) ) from XBOOLE_0:sch 1();
 A30: for x being object st x in field S holds
x in rng H
proof
let x be object ; :: thesis: ( x in field S implies x in rng H )
assume x in field S ; :: thesis: x in rng H
then consider y being object such that
A31: y in M and
A32: [x,y] in Z by A22;
set z1 = H . y;
( H . y in rng H & [(H . y),y] in Z ) by A27, A28, A31, FUNCT_1:def 3;
hence x in rng H by A24, A32; :: thesis: verum
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 ; :: thesis: ( z1 in dom H & z2 in dom H & H . z1 = H . z2 implies z1 = z2 )
assume that
A33: ( z1 in dom H & z2 in dom H ) and
A34: H . z1 = H . z2 ; :: thesis: z1 = z2
( [(H . z1),z1] in Z & [(H . z2),z2] in Z ) by A27, A28, A33;
hence z1 = z2 by A24, A34; :: thesis: verum
end;
then A35: H is one-to-one by FUNCT_1:def 4;
for z being object st z in W0 holds
ex x, y being object st z = [x,y]
proof
let z be object ; :: thesis: ( z in W0 implies ex x, y being object st z = [x,y] )
assume z in W0 ; :: thesis: ex x, y being object st z = [x,y]
then ex z1, z2 being object st
( z = [z1,z2] & [(H . z1),(H . z2)] in S ) by A29;
hence ex x, y being object st z = [x,y] ; :: thesis: verum
end;
then reconsider W0 = W0 as Relation by RELAT_1:def 1;
A36: for z being object st z in field W0 holds
z in M
proof
let z be object ; :: thesis: ( z in field W0 implies z in M )
assume z in field W0 ; :: thesis: z in M
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 ; :: thesis: z in M
then [z1,z] in [:M,M:] by A29;
hence z in M by ZFMISC_1:87; :: thesis: verum
end;
( [z,z1] in W0 implies z in M )
proof
assume [z,z1] in W0 ; :: thesis: z in M
then [z,z1] in [:M,M:] by A29;
hence z in M by ZFMISC_1:87; :: thesis: verum
end;
hence z in M by A37, A38; :: thesis: verum
end;
A39: for x being object st x in N holds
ex y being object st S3[x,y] ;
A40: for x, z1, z2 being object st x in N & S3[x,z1] & S3[x,z2] holds
z1 = z2 ;
consider H1 being Function such that
A41: dom H1 = N and
A42: for x being object st x in N holds
S3[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 ; :: thesis: ( z1 in dom H1 & z2 in dom H1 & H1 . z1 = H1 . z2 implies z1 = z2 )
assume that
A43: z1 in dom H1 and
A44: z2 in dom H1 and
A45: H1 . z1 = H1 . z2 ; :: thesis: z1 = 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 z1 = z2 by A46, TARSKI:def 1; :: thesis: verum
end;
then A47: H1 is one-to-one by FUNCT_1:def 4;
set S1 = W0 |_2 (rng H1);
for x being object st x in rng H holds
x in field S
proof
let x be object ; :: thesis: ( x in rng H implies x in field S )
assume x in rng H ; :: thesis: x in field S
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 x in field S by A24; :: thesis: verum
end;
then A49: rng H = field S by A30, TARSKI:2;
for z being object st z in M holds
z in field W0
proof
let z be object ; :: thesis: ( z in M implies z in field W0 )
assume A50: z in M ; :: thesis: z in field W0
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 ; :: thesis: ex z1 being object st
( [z,z1] in W0 or [z1,z] in W0 )
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 ; :: thesis: ( [z,z3] in W0 or [z3,z] in W0 )
[z,z3] in [:M,M:] by A27, A50, A54, ZFMISC_1:87;
hence ( [z,z3] in W0 or [z3,z] in W0 ) by A29, A53, A55; :: thesis: verum
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 ; :: thesis: ex z1 being object st
( [z,z1] in W0 or [z1,z] in W0 )
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 ; :: thesis: ( [z,z3] in W0 or [z3,z] in W0 )
[z3,z] in [:M,M:] by A27, A50, A57, ZFMISC_1:87;
hence ( [z,z3] in W0 or [z3,z] in W0 ) by A29, A56, A58; :: thesis: verum
end;
hence ex z1 being object st
( [z,z1] in W0 or [z1,z] in W0 ) by A51, A52; :: thesis: verum
end;
hence z in field W0 by Th1; :: thesis: verum
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 ; :: thesis: ( [a,b] in W0 iff ( a in field W0 & b in field W0 & [(H . a),(H . b)] in S ) )
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 ; :: thesis: ( a in field W0 & b in field W0 & [(H . a),(H . b)] in S )
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 ( a in field W0 & b in field W0 & [(H . a),(H . b)] in S ) by A59, A62, A63, A64, XTUPLE_0:1, ZFMISC_1:87; :: thesis: verum
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 ; :: thesis: [a,b] in W0
[a,b] in [:M,M:] by A59, A65, ZFMISC_1:87;
hence [a,b] in W0 by A29, A66; :: thesis: verum
end;
hence ( [a,b] in W0 iff ( a in field W0 & b in field W0 & [(H . a),(H . b)] in S ) ) by A60; :: thesis: verum
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: W0 |_2 (rng H1) is well-ordering by WELLORD1:25;
defpred S5[ object ] means ex x, y being object st
( $1 = [x,y] & [(H1 . x),(H1 . y)] in W0 |_2 (rng H1) );
consider W00 being set such that
A69: for z being object holds
( z in W00 iff ( z in [:N,N:] & S5[z] ) ) from XBOOLE_0:sch 1();
 for z being object st z in W00 holds
ex x, y being object st z = [x,y]
proof
let z be object ; :: thesis: ( z in W00 implies ex x, y being object st z = [x,y] )
assume z in W00 ; :: thesis: ex x, y being object st z = [x,y]
then ex z1, z2 being object st
( z = [z1,z2] & [(H1 . z1),(H1 . z2)] in W0 |_2 (rng H1) ) by A69;
hence ex x, y being object st z = [x,y] ; :: thesis: verum
end;
then reconsider W00 = W00 as Relation by RELAT_1:def 1;
A70: for z being object st z in field W00 holds
z in N
proof
let z be object ; :: thesis: ( z in field W00 implies z in N )
assume z in field W00 ; :: thesis: z in N
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 ; :: thesis: z in N
then [z1,z] in [:N,N:] by A69;
hence z in N by ZFMISC_1:87; :: thesis: verum
end;
( [z,z1] in W00 implies z in N )
proof
assume [z,z1] in W00 ; :: thesis: z in N
then [z,z1] in [:N,N:] by A69;
hence z in N by ZFMISC_1:87; :: thesis: verum
end;
hence z in N by A71, A72; :: thesis: verum
end;
rng H1 c= M
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng H1 or x in M )
assume x in rng H1 ; :: thesis: x in M
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 st z1 in {y} holds
z1 in N by A41, A73, TARSKI:def 1;
then A75: {y} c= N ;
x = {y} by A41, A42, A73, A74;
hence x in M by A1, A75; :: thesis: verum
end;
then A76: field (W0 |_2 (rng H1)) = rng H1 by A20, A59, A67, WELLORD1:31, WELLORD1:44;
for z being object st z in N holds
z in field W00
proof
let z be object ; :: thesis: ( z in N implies z in field W00 )
assume A77: z in N ; :: thesis: z in field W00
ex z1 being object st
( [z,z1] in W00 or [z1,z] in W00 )
proof
H1 . z in field (W0 |_2 (rng H1)) by A41, A76, A77, FUNCT_1:def 3;
then consider z2 being object such that
A78: ( [(H1 . z),z2] in W0 |_2 (rng H1) or [z2,(H1 . z)] in W0 |_2 (rng H1) ) by Th1;
A79: ( [(H1 . z),z2] in W0 |_2 (rng H1) implies ex z1 being object st
( [z,z1] in W00 or [z1,z] in W00 ) )
proof
assume A80: [(H1 . z),z2] in W0 |_2 (rng H1) ; :: thesis: ex z1 being object st
( [z,z1] in W00 or [z1,z] in W00 )
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 ; :: thesis: ( [z,z3] in W00 or [z3,z] in W00 )
[z,z3] in [:N,N:] by A41, A77, A81, ZFMISC_1:87;
hence ( [z,z3] in W00 or [z3,z] in W00 ) by A69, A80, A82; :: thesis: verum
end;
( [z2,(H1 . z)] in W0 |_2 (rng H1) implies ex z1 being object st
( [z,z1] in W00 or [z1,z] in W00 ) )
proof
assume A83: [z2,(H1 . z)] in W0 |_2 (rng H1) ; :: thesis: ex z1 being object st
( [z,z1] in W00 or [z1,z] in W00 )
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 ; :: thesis: ( [z,z3] in W00 or [z3,z] in W00 )
[z3,z] in [:N,N:] by A41, A77, A84, ZFMISC_1:87;
hence ( [z,z3] in W00 or [z3,z] in W00 ) by A69, A83, A85; :: thesis: verum
end;
hence ex z1 being object st
( [z,z1] in W00 or [z1,z] in W00 ) by A78, A79; :: thesis: verum
end;
hence z in field W00 by Th1; :: thesis: verum
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 W0 |_2 (rng H1) ) )
proof
let a, b be object ; :: thesis: ( [a,b] in W00 iff ( a in field W00 & b in field W00 & [(H1 . a),(H1 . b)] in W0 |_2 (rng H1) ) )
A87: ( [a,b] in W00 implies ( a in field W00 & b in field W00 & [(H1 . a),(H1 . b)] in W0 |_2 (rng H1) ) )
proof
assume A88: [a,b] in W00 ; :: thesis: ( a in field W00 & b in field W00 & [(H1 . a),(H1 . b)] in W0 |_2 (rng H1) )
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 W0 |_2 (rng H1) by A69, A88;
a = x by A90, XTUPLE_0:1;
hence ( a in field W00 & b in field W00 & [(H1 . a),(H1 . b)] in W0 |_2 (rng H1) ) by A86, A89, A90, A91, XTUPLE_0:1, ZFMISC_1:87; :: thesis: verum
end;
( a in field W00 & b in field W00 & [(H1 . a),(H1 . b)] in W0 |_2 (rng H1) implies [a,b] in W00 )
proof
assume that
A92: ( a in field W00 & b in field W00 ) and
A93: [(H1 . a),(H1 . b)] in W0 |_2 (rng H1) ; :: thesis: [a,b] in W00
[a,b] in [:N,N:] by A86, A92, ZFMISC_1:87;
hence [a,b] in W00 by A69, A93; :: thesis: verum
end;
hence ( [a,b] in W00 iff ( a in field W00 & b in field W00 & [(H1 . a),(H1 . b)] in W0 |_2 (rng H1) ) ) by A87; :: thesis: verum
end;
then H1 is_isomorphism_of W00,W0 |_2 (rng H1) by A41, A47, A76, A86;
then H1 " is_isomorphism_of W0 |_2 (rng H1),W00 by WELLORD1:39;
hence ex R being Relation st
( R is well-ordering & field R = N ) by A68, A86, WELLORD1:44; :: thesis: verum