let X be set ; :: thesis: for A being Ordinal st X,A are_equipotent holds
ex R being Order of X st
( R well_orders X & order_type_of R = A )
let A be Ordinal; :: thesis: ( X,A are_equipotent implies ex R being Order of X st
( R well_orders X & order_type_of R = A ) )
given f being Function such that A1: ( f is one-to-one & dom f = X & rng f = A ) ; :: according to WELLORD2:def 4 :: thesis: ex R being Order of X st
( R well_orders X & order_type_of R = A )
reconsider f = f as Function of X,A by A1, FUNCT_2:4;
reconsider f' = f as one-to-one Function by A1;
reconsider g = f " as Function of A,X by A1, FUNCT_2:31;
A2: ( dom g = A & rng g = X ) by A1, FUNCT_1:55;
set R = (f * (RelIncl A)) * g;
( dom (RelIncl A) = A & rng (RelIncl A) = A ) by ORDERS_1:99;
then ( rng (f * (RelIncl A)) = A & dom (f * (RelIncl A)) = X ) by A1, RELAT_1:46, RELAT_1:47;
then A3: ( dom ((f * (RelIncl A)) * g) = X & rng ((f * (RelIncl A)) * g) = X ) by A2, RELAT_1:46, RELAT_1:47;
then A4: field ((f * (RelIncl A)) * g) = X \/ X by RELAT_1:def 6
.= X ;
then A5: ( (f' * (RelIncl A)) * (f' " ) is_reflexive_in X & (f' * (RelIncl A)) * (f' " ) is_antisymmetric_in X & (f' * (RelIncl A)) * (f' " ) is_transitive_in X ) by RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
reconsider R = (f * (RelIncl A)) * g as Relation of X ;
reconsider R = R as Order of X by A3, A5, PARTFUN1:def 4;
A6: f is_isomorphism_of R, RelIncl A

proof

thus ( dom f = field R & rng f = field (RelIncl A) & f is one-to-one ) by A1, A4, WELLORD2:def 1; :: according to WELLORD1:def 7 :: thesis: for b₁, b₂ being set holds
( ( not [b₁,b₂] in R or ( b₁ in field R & b₂ in field R & [(f . b₁),(f . b₂)] in RelIncl A ) ) & ( not b₁ in field R or not b₂ in field R or not [(f . b₁),(f . b₂)] in RelIncl A or [b₁,b₂] in R ) )
let a, b be set ; :: thesis: ( ( not [a,b] in R or ( a in field R & b in field R & [(f . a),(f . b)] in RelIncl A ) ) & ( not a in field R or not b in field R or not [(f . a),(f . b)] in RelIncl A or [a,b] in R ) )

hereby :: thesis: ( not a in field R or not b in field R or not [(f . a),(f . b)] in RelIncl A or [a,b] in R )

assume A7: [a,b] in R ; :: thesis: ( a in field R & b in field R & [(f . a),(f . b)] in RelIncl A )
hence ( a in field R & b in field R ) by RELAT_1:30; :: thesis: [(f . a),(f . b)] in RelIncl A
consider x being set such that
A8: ( [a,x] in f * (RelIncl A) & [x,b] in g ) by A7, RELAT_1:def 8;
consider y being set such that
A9: ( [a,y] in f & [y,x] in RelIncl A ) by A8, RELAT_1:def 8;
( y = f . a & b = g . x & a in dom f & x in dom g ) by A8, A9, FUNCT_1:8;
hence [(f . a),(f . b)] in RelIncl A by A1, A9, FUNCT_1:57; :: thesis: verum

end;

assume A10: ( a in field R & b in field R & [(f . a),(f . b)] in RelIncl A ) ; :: thesis: [a,b] in R
then ( (f " ) . (f . b) = b & f . b in A ) by A1, A4, FUNCT_1:56, FUNCT_1:def 5;
then A11: ( [a,(f . a)] in f & [(f . b),b] in g ) by A1, A2, A4, A10, FUNCT_1:8;
then [a,(f . b)] in f * (RelIncl A) by A10, RELAT_1:def 8;
hence [a,b] in R by A11, RELAT_1:def 8; :: thesis: verum

end;

then A12: f " is_isomorphism_of RelIncl A,R by WELLORD1:49;
A13: R, RelIncl A are_isomorphic by A6, WELLORD1:def 8;
take R ; :: thesis: ( R well_orders X & order_type_of R = A )
thus R well_orders X :: thesis: order_type_of R = A

proof

thus ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X ) by A4, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16; :: according to WELLORD1:def 5 :: thesis: ( R is_connected_in X & R is_well_founded_in X )
( RelIncl A is connected & RelIncl A is well_founded ) by WELLORD2:4, WELLORD2:6;
then ( R is connected & R is well_founded ) by A12, WELLORD1:53;
hence ( R is_connected_in X & R is_well_founded_in X ) by A4, RELAT_2:def 14, WELLORD1:5; :: thesis: verum

end;

then R is well-ordering by A4, WELLORD1:8;
hence order_type_of R = A by A13, WELLORD2:def 2; :: thesis: verum