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 and
A2: dom f = X and
A3: 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 A2, A3, FUNCT_2:2;
reconsider g = f " as Function of A,X by A1, A3, FUNCT_2:25;
A4: dom g = A by A1, A3, FUNCT_1:33;
reconsider f9 = f as one-to-one Function by A1;
A5: ( RelIncl A is connected & RelIncl A is well_founded ) by WELLORD2:3, WELLORD2:5;
A6: dom (RelIncl A) = A by ORDERS_1:14;
rng (RelIncl A) = A by ORDERS_1:14;
then A7: rng (f * (RelIncl A)) = A by A3, A6, RELAT_1:28;
set R = (f * (RelIncl A)) * g;
dom (f * (RelIncl A)) = X by A2, A3, A6, RELAT_1:27;
then A8: dom ((f * (RelIncl A)) * g) = X by A4, A7, RELAT_1:27;
rng g = X by A1, A2, FUNCT_1:33;
then rng ((f * (RelIncl A)) * g) = X by A4, A7, RELAT_1:28;
then A9: field ((f * (RelIncl A)) * g) = X \/ X by A8, RELAT_1:def 6
.= X ;
reconsider R = (f * (RelIncl A)) * g as Relation of X ;
(f9 * (RelIncl A)) * (f9 ") is_reflexive_in X by A9, RELAT_2:def 9;
then reconsider R = R as Order of X by A8, PARTFUN1:def 2;
A10: 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, A2, A3, A9, 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 A11: [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:15; :: thesis: [(f . a),(f . b)] in RelIncl A
consider x being set such that
A12: [a,x] in f * (RelIncl A) and
A13: [x,b] in g by A11, RELAT_1:def 8;
A14: ( b = g . x & x in dom g ) by A13, FUNCT_1:1;
consider y being set such that
A15: [a,y] in f and
A16: [y,x] in RelIncl A by A12, RELAT_1:def 8;
y = f . a by A15, FUNCT_1:1;
hence [(f . a),(f . b)] in RelIncl A by A1, A3, A16, A14, FUNCT_1:35; :: thesis: verum

end;

assume that
A17: a in field R and
A18: b in field R and
A19: [(f . a),(f . b)] in RelIncl A ; :: thesis: [a,b] in R
[a,(f . a)] in f by A2, A9, A17, FUNCT_1:1;
then A20: [a,(f . b)] in f * (RelIncl A) by A19, RELAT_1:def 8;
( (f ") . (f . b) = b & f . b in A ) by A1, A2, A3, A9, A18, FUNCT_1:34, FUNCT_1:def 3;
then [(f . b),b] in g by A4, FUNCT_1:1;
hence [a,b] in R by A20, RELAT_1:def 8; :: thesis: verum

end;

then f " is_isomorphism_of RelIncl A,R by WELLORD1:39;
then ( R is connected & R is well_founded ) by A5, WELLORD1:43;
then A21: ( R is_connected_in X & R is_well_founded_in X ) by A9, RELAT_2:def 14, WELLORD1:3;
take R ; :: thesis: ( R well_orders X & order_type_of R = A )
A22: R is_antisymmetric_in X by A9, RELAT_2:def 12;
( R is_reflexive_in X & R is_transitive_in X ) by A9, RELAT_2:def 9, RELAT_2:def 16;
hence R well_orders X by A22, A21, WELLORD1:def 5; :: thesis: order_type_of R = A
then A23: R is well-ordering by A9, WELLORD1:4;
R, RelIncl A are_isomorphic by A10, WELLORD1:def 8;
hence order_type_of R = A by A23, WELLORD2:def 2; :: thesis: verum