deffunc H_{1}( object ) -> set = {$1};

defpred S_{1}[ object ] means $1 is Ordinal;

let X be set ; :: thesis: ex R being Relation st R well_orders X

consider Class being set such that

A1: X in Class and

A2: for Y, Z being set st Y in Class & Z c= Y holds

Z in Class and

for Y being set st Y in Class holds

bool Y in Class and

A3: for Y being set holds

( not Y c= Class or Y,Class are_equipotent or Y in Class ) by ZFMISC_1:112;

consider ON being set such that

A4: for x being object holds

( x in ON iff ( x in Class & S_{1}[x] ) )
from XBOOLE_0:sch 1();

for Y being set st Y in ON holds

( Y is Ordinal & Y c= ON )

A8: ON c= Class by A4;

A9: ON,Class are_equipotent

then consider R being Relation such that

A10: R well_orders Class by A9, Lm1;

consider f being Function such that

A11: ( dom f = X & ( for x being object st x in X holds

f . x = H_{1}(x) ) )
from FUNCT_1:sch 3();

A12: rng f c= Class

field (R |_2 Class) = Class by A10, Th10;

then A19: field ((R |_2 Class) |_2 (rng f)) = rng f by A10, A12, Th10, WELLORD1:31;

R |_2 Class is well-ordering by A10, Th10;

hence ex R being Relation st R well_orders X by A16, A19, Lm1, WELLORD1:25; :: thesis: verum

defpred S

let X be set ; :: thesis: ex R being Relation st R well_orders X

consider Class being set such that

A1: X in Class and

A2: for Y, Z being set st Y in Class & Z c= Y holds

Z in Class and

for Y being set st Y in Class holds

bool Y in Class and

A3: for Y being set holds

( not Y c= Class or Y,Class are_equipotent or Y in Class ) by ZFMISC_1:112;

consider ON being set such that

A4: for x being object holds

( x in ON iff ( x in Class & S

for Y being set st Y in ON holds

( Y is Ordinal & Y c= ON )

proof

then reconsider ON = ON as epsilon-transitive epsilon-connected set by ORDINAL1:19;
let Y be set ; :: thesis: ( Y in ON implies ( Y is Ordinal & Y c= ON ) )

assume A5: Y in ON ; :: thesis: ( Y is Ordinal & Y c= ON )

hence Y is Ordinal by A4; :: thesis: Y c= ON

reconsider A = Y as Ordinal by A4, A5;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in ON )

assume A6: x in Y ; :: thesis: x in ON

then x in A ;

then reconsider B = x as Ordinal ;

A7: B c= A by A6, ORDINAL1:def 2;

A in Class by A4, A5;

then B in Class by A2, A7;

hence x in ON by A4; :: thesis: verum

end;assume A5: Y in ON ; :: thesis: ( Y is Ordinal & Y c= ON )

hence Y is Ordinal by A4; :: thesis: Y c= ON

reconsider A = Y as Ordinal by A4, A5;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in ON )

assume A6: x in Y ; :: thesis: x in ON

then x in A ;

then reconsider B = x as Ordinal ;

A7: B c= A by A6, ORDINAL1:def 2;

A in Class by A4, A5;

then B in Class by A2, A7;

hence x in ON by A4; :: thesis: verum

A8: ON c= Class by A4;

A9: ON,Class are_equipotent

proof

field (RelIncl ON) = ON
by Def1;
assume
not ON,Class are_equipotent
; :: thesis: contradiction

then ON in Class by A3, A8;

then ON in ON by A4;

hence contradiction ; :: thesis: verum

end;then ON in Class by A3, A8;

then ON in ON by A4;

hence contradiction ; :: thesis: verum

then consider R being Relation such that

A10: R well_orders Class by A9, Lm1;

consider f being Function such that

A11: ( dom f = X & ( for x being object st x in X holds

f . x = H

A12: rng f c= Class

proof

A16:
X, rng f are_equipotent
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in Class )

assume x in rng f ; :: thesis: x in Class

then consider y being object such that

A13: y in dom f and

A14: x = f . y by FUNCT_1:def 3;

A15: {y} c= X by A11, A13, TARSKI:def 1;

f . y = {y} by A11, A13;

hence x in Class by A1, A2, A14, A15; :: thesis: verum

end;assume x in rng f ; :: thesis: x in Class

then consider y being object such that

A13: y in dom f and

A14: x = f . y by FUNCT_1:def 3;

A15: {y} c= X by A11, A13, TARSKI:def 1;

f . y = {y} by A11, A13;

hence x in Class by A1, A2, A14, A15; :: thesis: verum

proof

set Q = R |_2 Class;
take
f
; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = X & rng f = rng f )

thus f is one-to-one :: thesis: ( dom f = X & rng f = rng f )

end;thus f is one-to-one :: thesis: ( dom f = X & rng f = rng f )

proof

thus
( dom f = X & rng f = rng f )
by A11; :: thesis: verum
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )

assume that

A17: ( x in dom f & y in dom f ) and

A18: f . x = f . y ; :: thesis: x = y

( f . x = {x} & f . y = {y} ) by A11, A17;

hence x = y by A18, ZFMISC_1:3; :: thesis: verum

end;assume that

A17: ( x in dom f & y in dom f ) and

A18: f . x = f . y ; :: thesis: x = y

( f . x = {x} & f . y = {y} ) by A11, A17;

hence x = y by A18, ZFMISC_1:3; :: thesis: verum

field (R |_2 Class) = Class by A10, Th10;

then A19: field ((R |_2 Class) |_2 (rng f)) = rng f by A10, A12, Th10, WELLORD1:31;

R |_2 Class is well-ordering by A10, Th10;

hence ex R being Relation st R well_orders X by A16, A19, Lm1, WELLORD1:25; :: thesis: verum