deffunc H1( object ) -> set = {\$1};
defpred S1[ 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 & S1[x] ) ) from for Y being set st Y in ON holds
( Y is Ordinal & Y c= ON )
proof
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 ;
A in Class by A4, A5;
then B in Class by A2, A7;
hence x in ON by A4; :: thesis: verum
end;
then reconsider ON = ON as epsilon-transitive epsilon-connected set by ORDINAL1:19;
A8: ON c= Class by A4;
A9: ON,Class are_equipotent
proof end;
field (RelIncl ON) = ON by Def1;
then consider R being Relation such that
A10: R well_orders Class by ;
consider f being Function such that
A11: ( dom f = X & ( for x being object st x in X holds
f . x = H1(x) ) ) from A12: rng f c= Class
proof
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 ;
f . y = {y} by ;
hence x in Class by A1, A2, A14, A15; :: thesis: verum
end;
A16: X, rng f are_equipotent
proof
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 )
proof
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 ;
hence x = y by ; :: thesis: verum
end;
thus ( dom f = X & rng f = rng f ) by A11; :: thesis: verum
end;
set Q = R |_2 Class;
field (R |_2 Class) = Class by ;
then A19: field ((R |_2 Class) |_2 (rng f)) = rng f by ;
R |_2 Class is well-ordering by ;
hence ex R being Relation st R well_orders X by ; :: thesis: verum